Definition df-xor 1354

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 103), \/ (wo 697), 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 1353	. 2 wff ( ph \/_ ps )
4	1, 2	wo 697	. . 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  1355  xorbi2d  1358  xorbi1d  1359  xorbin  1362  xorcom  1366  xornbidc  1369  xordc1  1371  anxordi  1378  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  mptxor  1402  reapltxor  8344  zeoxor  11555  odd2np1  11559  bdxor  13023