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

Metamath Proof Explorer

Theorem xor

Description: Two ways to express exclusive disjunction ( df-xor ). Theorem *5.22 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 22-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 iman 
 |-  ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
2 iman 
 |-  ( ( ps -> ph ) <-> -. ( ps /\ -. ph ) )
3 1 2 anbi12i 
 |-  ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( -. ( ph /\ -. ps ) /\ -. ( ps /\ -. ph ) ) )
4 dfbi2 
 |-  ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
5 ioran 
 |-  ( -. ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) <-> ( -. ( ph /\ -. ps ) /\ -. ( ps /\ -. ph ) ) )
6 3 4 5 3bitr4ri 
 |-  ( -. ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) <-> ( ph <-> ps ) )
7 6 con1bii 
 |-  ( -. ( ph <-> ps ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )