\begin{definition}[Definition:Biconditional]
The '''biconditional''' is a binary connective:
:$p \iff q$
defined as:
:$\paren {p \implies q} \land \paren {q \implies p}$
That is:
:'''''If'' $p$ is true, ''then'' $q$ is true, ''and if'' $q$ is true, ''then'' $p$ is true'''.
$p \iff q$ can be voiced:
:'''$p$ if and only if $q$.'''
\end{definition}