Definition df-xor 1418

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 104), ∨ (wo 713), 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 1417	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 713	. . 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  1419  xorbi2d  1422  xorbi1d  1423  xorbin  1426  xorcom  1430  xornbidc  1433  xordc1  1435  anxordi  1442  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  mptxor  1466  reapltxor  8752  zeoxor  12401  odd2np1  12405  bdxor  16308  trirec0xor  16527