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

Definition df-nan 1478
Description: Define incompatibility, or alternative denial ("not-and" or "nand"). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true (df-tru 1533) and the constant false (df-fal 1543), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1571), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1572), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1573), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1574). Contrast with (df-an 397), (df-or 844), (wi 4), and (df-xor 1498). (Contributed by Jeff Hoffman, 19-Nov-2007.)
Assertion
Ref Expression
df-nan ((𝜑𝜓) ↔ ¬ (𝜑𝜓))

Detailed syntax breakdown of Definition df-nan
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wnan 1477 . 2 wff (𝜑𝜓)
41, 2wa 396 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 207 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1479  nanimn  1480  nanor  1481  nanbi  1486  xornan2  1506  trunanfal  1572  nic-mpALT  1666  nic-ax  1667  nic-axALT  1668  nfnan  1894  elnanel  9062  naim1  33623  naim2  33624  df3nandALT1  33633  imnand2  33636  waj-ax  33648  lukshef-ax2  33649  arg-ax  33650  nandsym1  33656  tsna1  35292  tsna2  35293  tsna3  35294  ifpdfnan  39719  ifpnannanb  39740  nanorxor  40504  undisjrab  40505
  Copyright terms: Public domain W3C validator