Theorem hadass

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

Conclusion
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \veebar (\psi \veebar \chi) \)
Proof
l0
df-had
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \veebar \psi) \veebar \chi \)
xorass
\( \vdash (\varphi \veebar \psi) \veebar \chi \leftrightarrow \varphi \veebar (\psi \veebar \chi) \)
bitri l0 _