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

Axiom ax-1 6
Description: Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. The 3 axioms are also given as Definition 2.1 of [Hamilton] p. 28. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of and to the assertion of simply." It is Proposition 1 of [Frege1879] p. 26, its first axiom. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-1

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2
2 wps . . 3
32, 1wi 4 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a1i  11  id  21  id1  22  a1d  24  a1dd  45  jarr  94  pm2.86i  95  pm2.86d  96  pm2.51  148  dfbi1gb  187  pm5.1im  231  biimt  327  pm5.4  353  pm4.8  356  olc  375  simpl  445  pm4.45im  547  pm2.64  766  pm2.74  821  pm2.82  827  oibabs  853  pm5.14  858  biort  868  dedlem0a  920  meredith  1424  tbw-bijust  1483  tbw-negdf  1484  tbw-ax2  1486  merco1  1498  ax13b  1717  ax12dgen  1744  19.38  1818  nfimdOLD  1834  hbimOLD  1842  a16gOLD  2055  stdpc4  2099  sbi2  2143  ax12v  2189  ax12  2265  axc5c7toc5  2273  axc5c711toc5  2280  ax12f  2301  ax12eq  2302  ax12el  2303  ax12indi  2305  ax12indalem  2306  ax12inda2ALT  2307  ax12inda2  2308  morimOLD  2374  morimvOLD  2375  euim  2377  alral  2818  r19.12  2873  r19.27av  2898  r19.37  2912  eqvinc  3125  rr19.3v  3139  class2seteq  4483  dvdemo2  4551  asymref2  5238  iotanul  5416  sorpssuni  6379  sorpssint  6380  dfwe2  6403  ordunisuc2  6465  tfindsg  6481  findsg  6513  smo11  6788  omex  7765  r111  7868  kmlem12  8212  fin1a2lem10  8460  domtriomlem  8493  ltlen  9355  squeeze0  10101  elnnnn0b  10490  iccneg  11268  hash2prde  12028  hash2pwpr  12031  disjxwrd  12196  algcvgblem  13599  cshwshashlem1  13969  cshwshashlem2  13970  prmirred  17400  gsmtrcl  17669  mamufacex  17760  mavmulsolcl  17832  symgmatr01lem  17933  cxpcn2  21650  bpos1  22088  usgra2edg  22423  nbgra0nb  22462  nbcusgra  22493  wlkdvspthlem  22628  usgrcyclnl2  22649  4cycl4dv  22675  2bornot2b  22779  stcltr2i  24801  mdsl1i  24847  eqvincg  24986  prsiga  25754  rpdmgm  26157  hbimtg  26773  idinside  27357  tb-ax2  27468  wl-jarri  27578  wl-equsal1t  27591  a1i4  27671  tsim3  28086  prtlem1  28132  axc5c4c711toc5  28830  axc5c4c711toc4  28831  axc5c4c711toc7  28832  axc5c4c711to11  28833  nn01to3  29366  clwwlkgt0  29615  scshwfzeqfzo  29673  nbhashuvtx1  29714  rusgrasn  29738  frgra3vlem2  29774  frgranbnb  29793  frgrancvvdeqlem2  29805  frgrareg  29891  frgraregord013  29892  frgraogt3nreg  29894  pm2.43bgbi  30067  pm2.43cbi  30068  hbimpg  30109  hbimpgVD  30486  a6e2ndeqVD  30491  a6e2ndeqALT  30513  bnj1533  30693  bnj1176  30844  bj-andnotim  30912  bj-alax1  30915  bj-equsal1t  30922  a16gNEW11  31098  stdpc4NEW11  31107  sbi2NEW11  31116  ax12vNEW11  31147  atpsubN  32100
  Copyright terms: Public domain W3C validator