Definition df-xor 1396

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 104), \/ (wo 710), and -> (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.)

Assertion

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

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wxo 1395	. 2 wff ( ph \/_ ps )
4	1, 2	wo 710	. . 3 wff ( ph \/ ps )
5	1, 2	wa 104	. . . 4 wff ( ph /\ ps )
6	5	wn 3	. . 3 wff -. ( ph /\ ps )
7	4, 6	wa 104	. 2 wff ( ( ph \/ ps ) /\ -. ( ph /\ ps ) )
8	3, 7	wb 105	1 wff ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )

This definition is referenced by:  xoranor  1397  xorbi2d  1400  xorbi1d  1401  xorbin  1404  xorcom  1408  xornbidc  1411  xordc1  1413  anxordi  1420  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  mptxor  1444  reapltxor  8697  zeoxor  12295  odd2np1  12299  bdxor  15971  trirec0xor  16186