Definition df-xor 1313

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 103), \/ (wo 665), 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 1312	. 2 wff ( ph \/_ ps )
4	1, 2	wo 665	. . 3 wff ( ph \/ ps )
5	1, 2	wa 103	. . . 4 wff ( ph /\ ps )
6	5	wn 3	. . 3 wff -. ( ph /\ ps )
7	4, 6	wa 103	. 2 wff ( ( ph \/ ps ) /\ -. ( ph /\ ps ) )
8	3, 7	wb 104	1 wff ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )

This definition is referenced by:  xoranor  1314  xorbi2d  1317  xorbi1d  1318  xorbin  1321  xorcom  1325  xornbidc  1328  xordc1  1330  anxordi  1337  truxortru  1356  truxorfal  1357  falxortru  1358  falxorfal  1359  mptxor  1361  reapltxor  8127  zeoxor  11208  odd2np1  11212  bdxor  12000