Metamath Proof Explorer

Theorem cadcomb

Description: Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

Ref Expression
Assertion cadcomb ⊢ cadd φ ψ χ ↔ cadd φ χ ψ

Proof

Step Hyp Ref Expression
1 cadan ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
2 3ancoma ⊢ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ φ ∨ ψ ∧ ψ ∨ χ
3 orcom ⊢ ψ ∨ χ ↔ χ ∨ ψ
4 3 3anbi3i ⊢ φ ∨ χ ∧ φ ∨ ψ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ φ ∨ ψ ∧ χ ∨ ψ
5 1 2 4 3bitri ⊢ cadd φ ψ χ ↔ φ ∨ χ ∧ φ ∨ ψ ∧ χ ∨ ψ
6 cadan ⊢ cadd φ χ ψ ↔ φ ∨ χ ∧ φ ∨ ψ ∧ χ ∨ ψ
7 5 6 bitr4i ⊢ cadd φ ψ χ ↔ cadd φ χ ψ