MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xor Structured version   Visualization version   GIF version

Definition df-xor 1502
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 1539) and the constant false (df-fal 1549), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1581), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1582), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1583), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1584). Contrast with (df-an 399), (df-or 844), (wi 4), and (df-nan 1482). (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor ((𝜑𝜓) ↔ ¬ (𝜑𝜓))

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wxo 1501 . 2 wff (𝜑𝜓)
41, 2wb 208 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 208 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1503  xorcom  1504  xorcomOLD  1505  xorass  1506  excxor  1507  xor2  1508  xorneg2  1512  xorbi12i  1515  xorbi12iOLD  1516  xorbi12d  1517  anxordi  1518  xorexmid  1519  truxortru  1581  truxorfal  1582  falxorfal  1584  hadbi  1597  elsymdifxor  4229  sadadd2lem2  15802  f1omvdco3  18580  bj-bixor  33929  tsxo3  35421  tsxo4  35422  ifpxorxorb  39883  or3or  40377  axorbtnotaiffb  43146  axorbciffatcxorb  43148  aisbnaxb  43154  abnotbtaxb  43158  abnotataxb  43159  afv2orxorb  43434
  Copyright terms: Public domain W3C validator