Metamath Proof Explorer


Theorem wl-3xorcoma

Description: Commutative law for triple xor. Copy of hadcoma . (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 17-Dec-2023)

Ref Expression
Assertion wl-3xorcoma hadd φ ψ χ hadd ψ φ χ

Proof

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