This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ⊻ ψ ↔ ψ ⊻ φ