Definition df-xor 1355

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 1354	. 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  1356  xorbi2d  1359  xorbi1d  1360  xorbin  1363  xorcom  1367  xornbidc  1370  xordc1  1372  anxordi  1379  truxortru  1398  truxorfal  1399  falxortru  1400  falxorfal  1401  mptxor  1403  reapltxor  8375  zeoxor  11602  odd2np1  11606  bdxor  13205  trirec0xor  13413