Theorem hadbi

The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi) \)
Proof
l0
df-xor
\( \vdash (\varphi \veebar \psi) \veebar \chi \leftrightarrow \neg (\varphi \veebar \psi \leftrightarrow \chi) \)
l1
df-had
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \veebar \psi) \veebar \chi \)
xnor
l3
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\neg (\varphi \veebar \psi) \leftrightarrow \chi) \)
nbbn
\( \vdash \neg (\varphi \veebar \psi) \leftrightarrow \chi \leftrightarrow \neg (\varphi \veebar \psi \leftrightarrow \chi) \)
bitri l3 _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow \neg (\varphi \veebar \psi \leftrightarrow \chi) \)
3bitr4i l0 l1 _