Definition df-xor 1358

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 1357	. 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  1359  xorbi2d  1362  xorbi1d  1363  xorbin  1366  xorcom  1370  xornbidc  1373  xordc1  1375  anxordi  1382  truxortru  1401  truxorfal  1402  falxortru  1403  falxorfal  1404  mptxor  1406  reapltxor  8458  zeoxor  11752  odd2np1  11756  bdxor  13382  trirec0xor  13587