Definition df-xor 1398

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 104), ∨ (wo 712), 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 1397	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 712	. . 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  1399  xorbi2d  1402  xorbi1d  1403  xorbin  1406  xorcom  1410  xornbidc  1413  xordc1  1415  anxordi  1422  truxortru  1441  truxorfal  1442  falxortru  1443  falxorfal  1444  mptxor  1446  reapltxor  8704  zeoxor  12346  odd2np1  12350  bdxor  16109  trirec0xor  16324