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 φ ψ χ ↔ φ ↔ ψ ↔ χ