Metamath Proof Explorer

Theorem xor3

Description: Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006)

Ref Expression
Assertion xor3 
|- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )

Proof

Step Hyp Ref Expression
1 pm5.18 
 |-  ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) )
2 1 con2bii 
 |-  ( ( ph <-> -. ps ) <-> -. ( ph <-> ps ) )
3 2 bicomi 
 |-  ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )