Definition df-xor 1305

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊻ ⊤ ) ↔ ⊥ ) (truxortru 1358), (( ⊤ ⊻ ⊥ ) ↔ ⊤ ) (truxorfal 1359), (( ⊥ ⊻ ⊤ ) ↔ ⊤ ) (falxortru 1360), and (( ⊥ ⊻ ⊥ ) ↔ ⊥ ) (falxorfal 1361). Contrast with ∧ (df-an 360), ∨ (df-or 359), → (wi 4), and ⊼ (df-nan 1288) . (Contributed by FL, 22-Nov-2010.)

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 1304	. 2 wff (φ ⊻ ψ)
4	1, 2	wb 176	. . 3 wff (φ ↔ ψ)
5	4	wn 3	. 2 wff ¬ (φ ↔ ψ)
6	3, 5	wb 176	1 wff ((φ ⊻ ψ) ↔ ¬ (φ ↔ ψ))

This definition is referenced by:  xnor  1306  xorcom  1307  xorass  1308  excxor  1309  xor2  1310  xorneg1  1311  xorbi12i  1314  xorbi12d  1315  truxortru  1358  truxorfal  1359  falxortru  1360  falxorfal  1361  hadbi  1387  had0  1403  mpto2  1534  mpto2OLD  1535  mtp-xorOLD  1537