Metamath Proof Explorer


Theorem hadbi

Description: The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion hadbi haddφψχφψχ

Proof

Step Hyp Ref Expression
1 df-xor φψχ¬φψχ
2 df-had haddφψχφψχ
3 xnor φψ¬φψ
4 3 bibi1i φψχ¬φψχ
5 nbbn ¬φψχ¬φψχ
6 4 5 bitri φψχ¬φψχ
7 1 2 6 3bitr4i haddφψχφψχ