Definition df-xor 1249

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 1248	. 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  1250  xorbi2d  1252  xorbi1d  1253  xorbin  1255  xorcom  1259  xornbidc  1262  xordc1  1264  anxordi  1271  truxortru  1290  truxorfal  1291  falxortru  1292  falxorfal  1293  mpto2  1295  mtp-xor  1296