Theorem xor 935

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

Assertion

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

Proof of Theorem xor

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386

This theorem is referenced by:  dfbi3OLD  995  pm5.24  996  4exmidOLD  998  excxor  1469  elsymdif  3849  symdif2  3852  rpnnen2lem12  14954  ist0-3  21149  eliuniincex  39292  eliincex  39293  abnotataxb  41083  ldepslinc  42298