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 
|- ( ( ph \/_ ps ) <-> ( ps \/_ ph ) )

Proof

Step Hyp Ref Expression
1 df-xor 
 |-  ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
2 bicom 
 |-  ( ( ph <-> ps ) <-> ( ps <-> ph ) )
3 1 2 xchbinx 
 |-  ( ( ph \/_ ps ) <-> -. ( ps <-> ph ) )
4 df-xor 
 |-  ( ( ps \/_ ph ) <-> -. ( ps <-> ph ) )
5 3 4 bitr4i 
 |-  ( ( ph \/_ ps ) <-> ( ps \/_ ph ) )