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

Definition df-nan 1288
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 1310) and the constant false  F. (df-fal 1311), we will be able to prove these truth table values:  ( (  T.  -/\  T.  )  <->  F.  ) (trunantru 1344), 
( (  T.  -/\  F.  )  <->  T.  ) (trunanfal 1345),  ( (  F.  -/\  T.  )  <->  T.  ) (falnantru 1346), and  ( (  F.  -/\  F.  )  <->  T.  ) (falnanfal 1347). Contrast with  /\ (df-an 360), 
\/ (df-or 359), 
-> (wi 4), and  \/_ (df-xor 1296) . (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 1287 . 2  wff  ( ph  -/\ 
ps )
41, 2wa 358 . . 3  wff  ( ph  /\ 
ps )
54wn 3 . 2  wff  -.  ( ph  /\  ps )
63, 5wb 176 1  wff  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
This definition is referenced by:  nanan  1289  nancom  1290  nannan  1291  nannot  1293  nanbi  1294  trunanfal  1345  nic-mpALT  1427  nic-ax  1428  nic-axALT  1429  naim1  24895  naim2  24896  nabi1  24900  nabi2  24901  df3nandALT1  24907  imnand2  24910  waj-ax  24925  lukshef-ax2  24926  arg-ax  24927  nandsym1  24933
  Copyright terms: Public domain W3C validator