Definition df-xor 1376

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 104), \/ (wo 708), 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 1375	. 2 wff ( ph \/_ ps )
4	1, 2	wo 708	. . 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  1377  xorbi2d  1380  xorbi1d  1381  xorbin  1384  xorcom  1388  xornbidc  1391  xordc1  1393  anxordi  1400  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  mptxor  1424  reapltxor  8540  zeoxor  11864  odd2np1  11868  bdxor  14359  trirec0xor  14564