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  3096  r19.21v  3163  r19.37  3241  eqvincg  3591  rr19.3v  3610  class2seteq  3651  r19.3rzv  4444  ralidmw  4457  ralidm  4458  dvdemo2  5309  iunopeqop  5467  po2ne  5546  asymref2  6072  elfv2ex  6875  elovmpt3imp  7615  sorpssuni  7677  dfwe2  7719  ordunisuc2  7786  xpord3ind  8097  smo11  8295  omex  9553  r111  9688  kmlem12  10073  squeeze0  12046  nn0ge2m1nn  12472  nn0lt10b  12555  iccneg  13389  hashfzp1  14355  hash2prde  14394  hash2pwpr  14400  hashge2el2dif  14404  hash3tpde  14417  relexprel  14963  algcvgblem  16505  prm23ge5  16744  cshwshashlem1  17024  dfgrp2e  18897  gsmtrcl  19449  nzerooringczr  21437  symgmatr01lem  22596  cxpcn2  26696  logbgcd1irr  26744  rpdmgm  26975  bpos1  27234  2lgs  27358  2sqnn0  27389  umgrislfupgrlem  29179  uhgr2edg  29265  nbusgrvtxm1  29436  uvtx01vtx  29454  g0wlk0  29708  wlkonl1iedg  29721  wlkreslem  29725  crctcshwlkn0lem5  29871  0enwwlksnge1  29921  clwwlknonex2lem2  30167  frgr3vlem2  30333  frgrnbnb  30352  frgrregord013  30454  frgrogt3nreg  30456  2bornot2b  30523  stcltr2i  32335  mdsl1i  32381  prsiga  34281  logdivsqrle  34800  bnj1533  35000  bnj1176  35153  axprALT2  35259  onvf1odlem1  35291  jath  35913  idinside  36272  tb-ax2  36572  bj-a1k  36802  bj-peircestab  36813  bj-currypeirce  36819  bj-andnotim  36851  bj-ssbeq  36945  bj-eqs  36968  bj-alnnf  37032  curryset  37251  currysetlem3  37254  wl-moae  37832  tsim3  38444  mpobi123f  38474  mptbi12f  38478  ac6s6  38484  ax12fromc15  39342  axc5c7toc5  39349  axc5c711toc5  39356  ax12f  39377  ax12eq  39378  ax12el  39379  ax12indi  39381  ax12indalem  39382  ax12inda2ALT  39383  ax12inda2  39384  atpsubN  40190  ifpim23g  43925  rp-fakeimass  43942  inintabss  44008  ntrneiiso  44521  spALT  44631  axc5c4c711toc5  44832  axc5c4c711toc4  44833  axc5c4c711toc7  44834  axc5c4c711to11  44835  pm2.43bgbi  44947  pm2.43cbi  44948  hbimpg  44984  hbimpgVD  45333  ax6e2ndeqVD  45338  ax6e2ndeqALT  45360  dfbi1ALTa  45369  simprimi  45370  ralimralim  45515  confun  47373  confun5  47377  adh-jarrsc  47434  adh-minim  47435  adh-minimp  47447  f1cof1b  47511  iccpartnel  47872  fmtno4prmfac193  48007  prminf2  48022  zeo2ALTV  48105  fpprbasnn  48163  sbgoldbaltlem1  48213  elclnbgrelnbgr  48259  pgnbgreunbgrlem2lem1  48548  pgnbgreunbgrlem2lem2  48549  pgnbgreunbgrlem2lem3  48550  islinindfis  48883  lindslinindsimp2lem5  48896  zlmodzxznm  48931