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 ( 𝜓 , 𝜑 , 𝜒 ) )