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 1476
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 1531) and the constant false (df-fal 1541), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1569), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1570), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1571), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1572). Contrast with (df-an 397), (df-or 842), (wi 4), and (df-xor 1496). (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 1475 . 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  1477  nanimn  1478  nanor  1479  nanbi  1484  xornan2  1504  trunanfal  1570  nic-mpALT  1664  nic-ax  1665  nic-axALT  1666  nfnan  1892  elnanel  9058  naim1  33634  naim2  33635  df3nandALT1  33644  imnand2  33647  waj-ax  33659  lukshef-ax2  33660  arg-ax  33661  nandsym1  33667  tsna1  35303  tsna2  35304  tsna3  35305  ifpdfnan  39730  ifpnannanb  39751  nanorxor  40514  undisjrab  40515
  Copyright terms: Public domain W3C validator