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  8682  zeoxor  12255  odd2np1  12259  bdxor  15910  trirec0xor  16125