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

Definition df-nan 1483
 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 1541) and the constant false ⊥ (df-fal 1551), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1579), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1580), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1581), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1582). Contrast with ∧ (df-an 400), ∨ (df-or 845), → (wi 4), and ⊻ (df-xor 1503). (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 1482 . 2 wff (𝜑𝜓)
41, 2wa 399 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 209 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class This definition is referenced by:  nanan  1484  nanimn  1485  nanor  1486  nanbi  1491  xornan2  1512  trunanfal  1580  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfnan  1901  elnanel  9108  naim1  34153  naim2  34154  df3nandALT1  34163  imnand2  34166  waj-ax  34178  lukshef-ax2  34179  arg-ax  34180  nandsym1  34186  tsna1  35888  tsna2  35889  tsna3  35890  ifpdfnan  40595  ifpnannanb  40616  nanorxor  41410  undisjrab  41411
 Copyright terms: Public domain W3C validator