Definition df-xor 1425

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 104), ∨ (wo 720), 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 1424	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 720	. . 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 used by:  xoranor  1426  xorbi2d  1429  xorbi1d  1430  xorbin  1433  xorcom  1437  xornbidc  1440  xordc1  1442  anxordi  1449  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  mptxor  1473  reapltxor  8919  zeoxor  12652  odd2np1  12656  bdxor  16981  trirec0xor  17213