Definition df-xor 1425

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 104), \/ (wo 720), 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 1424	. 2 wff ( ph \/_ ps )
4	1, 2	wo 720	. . 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  1426  xorbi2d  1429  xorbi1d  1430  xorbin  1433  xorcom  1437  xornbidc  1440  xordc1  1442  anxordi  1449  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  mptxor  1473  reapltxor  8907  zeoxor  12614  odd2np1  12618  bdxor  16776  trirec0xor  16999