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 1609
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 1656) and the constant false (df-fal 1666), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1694), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1695), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1696), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1697). Contrast with (df-an 385), (df-or 874), (wi 4), and (df-xor 1634). (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 1608 . 2 wff (𝜑𝜓)
41, 2wa 384 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 197 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1610  nanimn  1611  nanor  1612  nancomOLD  1614  nannanOLD  1616  nannotOLD  1619  nanbi  1620  nanbi1OLD  1622  xornan2  1642  trunanfal  1695  nic-mpALT  1767  nic-ax  1768  nic-axALT  1769  nfnan  1999  naim1  32830  naim2  32831  df3nandALT1  32840  imnand2  32843  waj-ax  32855  lukshef-ax2  32856  arg-ax  32857  nandsym1  32863  tsna1  34375  tsna2  34376  tsna3  34377  ifpdfnan  38510  ifpnannanb  38531  nanorxor  39181  undisjrab  39182
  Copyright terms: Public domain W3C validator