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  2308  ax12vALT  2472  moabs  2542  moa1  2550  r19.35  3093  r19.21v  3160  r19.37  3238  eqvincg  3588  rr19.3v  3607  class2seteq  3647  r19.3rzv  4433  ralidmw  4446  ralidm  4447  dvdemo2  5305  iunopeqop  5464  iunopeqopOLD  5465  po2ne  5544  asymref2  6069  elfv2ex  6872  elovmpt3imp  7613  sorpssuni  7675  dfwe2  7717  ordunisuc2  7784  xpord3ind  8095  smo11  8293  omex  9553  r111  9688  kmlem12  10073  squeeze0  12048  nn0ge2m1nn  12496  nn0lt10b  12580  iccneg  13414  hashfzp1  14382  hash2prde  14421  hash2pwpr  14427  hashge2el2dif  14431  hash3tpde  14444  relexprel  14990  algcvgblem  16535  prm23ge5  16775  cshwshashlem1  17055  dfgrp2e  18928  gsmtrcl  19480  nzerooringczr  21449  symgmatr01lem  22606  cxpcn2  26698  logbgcd1irr  26746  rpdmgm  26976  bpos1  27234  2lgs  27358  2sqnn0  27389  umgrislfupgrlem  29179  uhgr2edg  29265  nbusgrvtxm1  29436  uvtx01vtx  29454  g0wlk0  29707  wlkonl1iedg  29720  wlkreslem  29724  crctcshwlkn0lem5  29870  0enwwlksnge1  29920  clwwlknonex2lem2  30166  frgr3vlem2  30332  frgrnbnb  30351  frgrregord013  30453  frgrogt3nreg  30455  2bornot2b  30522  stcltr2i  32334  mdsl1i  32380  prsiga  34263  logdivsqrle  34782  bnj1533  34982  bnj1176  35135  axprALT2  35241  onvf1odlem1  35273  jath  35895  idinside  36254  tb-ax2  36554  bj-a1k  36792  bj-peircestab  36803  bj-currypeirce  36809  bj-andnotim  36841  bj-ssbeq  36935  bj-eqs  36958  bj-alnnf  37022  curryset  37241  currysetlem3  37244  wl-moae  37829  tsim3  38441  mpobi123f  38471  mptbi12f  38475  ac6s6  38481  ax12fromc15  39339  axc5c7toc5  39346  axc5c711toc5  39353  ax12f  39374  ax12eq  39375  ax12el  39376  ax12indi  39378  ax12indalem  39379  ax12inda2ALT  39380  ax12inda2  39381  atpsubN  40187  ifpim23g  43910  rp-fakeimass  43927  inintabss  43993  ntrneiiso  44506  spALT  44616  axc5c4c711toc5  44817  axc5c4c711toc4  44818  axc5c4c711toc7  44819  axc5c4c711to11  44820  pm2.43bgbi  44932  pm2.43cbi  44933  hbimpg  44969  hbimpgVD  45318  ax6e2ndeqVD  45323  ax6e2ndeqALT  45345  dfbi1ALTa  45354  simprimi  45355  ralimralim  45500  confun  47375  confun5  47379  adh-jarrsc  47436  adh-minim  47437  adh-minimp  47449  f1cof1b  47513  iccpartnel  47886  fmtno4prmfac193  48024  prminf2  48039  zeo2ALTV  48135  fpprbasnn  48193  sbgoldbaltlem1  48243  elclnbgrelnbgr  48289  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  pgnbgreunbgrlem2lem3  48580  islinindfis  48913  lindslinindsimp2lem5  48926  zlmodzxznm  48961