Definition df-xor 1418

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 104), \/ (wo 713), 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 1417	. 2 wff ( ph \/_ ps )
4	1, 2	wo 713	. . 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  1419  xorbi2d  1422  xorbi1d  1423  xorbin  1426  xorcom  1430  xornbidc  1433  xordc1  1435  anxordi  1442  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  mptxor  1466  reapltxor  8732  zeoxor  12375  odd2np1  12379  bdxor  16157  trirec0xor  16372