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

Definition df-nan 1381
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 1441) and the constant false F. (df-fal 1444), we will be able to prove these truth table values:  ( ( T.  -/\ T.  )  <-> F.  ) (trunantru 1480), 
( ( T.  -/\ F.  )  <-> T.  ) (trunanfal 1481),  ( ( F.  -/\ T.  )  <-> T.  ) (falnantru 1483), and  ( ( F.  -/\ F.  )  <-> T.  ) (falnanfal 1484). Contrast with  /\ (df-an 373), 
\/ (df-or 372), 
-> (wi 4), and  \/_ (df-xor 1402) . (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 1380 . 2  wff  ( ph  -/\ 
ps )
41, 2wa 371 . . 3  wff  ( ph  /\ 
ps )
54wn 3 . 2  wff  -.  ( ph  /\  ps )
63, 5wb 188 1  wff  ( (
ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1382  nancom  1383  nancomOLD  1384  nannan  1385  nannanOLD  1386  nannot  1388  nanbi  1389  nanbiOLD  1390  nanbiOLDOLD  1391  nanbi1  1392  xornan2  1411  trunanfal  1481  trunanfalOLD  1482  nic-mpALT  1550  nic-ax  1551  nic-axALT  1552  nfnan  1990  naim1  31056  naim2  31057  df3nandALT1  31068  imnand2  31071  waj-ax  31085  lukshef-ax2  31086  arg-ax  31087  nandsym1  31093  wl-dfnan2  31821  tsna1  32356  tsna2  32357  tsna3  32358  ifpdfnan  36106  ifpnannanb  36127  nanorxor  36629  undisjrab  36630
  Copyright terms: Public domain W3C validator