Theorem cadcoma

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

Conclusion
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ cadd } ( \psi , \varphi , \chi ) \)
Proof
l0
ancom
xorcom
anbi2i _
l3
orbi12i l0 _
\( \vdash \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \leftrightarrow \psi \wedge \varphi \vee \chi \wedge (\psi \veebar \varphi) \)
l4
df-cad
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \)
df-cad
\( \vdash \text{ cadd } ( \psi , \varphi , \chi ) \leftrightarrow \psi \wedge \varphi \vee \chi \wedge (\psi \veebar \varphi) \)
3bitr4i l3 l4 _