Theorem hadcoma

Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 17-Dec-2023.)

Conclusion
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \psi , \varphi , \chi ) \)
Proof
bicom
l1
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow \varphi \leftrightarrow \chi) \)
l2
hadbi
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi) \)
hadbi
\( \vdash \text{ hadd } ( \psi , \varphi , \chi ) \leftrightarrow (\psi \leftrightarrow \varphi \leftrightarrow \chi) \)
3bitr4i l1 l2 _