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χτζ