Definition df-xor 1514

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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1587), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1588), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1589), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1590). Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and ⊼ (df-nan 1494). (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 1513	. 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  1515  xorcom  1516  xorass  1517  excxor  1518  xor2  1519  xorneg2  1523  xorbi12i  1526  xorbi12d  1527  anxordi  1528  xorexmid  1529  truxortru  1587  truxorfal  1588  falxorfal  1590  hadbi  1600  elsymdifxor  4200  sadadd2lem2  16419  f1omvdco3  19424  bj-bixor  36856  wl-df3xor2  37785  wl-3xorbi  37789  wl-2xor  37799  tsxo3  38460  tsxo4  38461  oneptri  43685  ifpxorxorb  43938  or3or  44450  axorbtnotaiffb  47351  axorbciffatcxorb  47353  aisbnaxb  47359  abnotbtaxb  47363  abnotataxb  47364  afv2orxorb  47676