Definition df-xor 1337

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

This definition is referenced by:  xoranor  1338  xorbi2d  1341  xorbi1d  1342  xorbin  1345  xorcom  1349  xornbidc  1352  xordc1  1354  anxordi  1361  truxortru  1380  truxorfal  1381  falxortru  1382  falxorfal  1383  mptxor  1385  reapltxor  8269  zeoxor  11414  odd2np1  11418  bdxor  12726