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. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 hadrot ⊢ hadd φ ψ χ ↔ hadd ψ χ φ
2 hadbi ⊢ hadd ψ χ φ ↔ ψ ↔ χ ↔ φ
3 1 2 bitri ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
4 biass ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ ↔ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
5 3 4 mpbir ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
6 5 biimpri ⊢ φ → hadd φ ψ χ ↔ ψ ↔ χ