Definition df-xor 1512

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 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1585), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1586), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1587), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1588). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1492). (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 1511	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1513  xorcom  1514  xorass  1515  excxor  1516  xor2  1517  xorneg2  1521  xorbi12i  1524  xorbi12d  1525  anxordi  1526  xorexmid  1527  truxortru  1585  truxorfal  1586  falxorfal  1588  hadbi  1598  elsymdifxor  4226  sadadd2lem2  16427  f1omvdco3  19386  bj-bixor  36586  wl-df3xor2  37464  wl-3xorbi  37468  wl-2xor  37478  tsxo3  38140  tsxo4  38141  oneptri  43253  ifpxorxorb  43507  or3or  44019  axorbtnotaiffb  46908  axorbciffatcxorb  46910  aisbnaxb  46916  abnotbtaxb  46920  abnotataxb  46921  afv2orxorb  47233