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

Definition df-nan 1298
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 1329) and the constant false  F. (df-fal 1330), we will be able to prove these truth table values:  ( (  T.  -/\  T.  )  <->  F.  ) (trunantru 1364), 
( (  T.  -/\  F.  )  <->  T.  ) (trunanfal 1365),  ( (  F.  -/\  T.  )  <->  T.  ) (falnantru 1366), and  ( (  F.  -/\  F.  )  <->  T.  ) (falnanfal 1367). Contrast with  /\ (df-an 362), 
\/ (df-or 361), 
-> (wi 4), and  \/_ (df-xor 1315) . (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 1297 . 2  wff  ( ph  -/\ 
ps )
41, 2wa 360 . . 3  wff  ( ph  /\ 
ps )
54wn 3 . 2  wff  -.  ( ph  /\  ps )
63, 5wb 178 1  wff  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
This definition is referenced by:  nanan  1299  nancom  1300  nannan  1301  nannot  1303  nanbi  1304  nanbi1  1305  trunanfal  1365  nic-mpALT  1447  nic-ax  1448  nic-axALT  1449  nfnan  1848  naim1  26136  naim2  26137  df3nandALT1  26148  imnand2  26151  waj-ax  26166  lukshef-ax2  26167  arg-ax  26168  nandsym1  26174
  Copyright terms: Public domain W3C validator