Definition df-xor 1387

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 104), ∨ (wo 709), 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 1386	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 709	. . 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  1388  xorbi2d  1391  xorbi1d  1392  xorbin  1395  xorcom  1399  xornbidc  1402  xordc1  1404  anxordi  1411  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  mptxor  1435  reapltxor  8633  zeoxor  12051  odd2np1  12055  bdxor  15566  trirec0xor  15776