MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nan Structured version   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 T. (df-tru 1382) and the constant false F. (df-fal 1385), we will be able to prove these truth table values:  ( ( T.  -/\ T.  )  <-> F.  ) (trunantru 1421), 
( ( T.  -/\ F.  )  <-> T.  ) (trunanfal 1422),  ( ( F.  -/\ T.  )  <-> T.  ) (falnantru 1423), and  ( ( F.  -/\ F.  )  <-> T.  ) (falnanfal 1424). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  \/_ (df-xor 1361) . (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 1343 . 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  1345  nancom  1346  nannan  1347  nannot  1349  nanbi  1350  nanbi1  1351  xornan2  1369  trunanfal  1422  nic-mpALT  1489  nic-ax  1490  nic-axALT  1491  nfnan  1876  naim1  29703  naim2  29704  df3nandALT1  29715  imnand2  29718  waj-ax  29732  lukshef-ax2  29733  arg-ax  29734  nandsym1  29740  tsna1  30382  tsna2  30383  tsna3  30384
  Copyright terms: Public domain W3C validator