Metamath Proof Explorer

Theorem hadbi123d

Description: Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 hadbid.1 ⊢ φ → ψ ↔ χ
2 hadbid.2 ⊢ φ → θ ↔ τ
3 hadbid.3 ⊢ φ → η ↔ ζ
4 1 2 xorbi12d ⊢ φ → ψ ⊻ θ ↔ χ ⊻ τ
5 4 3 xorbi12d ⊢ φ → ψ ⊻ θ ⊻ η ↔ χ ⊻ τ ⊻ ζ
6 df-had ⊢ hadd ψ θ η ↔ ψ ⊻ θ ⊻ η
7 df-had ⊢ hadd χ τ ζ ↔ χ ⊻ τ ⊻ ζ
8 5 6 7 3bitr4g ⊢ φ → hadd ψ θ η ↔ hadd χ τ ζ