Metamath Proof Explorer


Theorem hadass

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

Ref Expression
Assertion hadass haddφψχφψχ

Proof

Step Hyp Ref Expression
1 df-had haddφψχφψχ
2 xorass φψχφψχ
3 1 2 bitri haddφψχφψχ