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

Definition df-nan 1335
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 T. (df-tru 1373) and the constant false F. (df-fal 1376), we will be able to prove these truth table values:  ( ( T.  -/\ T.  )  <-> F.  ) (trunantru 1412), 
( ( T.  -/\ F.  )  <-> T.  ) (trunanfal 1413),  ( ( F.  -/\ T.  )  <-> T.  ) (falnantru 1414), and  ( ( F.  -/\ F.  )  <-> T.  ) (falnanfal 1415). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  \/_ (df-xor 1352) . (Contributed by Jeff Hoffman, 19-Nov-2007.)
Assertion
Ref Expression
df-nan  |-  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )

Detailed syntax breakdown of Definition df-nan
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wnan 1334 . 2  wff  ( ph  -/\ 
ps )
41, 2wa 369 . . 3  wff  ( ph  /\ 
ps )
54wn 3 . 2  wff  -.  ( ph  /\  ps )
63, 5wb 184 1  wff  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1336  nancom  1337  nannan  1338  nannot  1340  nanbi  1341  nanbi1  1342  xornan2  1360  trunanfal  1413  nic-mpALT  1480  nic-ax  1481  nic-axALT  1482  nfnan  1867  naim1  28376  naim2  28377  df3nandALT1  28388  imnand2  28391  waj-ax  28405  lukshef-ax2  28406  arg-ax  28407  nandsym1  28413  tsna1  29104  tsna2  29105  tsna3  29106
  Copyright terms: Public domain W3C validator