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

Definition df-nan 1344
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 1398) and the constant false (df-fal 1401), we will be able to prove these truth table values: (trunantru 1437), (trunanfal 1438), (falnantru 1439), and (falnanfal 1440). Contrast with /\ (df-an 371), \/ (df-or 370), -> (wi 4), and \/_ (df-xor 1364) . (Contributed by Jeff Hoffman, 19-Nov-2007.)
Assertion
Ref Expression
df-nan

Detailed syntax breakdown of Definition df-nan
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wnan 1343 . 2
41, 2wa 369 . . 3
54wn 3 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1345  nancom  1346  nancomOLD  1347  nannan  1348  nannanOLD  1349  nannot  1351  nanbi  1352  nanbiOLD  1353  nanbi1  1354  xornan2  1372  trunanfal  1438  nic-mpALT  1505  nic-ax  1506  nic-axALT  1507  nfnan  1929  naim1  29850  naim2  29851  df3nandALT1  29862  imnand2  29865  waj-ax  29879  lukshef-ax2  29880  arg-ax  29881  nandsym1  29887  tsna1  30551  tsna2  30552  tsna3  30553  nanorxor  31185  undisjrab  31186  bj-ifdfnan  37734  bj-ifnannanb  37735
  Copyright terms: Public domain W3C validator