Metamath Proof Explorer

Theorem had1

Description: If the first input is true, then the adder sum is equivalent to the biconditionality of the other two inputs, and conversely. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020) Strengthen to a biconditional. (Revised by BJ, 10-Aug-2026)

Ref Expression
Assertion had1 ⊢ φ ↔ hadd φ ψ χ ↔ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 hadrot ⊢ hadd φ ψ χ ↔ hadd ψ χ φ
2 hadbi ⊢ hadd ψ χ φ ↔ ψ ↔ χ ↔ φ
3 1 2 bitri ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
4 birot ⊢ φ ↔ hadd φ ψ χ ↔ ψ ↔ χ ↔ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
5 3 4 mpbir ⊢ φ ↔ hadd φ ψ χ ↔ ψ ↔ χ