Metamath Proof Explorer


Theorem hadcoma

Description: Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 17-Dec-2023)

Ref Expression
Assertion hadcoma hadd φ ψ χ hadd ψ φ χ

Proof

Step Hyp Ref Expression
1 bicom φ ψ ψ φ
2 1 bibi1i φ ψ χ ψ φ χ
3 hadbi hadd φ ψ χ φ ψ χ
4 hadbi hadd ψ φ χ ψ φ χ
5 2 3 4 3bitr4i hadd φ ψ χ hadd ψ φ χ