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  4223  sadadd2lem2  16420  f1omvdco3  19379  bj-bixor  36579  wl-df3xor2  37457  wl-3xorbi  37461  wl-2xor  37471  tsxo3  38133  tsxo4  38134  oneptri  43246  ifpxorxorb  43500  or3or  44012  axorbtnotaiffb  46904  axorbciffatcxorb  46906  aisbnaxb  46912  abnotbtaxb  46916  abnotataxb  46917  afv2orxorb  47229