Definition df-xor 1366

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 103), \/ (wo 698), 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 1365	. 2 wff ( ph \/_ ps )
4	1, 2	wo 698	. . 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  1367  xorbi2d  1370  xorbi1d  1371  xorbin  1374  xorcom  1378  xornbidc  1381  xordc1  1383  anxordi  1390  truxortru  1409  truxorfal  1410  falxortru  1411  falxorfal  1412  mptxor  1414  reapltxor  8483  zeoxor  11802  odd2np1  11806  bdxor  13678  trirec0xor  13884