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  1640  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  tbw-ax2  1701  merco1  1713  nftht  1792  ala1  1813  exa1  1838  ax13b  2031  sbi2  2302  ax12vALT  2474  moabs  2543  moa1  2551  r19.35  3108  r19.35OLD  3109  r19.21v  3180  r19.37  3262  r19.12OLD  3315  eqvincg  3648  rr19.3v  3667  class2seteq  3710  ralidmw  4508  ralidm  4512  dvdemo2  5374  iunopeqop  5526  po2ne  5608  asymref2  6137  elfv2ex  6952  elovmpt3imp  7690  sorpssuni  7752  dfwe2  7794  ordunisuc2  7865  xpord3ind  8181  smo11  8404  omex  9683  r111  9815  kmlem12  10202  squeeze0  12171  nn0ge2m1nn  12596  nn0lt10b  12680  iccneg  13512  hashfzp1  14470  hash2prde  14509  hash2pwpr  14515  hashge2el2dif  14519  hash3tpde  14532  relexprel  15078  algcvgblem  16614  prm23ge5  16853  cshwshashlem1  17133  dfgrp2e  18981  gsmtrcl  19534  nzerooringczr  21491  symgmatr01lem  22659  cxpcn2  26789  logbgcd1irr  26837  rpdmgm  27068  bpos1  27327  2lgs  27451  2sqnn0  27482  umgrislfupgrlem  29139  uhgr2edg  29225  nbusgrvtxm1  29396  uvtx01vtx  29414  g0wlk0  29670  wlkonl1iedg  29683  wlkreslem  29687  crctcshwlkn0lem5  29834  0enwwlksnge1  29884  clwwlknonex2lem2  30127  frgr3vlem2  30293  frgrnbnb  30312  frgrregord013  30414  frgrogt3nreg  30416  2bornot2b  30483  stcltr2i  32294  mdsl1i  32340  prsiga  34132  logdivsqrle  34665  bnj1533  34866  bnj1176  35019  jath  35725  idinside  36085  tb-ax2  36385  bj-a1k  36545  bj-peircestab  36554  bj-currypeirce  36558  bj-andnotim  36589  bj-ssbeq  36654  bj-eqs  36676  bj-nnftht  36742  curryset  36947  currysetlem3  36950  wl-moae  37517  tsim3  38139  mpobi123f  38169  mptbi12f  38173  ac6s6  38179  ax12fromc15  38906  axc5c7toc5  38913  axc5c711toc5  38920  ax12f  38941  ax12eq  38942  ax12el  38943  ax12indi  38945  ax12indalem  38946  ax12inda2ALT  38947  ax12inda2  38948  atpsubN  39755  ifpim23g  43508  rp-fakeimass  43525  inintabss  43591  ntrneiiso  44104  spALT  44214  axc5c4c711toc5  44421  axc5c4c711toc4  44422  axc5c4c711toc7  44423  axc5c4c711to11  44424  pm2.43bgbi  44537  pm2.43cbi  44538  hbimpg  44574  hbimpgVD  44924  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  dfbi1ALTa  44960  simprimi  44961  ralimralim  45086  confun  46951  confun5  46955  adh-jarrsc  47012  adh-minim  47013  adh-minimp  47025  f1cof1b  47089  iccpartnel  47425  fmtno4prmfac193  47560  prminf2  47575  zeo2ALTV  47658  fpprbasnn  47716  sbgoldbaltlem1  47766  elclnbgrelnbgr  47812  uspgrimprop  47873  islinindfis  48366  lindslinindsimp2lem5  48379  zlmodzxznm  48414