Definition df-xor 1266

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 97), ∨ (wo 628), 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 1265	. 2 wff (φ ⊻ ψ)
4	1, 2	wo 628	. . 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  1267  xorbi2d  1269  xorbi1d  1270  xorbin  1272  xorcom  1276  xornbidc  1279  xordc1  1281  anxordi  1288  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  mpto2  1312  mtp-xor  1313  reapltxor  7325  bdxor  8890