Metamath Proof Explorer

Theorem nbi2

Description: Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 24-Jan-2013)

Ref Expression
Assertion nbi2 
|- ( -. ( ph <-> ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 xor3 
 |-  ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
2 pm5.17 
 |-  ( ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) <-> ( ph <-> -. ps ) )
3 1 2 bitr4i 
 |-  ( -. ( ph <-> ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )