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 1446
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 1484) and the constant false (df-fal 1487), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1522), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1523), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1524), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1525). Contrast with (df-an 386), (df-or 385), (wi 4), and (df-xor 1463) . (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 1445 . 2 wff (𝜑𝜓)
41, 2wa 384 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 196 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1447  nancom  1448  nannan  1449  nannot  1451  nanbi  1452  nanbi1  1453  xornan2  1471  trunanfal  1523  nic-mpALT  1595  nic-ax  1596  nic-axALT  1597  nfnan  1828  nfnanOLD  2236  naim1  32359  naim2  32360  df3nandALT1  32371  imnand2  32374  waj-ax  32388  lukshef-ax2  32389  arg-ax  32390  nandsym1  32396  wl-dfnan2  33267  tsna1  33922  tsna2  33923  tsna3  33924  ifpdfnan  37650  ifpnannanb  37671  nanorxor  38324  undisjrab  38325
  Copyright terms: Public domain W3C validator