Definition df-xor 1421

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 104), ∨ (wo 716), and → (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.)

Assertion

Ref	Expression
df-xor	⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wxo 1420	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 716	. . 3 wff (𝜑 ∨ 𝜓)
5	1, 2	wa 104	. . . 4 wff (𝜑 ∧ 𝜓)
6	5	wn 3	. . 3 wff ¬ (𝜑 ∧ 𝜓)
7	4, 6	wa 104	. 2 wff ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))
8	3, 7	wb 105	1 wff ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))

This definition is referenced by:  xoranor  1422  xorbi2d  1425  xorbi1d  1426  xorbin  1429  xorcom  1433  xornbidc  1436  xordc1  1438  anxordi  1445  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  mptxor  1469  reapltxor  8859  zeoxor  12548  odd2np1  12552  bdxor  16593  trirec0xor  16816