Definition df-xor 1267

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 97), ∨ (wo 629), 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 1266	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wo 629	. . 3 wff (𝜑 ∨ 𝜓)
5	1, 2	wa 97	. . . 4 wff (𝜑 ∧ 𝜓)
6	5	wn 3	. . 3 wff ¬ (𝜑 ∧ 𝜓)
7	4, 6	wa 97	. 2 wff ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))
8	3, 7	wb 98	1 wff ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))

This definition is referenced by:  xoranor  1268  xorbi2d  1271  xorbi1d  1272  xorbin  1275  xorcom  1279  xornbidc  1282  xordc1  1284  anxordi  1291  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  mptxor  1315  reapltxor  7580  bdxor  9956