Metamath Proof Explorer

Theorem cadbi123d

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

Ref Expression
Hypotheses cadbid.1 ⊢ φ → ψ ↔ χ
cadbid.2 ⊢ φ → θ ↔ τ
cadbid.3 ⊢ φ → η ↔ ζ
Assertion cadbi123d ⊢ φ → cadd ψ θ η ↔ cadd χ τ ζ

Proof

Step Hyp Ref Expression
1 cadbid.1 ⊢ φ → ψ ↔ χ
2 cadbid.2 ⊢ φ → θ ↔ τ
3 cadbid.3 ⊢ φ → η ↔ ζ
4 1 2 anbi12d ⊢ φ → ψ ∧ θ ↔ χ ∧ τ
5 1 2 xorbi12d ⊢ φ → ψ ⊻ θ ↔ χ ⊻ τ
6 3 5 anbi12d ⊢ φ → η ∧ ψ ⊻ θ ↔ ζ ∧ χ ⊻ τ
7 4 6 orbi12d ⊢ φ → ψ ∧ θ ∨ η ∧ ψ ⊻ θ ↔ χ ∧ τ ∨ ζ ∧ χ ⊻ τ
8 df-cad ⊢ cadd ψ θ η ↔ ψ ∧ θ ∨ η ∧ ψ ⊻ θ
9 df-cad ⊢ cadd χ τ ζ ↔ χ ∧ τ ∨ ζ ∧ χ ⊻ τ
10 7 8 9 3bitr4g ⊢ φ → cadd ψ θ η ↔ cadd χ τ ζ