Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1 Structured version   Visualization version   GIF 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 wff 𝜑
2 wps . . 3 wff 𝜓
32, 1wi 4 . 2 wff (𝜓𝜑)
41, 3wi 4 1 wff (𝜑 → (𝜓𝜑))
 Colors of variables: wff setvar class This axiom is referenced by:  a1i  11  id  22  idALT  23  a1d  25  a1dd  47  a1ddd  77  jarr  103  pm2.86d  104  pm2.86i  106  pm2.51  163  dfbi1ALT  202  pm5.1im  251  biimt  348  pm5.4  375  pm4.8  378  olc  397  simpl  471  pm4.45im  582  jao1i  820  pm2.64  825  pm2.74  886  pm2.82  892  oibabs  920  pm5.14  925  biort  935  dedlem0a  990  meredith  1556  tbw-bijust  1613  tbw-negdf  1614  tbw-ax2  1616  merco1  1628  ala1  1743  exa1  1744  ax13b  1914  ax12OLD  2233  sbi2  2285  ax12vALT  2320  moa1  2413  euim  2415  r19.12  2949  r19.27v  2956  r19.37  2971  eqvinc  3204  rr19.3v  3218  invdisjrab  4470  class2seteq  4658  dvdemo2  4729  asymref2  5323  iotanul  5668  elfv2ex  6022  elovmpt3imp  6663  sorpssuni  6719  sorpssint  6720  dfwe2  6748  ordunisuc2  6811  tfindsg  6827  findsg  6860  smo11  7223  omex  8298  r111  8396  kmlem12  8741  ltlen  9888  squeeze0  10675  elnnnn0b  11091  nn0ge2m1nn  11114  nn0lt10b  11179  znnn0nn  11228  iccneg  12032  hashfzp1  12941  hash2prde  12972  hash2pwpr  12976  hashge2el2dif  12978  scshwfzeqfzo  13280  relexprel  13484  nn0enne  14799  algcvgblem  15002  prm23ge5  15240  prmgaplem5  15479  prmgaplem6  15480  cshwshashlem1  15522  dfgrp2e  17161  gsmtrcl  17649  prmirred  19566  symgmatr01lem  20179  pmatcollpw3fi1  20313  cxpcn2  24175  rpdmgm  24439  bpos1  24698  2lgs  24822  usgra2edg  25650  nbgra0nb  25697  wlkdvspthlem  25876  usgrcyclnl2  25908  4cycl4dv  25934  nbhashuvtx1  26181  rusgrasn  26211  frgra3vlem2  26267  frgranbnb  26286  frgrancvvdeqlem2  26297  frgraregord013  26384  frgraogt3nreg  26386  2bornot2b  26451  stcltr2i  28307  mdsl1i  28353  eqvincg  28487  prsiga  29318  bnj1533  30022  bnj1176  30173  idinside  31197  tb-ax2  31384  bj-a1k  31540  bj-imim2ALT  31543  pm4.81ALT  31551  bj-andnotim  31581  bj-nftht  31604  bj-ssbeq  31651  bj-ssb0  31652  bj-ssb1a  31656  bj-eqs  31685  bj-stdpc4v  31780  bj-ax12v  31794  bj-dvdemo2  31833  wl-nftht0  32303  wl-jarri  32341  tsim3  32984  mpt2bi123f  33016  mptbi12f  33020  ac6s6  33025  ax12fromc15  33083  axc5c7toc5  33090  axc5c711toc5  33097  ax12f  33118  ax12eq  33119  ax12el  33120  ax12indi  33122  ax12indalem  33123  ax12inda2ALT  33124  ax12inda2  33125  atpsubN  33932  ifpim23g  36741  rp-fakeimass  36758  inintabss  36785  ntrneiiso  37291  axc5c4c711toc5  37507  axc5c4c711toc4  37508  axc5c4c711toc7  37509  axc5c4c711to11  37510  pm2.43bgbi  37626  pm2.43cbi  37627  hbimpg  37673  hbimpgVD  38044  ax6e2ndeqVD  38049  ax6e2ndeqALT  38071  ralimralim  38162  confun  39649  confun5  39653  iccpartnel  39871  fmtno4prmfac193  39918  prminf2  39933  zeo2ALTV  40015  sgoldbaltlem1  40096  iunopeqop  40221  umgrislfupgrlem  40439  uhgr2edg  40527  nbusgrvtxm1  40699  uvtxa01vtx0  40715  g01wlk0  40952  wlkOnl1iedg  40965  1wlkreslem  40970  crctcsh1wlkn0lem5  41109  0enwwlksnge1  41152  frgr3vlem2  41536  frgrnbnb  41555  frgrncvvdeqlem2  41562  av-frgraregord013  41641  av-frgraogt3nreg  41643  nzerooringczr  41956  islinindfis  42124  lindslinindsimp2lem5  42137  zlmodzxznm  42172
 Copyright terms: Public domain W3C validator