Theorem hadcomb

Commutative law for the adders sum. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \varphi , \chi , \psi ) \)
Proof
l0
biid
xorcom
l2
xorbi12i l0 _
\( \vdash \varphi \veebar (\psi \veebar \chi) \leftrightarrow \varphi \veebar (\chi \veebar \psi) \)
l3
hadass
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \veebar (\psi \veebar \chi) \)
hadass
\( \vdash \text{ hadd } ( \varphi , \chi , \psi ) \leftrightarrow \varphi \veebar (\chi \veebar \psi) \)
3bitr4i l2 l3 _