Theorem had1
If the first input is true, then the adder sum is equivalent to the
biconditionality of the other two inputs, and conversely. (Contributed by
Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen,
11-Jul-2020.) Strengthen to a biconditional. (Revised by BJ,
10-Aug-2026.)
Conclusion
\( \vdash \varphi \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi)) \)
Proof
l0
hadrot
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \psi , \chi , \varphi ) \)
hadbi
\( \vdash \text{ hadd } ( \psi , \chi , \varphi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi) \)
l2
bitri l0 _
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi) \)
birot
\( \vdash \varphi \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi)) \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi)) \)
mpbir l2 _