Definition df-xor 1371

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 103), ∨ (wo 703), 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 1370	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 703	. . 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  1372  xorbi2d  1375  xorbi1d  1376  xorbin  1379  xorcom  1383  xornbidc  1386  xordc1  1388  anxordi  1395  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  mptxor  1419  reapltxor  8508  zeoxor  11828  odd2np1  11832  bdxor  13871  trirec0xor  14077