Definition df-xor 1457

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 1478) and the constant false ⊥ (df-fal 1481), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1519), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1520), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1521), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1522). Contrast with ∧ (df-an 385), ∨ (df-or 384), → (wi 4), and ⊼ (df-nan 1440) . (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 1456	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 195	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 195	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1458  xorcom  1459  xorass  1460  excxor  1461  xor2  1462  xorneg2  1466  xorbi12i  1469  xorbi12d  1470  anxordi  1471  xorexmid  1472  truxortru  1519  truxorfal  1520  falxorfal  1522  hadbi  1528  sadadd2lem2  15010  f1omvdco3  17692  tsxo3  33116  tsxo4  33117  ifpxorxorb  36875  or3or  37339  axorbtnotaiffb  39719  axorbciffatcxorb  39721  aisbnaxb  39727  abnotbtaxb  39731  abnotataxb  39732