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  827  pm5.31r  831  jao1i  858  olc  868  oibabs  953  pm2.74  976  tarski-bernays-ax2  1640  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  tbw-ax2  1701  merco1  1713  nftht  1792  ala1  1813  exa1  1838  ax13b  2032  sbi2  2302  ax12vALT  2467  moabs  2536  moa1  2544  r19.35  3088  r19.35OLD  3089  r19.21v  3158  r19.37  3240  eqvincg  3614  rr19.3v  3633  class2seteq  3675  ralidmw  4471  ralidm  4475  dvdemo2  5329  iunopeqop  5481  po2ne  5562  asymref2  6090  elfv2ex  6904  elovmpt3imp  7646  sorpssuni  7708  dfwe2  7750  ordunisuc2  7820  xpord3ind  8135  smo11  8333  omex  9596  r111  9728  kmlem12  10115  squeeze0  12086  nn0ge2m1nn  12512  nn0lt10b  12596  iccneg  13433  hashfzp1  14396  hash2prde  14435  hash2pwpr  14441  hashge2el2dif  14445  hash3tpde  14458  relexprel  15005  algcvgblem  16547  prm23ge5  16786  cshwshashlem1  17066  dfgrp2e  18895  gsmtrcl  19446  nzerooringczr  21390  symgmatr01lem  22540  cxpcn2  26656  logbgcd1irr  26704  rpdmgm  26935  bpos1  27194  2lgs  27318  2sqnn0  27349  umgrislfupgrlem  29049  uhgr2edg  29135  nbusgrvtxm1  29306  uvtx01vtx  29324  g0wlk0  29580  wlkonl1iedg  29593  wlkreslem  29597  crctcshwlkn0lem5  29744  0enwwlksnge1  29794  clwwlknonex2lem2  30037  frgr3vlem2  30203  frgrnbnb  30222  frgrregord013  30324  frgrogt3nreg  30326  2bornot2b  30393  stcltr2i  32204  mdsl1i  32250  prsiga  34121  logdivsqrle  34641  bnj1533  34842  bnj1176  34995  onvf1odlem1  35090  jath  35712  idinside  36072  tb-ax2  36372  bj-a1k  36532  bj-peircestab  36541  bj-currypeirce  36545  bj-andnotim  36576  bj-ssbeq  36641  bj-eqs  36663  bj-nnftht  36729  curryset  36934  currysetlem3  36937  wl-moae  37504  tsim3  38126  mpobi123f  38156  mptbi12f  38160  ac6s6  38166  ax12fromc15  38898  axc5c7toc5  38905  axc5c711toc5  38912  ax12f  38933  ax12eq  38934  ax12el  38935  ax12indi  38937  ax12indalem  38938  ax12inda2ALT  38939  ax12inda2  38940  atpsubN  39747  ifpim23g  43484  rp-fakeimass  43501  inintabss  43567  ntrneiiso  44080  spALT  44190  axc5c4c711toc5  44391  axc5c4c711toc4  44392  axc5c4c711toc7  44393  axc5c4c711to11  44394  pm2.43bgbi  44507  pm2.43cbi  44508  hbimpg  44544  hbimpgVD  44893  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  dfbi1ALTa  44929  simprimi  44930  ralimralim  45075  confun  46940  confun5  46944  adh-jarrsc  47001  adh-minim  47002  adh-minimp  47014  f1cof1b  47078  iccpartnel  47439  fmtno4prmfac193  47574  prminf2  47589  zeo2ALTV  47672  fpprbasnn  47730  sbgoldbaltlem1  47780  elclnbgrelnbgr  47826  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  islinindfis  48438  lindslinindsimp2lem5  48451  zlmodzxznm  48486