Metamath Proof Explorer

Theorem cadcoma

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

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

Proof

Step Hyp Ref Expression
1 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
2 xorcom ⊢ φ ⊻ ψ ↔ ψ ⊻ φ
3 2 anbi2i ⊢ χ ∧ φ ⊻ ψ ↔ χ ∧ ψ ⊻ φ
4 1 3 orbi12i ⊢ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ ↔ ψ ∧ φ ∨ χ ∧ ψ ⊻ φ
5 df-cad ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ
6 df-cad ⊢ cadd ψ φ χ ↔ ψ ∧ φ ∨ χ ∧ ψ ⊻ φ
7 4 5 6 3bitr4i ⊢ cadd φ ψ χ ↔ cadd ψ φ χ