Definition df-xor 1307

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 102), ∨ (wo 661), 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 1306	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 661	. . 3 wff (𝜑 ∨ 𝜓)
5	1, 2	wa 102	. . . 4 wff (𝜑 ∧ 𝜓)
6	5	wn 3	. . 3 wff ¬ (𝜑 ∧ 𝜓)
7	4, 6	wa 102	. 2 wff ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))
8	3, 7	wb 103	1 wff ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))

This definition is referenced by:  xoranor  1308  xorbi2d  1311  xorbi1d  1312  xorbin  1315  xorcom  1319  xornbidc  1322  xordc1  1324  anxordi  1331  truxortru  1350  truxorfal  1351  falxortru  1352  falxorfal  1353  mptxor  1355  reapltxor  7689  zeoxor  10268  odd2np1  10272  bdxor  10627