Metamath Proof Explorer


Theorem xorcom

Description: The connector \/_ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 21-Apr-2024)

Ref Expression
Assertion xorcom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-xor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
2 bicom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )
3 1 2 xchbinx ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜓𝜑 ) )
4 df-xor ( ( 𝜓𝜑 ) ↔ ¬ ( 𝜓𝜑 ) )
5 3 4 bitr4i ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )