Metamath Proof Explorer

Theorem wl-hadbi123d

Description: Equivalence theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016) Alternative definition. (Revised by Wolf Lammen, 24-Apr-2024)

Ref Expression
Hypotheses wl-hadbid.1 ⊢ φ → ψ ↔ χ
wl-hadbid.2 ⊢ φ → θ ↔ τ
wl-hadbid.3 ⊢ φ → η ↔ ζ
Assertion wl-hadbi123d ⊢ φ → hadd ψ θ η ↔ hadd χ τ ζ

Proof

Step Hyp Ref Expression
1 wl-hadbid.1 ⊢ φ → ψ ↔ χ
2 wl-hadbid.2 ⊢ φ → θ ↔ τ
3 wl-hadbid.3 ⊢ φ → η ↔ ζ
4 1 2 bibi12d ⊢ φ → ψ ↔ θ ↔ χ ↔ τ
5 4 3 bibi12d ⊢ φ → ψ ↔ θ ↔ η ↔ χ ↔ τ ↔ ζ
6 wl-dfhad3 ⊢ hadd ψ θ η ↔ ψ ↔ θ ↔ η
7 wl-dfhad3 ⊢ hadd χ τ ζ ↔ χ ↔ τ ↔ ζ
8 5 6 7 3bitr4g ⊢ φ → hadd ψ θ η ↔ hadd χ τ ζ