Definition df-xor 1252

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 97), ∨ (wo 616), 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 1251	. 2 wff (φ ⊻ ψ)
4	1, 2	wo 616	. . 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  1253  xorbi2d  1255  xorbi1d  1256  xorbin  1258  xorcom  1262  xornbidc  1265  xordc1  1267  anxordi  1274  truxortru  1293  truxorfal  1294  falxortru  1295  falxorfal  1296  mpto2  1298  mtp-xor  1299  bdxor  6412