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

Definition df-nan 1294
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 1325) and the constant false  F. (df-fal 1326), we will be able to prove these truth table values:  ( (  T.  -/\  T.  )  <->  F.  ) (trunantru 1360), 
( (  T.  -/\  F.  )  <->  T.  ) (trunanfal 1361),  ( (  F.  -/\  T.  )  <->  T.  ) (falnantru 1362), and  ( (  F.  -/\  F.  )  <->  T.  ) (falnanfal 1363). Contrast with  /\ (df-an 361), 
\/ (df-or 360), 
-> (wi 4), and  \/_ (df-xor 1311) . (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 1293 . 2  wff  ( ph  -/\ 
ps )
41, 2wa 359 . . 3  wff  ( ph  /\ 
ps )
54wn 3 . 2  wff  -.  ( ph  /\  ps )
63, 5wb 177 1  wff  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
This definition is referenced by:  nanan  1295  nancom  1296  nannan  1297  nannot  1299  nanbi  1300  nanbi1  1301  trunanfal  1361  nic-mpALT  1443  nic-ax  1444  nic-axALT  1445  nfnan  1843  naim1  26038  naim2  26039  df3nandALT1  26050  imnand2  26053  waj-ax  26068  lukshef-ax2  26069  arg-ax  26070  nandsym1  26076
  Copyright terms: Public domain W3C validator