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 1439
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 1477) and the constant false (df-fal 1480), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1514), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1515), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1516), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1517). Contrast with (df-an 384), (df-or 383), (wi 4), and (df-xor 1456) . (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 1438 . 2 wff (𝜑𝜓)
41, 2wa 382 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 194 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1440  nancom  1441  nannan  1442  nannot  1444  nanbi  1445  nanbi1  1446  xornan2  1464  trunanfal  1515  nic-mpALT  1587  nic-ax  1588  nic-axALT  1589  nfnan  1816  nfnanOLD  2220  naim1  31356  naim2  31357  df3nandALT1  31368  imnand2  31371  waj-ax  31385  lukshef-ax2  31386  arg-ax  31387  nandsym1  31393  wl-dfnan2  32274  tsna1  32920  tsna2  32921  tsna3  32922  ifpdfnan  36649  ifpnannanb  36670  nanorxor  37325  undisjrab  37326
  Copyright terms: Public domain W3C validator