# Biconditional in terms of NAND

## Theorem

$p \iff q \dashv \vdash \paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \uparrow \paren {p \uparrow q}$

where $\iff$ denotes logical biconditional and $\uparrow$ denotes logical NAND.

## Proof

 $\ds p \iff q$ $\dashv \vdash$ $\ds \neg \paren {p \oplus q}$ Exclusive Or is Negation of Biconditional $\ds$ $\dashv \vdash$ $\ds \neg \paren {\paren {p \lor q} \land \neg \paren {p \land q} }$ Definition of Exclusive Or $\ds$ $\dashv \vdash$ $\ds \neg \paren {\paren {p \lor q} \land \paren {p \uparrow q} }$ Definition of Logical NAND $\ds$ $\dashv \vdash$ $\ds \neg \paren {\paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \land \paren {p \uparrow q} }$ Disjunction in terms of NAND $\ds$ $\dashv \vdash$ $\ds \paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \uparrow \paren {p \uparrow q}$ Definition of Logical NAND

$\blacksquare$