Definition df-xor 1425

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 104), \/ (wo 720), 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 1424	. 2 wff ( ph \/_ ps )
4	1, 2	wo 720	. . 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 used by:  xoranor  1426  xorbi2d  1429  xorbi1d  1430  xorbin  1433  xorcom  1437  xornbidc  1440  xordc1  1442  anxordi  1449  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  mptxor  1473  reapltxor  8917  zeoxor  12636  odd2np1  12640  bdxor  16862  trirec0xor  17094