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 φ χ ψ