Definition df-xor 1366

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 103), ∨ (wo 698), 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 1365	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 698	. . 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  1367  xorbi2d  1370  xorbi1d  1371  xorbin  1374  xorcom  1378  xornbidc  1381  xordc1  1383  anxordi  1390  truxortru  1409  truxorfal  1410  falxortru  1411  falxorfal  1412  mptxor  1414  reapltxor  8487  zeoxor  11806  odd2np1  11810  bdxor  13718  trirec0xor  13924