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

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. . 3 wff 𝜓
3	2, 1	wi 4	. 2 wff (𝜓 → 𝜑)
4	1, 3	wi 4	1 wff (𝜑 → (𝜓 → 𝜑))

This axiom is referenced by:  a1i  11  id  22  idALT  23  a1d  25  a1dd  50  a1ddd  80  jarr  106  jarri  107  pm2.86d  108  conax1  170  dfbi1ALT  214  pm5.1im  263  biimt  360  pm4.8  392  pm4.45im  828  pm5.31r  832  jao1i  859  olc  869  oibabs  954  pm2.74  977  tarski-bernays-ax2  1642  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  tbw-ax2  1703  merco1  1715  nftht  1794  ala1  1815  exa1  1840  ax13b  2034  sbi2  2309  ax12vALT  2474  moabs  2544  moa1  2552  r19.35  3095  r19.21v  3162  r19.37  3240  eqvincg  3603  rr19.3v  3622  class2seteq  3663  r19.3rzv  4457  ralidmw  4470  ralidm  4471  dvdemo2  5320  iunopeqop  5470  po2ne  5549  asymref2  6075  elfv2ex  6878  elovmpt3imp  7617  sorpssuni  7679  dfwe2  7721  ordunisuc2  7788  xpord3ind  8100  smo11  8298  omex  9556  r111  9691  kmlem12  10076  squeeze0  12049  nn0ge2m1nn  12475  nn0lt10b  12558  iccneg  13392  hashfzp1  14358  hash2prde  14397  hash2pwpr  14403  hashge2el2dif  14407  hash3tpde  14420  relexprel  14966  algcvgblem  16508  prm23ge5  16747  cshwshashlem1  17027  dfgrp2e  18897  gsmtrcl  19449  nzerooringczr  21439  symgmatr01lem  22601  cxpcn2  26716  logbgcd1irr  26764  rpdmgm  26995  bpos1  27254  2lgs  27378  2sqnn0  27409  umgrislfupgrlem  29199  uhgr2edg  29285  nbusgrvtxm1  29456  uvtx01vtx  29474  g0wlk0  29728  wlkonl1iedg  29741  wlkreslem  29745  crctcshwlkn0lem5  29891  0enwwlksnge1  29941  clwwlknonex2lem2  30187  frgr3vlem2  30353  frgrnbnb  30372  frgrregord013  30474  frgrogt3nreg  30476  2bornot2b  30543  stcltr2i  32354  mdsl1i  32400  prsiga  34290  logdivsqrle  34809  bnj1533  35010  bnj1176  35163  onvf1odlem1  35299  jath  35921  idinside  36280  tb-ax2  36580  bj-a1k  36746  bj-peircestab  36755  bj-currypeirce  36759  bj-andnotim  36790  bj-ssbeq  36856  bj-eqs  36878  bj-nnftht  36944  curryset  37149  currysetlem3  37152  wl-moae  37723  tsim3  38335  mpobi123f  38365  mptbi12f  38369  ac6s6  38375  ax12fromc15  39233  axc5c7toc5  39240  axc5c711toc5  39247  ax12f  39268  ax12eq  39269  ax12el  39270  ax12indi  39272  ax12indalem  39273  ax12inda2ALT  39274  ax12inda2  39275  atpsubN  40081  ifpim23g  43803  rp-fakeimass  43820  inintabss  43886  ntrneiiso  44399  spALT  44509  axc5c4c711toc5  44710  axc5c4c711toc4  44711  axc5c4c711toc7  44712  axc5c4c711to11  44713  pm2.43bgbi  44825  pm2.43cbi  44826  hbimpg  44862  hbimpgVD  45211  ax6e2ndeqVD  45216  ax6e2ndeqALT  45238  dfbi1ALTa  45247  simprimi  45248  ralimralim  45393  confun  47252  confun5  47256  adh-jarrsc  47313  adh-minim  47314  adh-minimp  47326  f1cof1b  47390  iccpartnel  47751  fmtno4prmfac193  47886  prminf2  47901  zeo2ALTV  47984  fpprbasnn  48042  sbgoldbaltlem1  48092  elclnbgrelnbgr  48138  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  islinindfis  48762  lindslinindsimp2lem5  48775  zlmodzxznm  48810