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, 30-Sep-1992.)
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 setvar class This axiom is referenced by:  a1i  11  id  22  id1  23  a1d  25  a1dd  46  jarr  98  pm2.86d  99  pm2.86i  101  pm2.51  153  dfbi1ALT  193  pm5.1im  238  biimt  335  pm5.4  362  pm4.8  365  olc  384  simpl  457  pm4.45im  562  pm2.64  789  pm2.74  846  pm2.82  852  oibabs  881  pm5.14  886  biort  896  dedlem0a  952  ifptru  1388  ifpfal  1389  meredith  1472  tbw-bijust  1531  tbw-negdf  1532  tbw-ax2  1534  merco1  1546  ala1  1660  exa1  1661  ax13b  1805  sbi2  2134  ax12vALT  2171  ax12  2234  axc5c7toc5  2242  axc5c711toc5  2249  ax12f  2270  ax12eq  2271  ax12el  2272  ax12indi  2274  ax12indalem  2275  ax12inda2ALT  2276  ax12inda2  2277  morimOLD  2341  morimvOLD  2342  euim  2344  r19.12  2983  r19.27v  2990  r19.37  3006  eqvinc  3226  rr19.3v  3241  class2seteq  4620  dvdemo2  4688  asymref2  5389  iotanul  5571  elovmpt3imp  6533  sorpssuni  6589  sorpssint  6590  dfwe2  6617  ordunisuc2  6679  tfindsg  6695  findsg  6727  smo11  7054  omex  8081  r111  8214  kmlem12  8562  domtriomlem  8843  ltlen  9707  squeeze0  10473  elnnnn0b  10865  nn0ge2m1nn  10886  nn0lt10b  10950  nn01to3  11204  iccneg  11670  ssnn0fi  12094  hash2prde  12516  hash2pwpr  12519  hashge2el2dif  12521  disjxwrd  12680  scshwfzeqfzo  12794  algcvgblem  14206  cshwshashlem1  14580  cshwshashlem2  14581  gsmtrcl  16541  prmirred  18525  prmirredOLD  18528  mamufacex  18891  mavmulsolcl  19053  symgmatr01lem  19155  pmatcollpw3fi1  19289  cxpcn2  23120  bpos1  23558  usgra2edg  24382  nbgra0nb  24429  nbcusgra  24463  wlkdvspthlem  24609  usgrcyclnl2  24641  4cycl4dv  24667  clwwlkgt0  24771  nbhashuvtx1  24915  rusgrasn  24945  frgra3vlem2  25001  frgranbnb  25020  frgrancvvdeqlem2  25031  frgrareg  25117  frgraregord013  25118  frgraogt3nreg  25120  2bornot2b  25172  stcltr2i  27194  mdsl1i  27240  eqvincg  27374  prsiga  28131  rpdmgm  28567  idinside  29734  tb-ax2  29845  wl-jarri  29969  a1i4  30114  tsim3  30539  mpt2bi123f  30571  mptbi12f  30575  ac6s6  30580  prtlem1  30584  axc5c4c711toc5  31309  axc5c4c711toc4  31310  axc5c4c711toc7  31311  axc5c4c711to11  31312  znnn0nn  31489  nzerooringczr  32880  suppmptcfin  32972  linc1  33026  islinindfis  33050  lindslinindsimp2lem5  33063  zlmodzxznm  33098  pm2.43bgbi  33287  pm2.43cbi  33288  hbimpg  33327  hbimpgVD  33704  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bnj1533  33910  bnj1176  34061  pm4.81ALT  34136  bj-imim2ALT  34167  bj-andnotim  34177  bj-nftht  34198  bj-stdpc4v  34334  bj-ax12v  34348  bj-dvdemo2  34389  atpsubN  35477  rp-fakeimass  37736
 Copyright terms: Public domain W3C validator