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  213  pm5.1im  263  biimt  361  pm4.8  394  pm4.45im  827  pm5.31r  831  jao1i  857  olc  867  oibabs  951  pm2.74  974  tarski-bernays-ax2  1643  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  tbw-ax2  1704  merco1  1716  nftht  1795  ala1  1816  exa1  1841  ax13b  2036  sbi2  2299  ax12vALT  2469  moabs  2538  moa1  2546  r19.35  3109  r19.35OLD  3110  r19.21v  3180  r19.37  3260  r19.12OLD  3313  eqvincg  3635  rr19.3v  3656  class2seteq  3699  ss2abdv  4059  ralidmw  4506  ralidm  4510  invdisjrab  5133  dvdemo2  5371  iunopeqop  5520  po2ne  5603  asymref2  6115  elfv2ex  6934  elovmpt3imp  7658  sorpssuni  7717  dfwe2  7756  ordunisuc2  7828  xpord3ind  8137  smo11  8359  omex  9634  r111  9766  kmlem12  10152  squeeze0  12113  nn0ge2m1nn  12537  nn0lt10b  12620  iccneg  13445  hashfzp1  14387  hash2prde  14427  hash2pwpr  14433  hashge2el2dif  14437  relexprel  14982  algcvgblem  16510  prm23ge5  16744  cshwshashlem1  17025  dfgrp2e  18844  gsmtrcl  19377  symgmatr01lem  22137  cxpcn2  26234  logbgcd1irr  26279  rpdmgm  26509  bpos1  26766  2lgs  26890  2sqnn0  26921  umgrislfupgrlem  28362  uhgr2edg  28445  nbusgrvtxm1  28616  uvtx01vtx  28634  g0wlk0  28889  wlkonl1iedg  28902  wlkreslem  28906  crctcshwlkn0lem5  29048  0enwwlksnge1  29098  clwwlknonex2lem2  29341  frgr3vlem2  29507  frgrnbnb  29526  frgrregord013  29628  frgrogt3nreg  29630  2bornot2b  29697  stcltr2i  31506  mdsl1i  31552  prsiga  33067  logdivsqrle  33600  bnj1533  33801  bnj1176  33954  jath  34632  idinside  34994  tb-ax2  35207  bj-a1k  35358  bj-peircestab  35367  bj-currypeirce  35371  bj-andnotim  35404  bj-ssbeq  35468  bj-eqs  35490  bj-nnftht  35557  curryset  35765  currysetlem3  35768  wl-moae  36323  tsim3  36938  mpobi123f  36968  mptbi12f  36972  ac6s6  36978  ax12fromc15  37713  axc5c7toc5  37720  axc5c711toc5  37727  ax12f  37748  ax12eq  37749  ax12el  37750  ax12indi  37752  ax12indalem  37753  ax12inda2ALT  37754  ax12inda2  37755  atpsubN  38562  ifpim23g  42179  rp-fakeimass  42196  inintabss  42262  ntrneiiso  42775  spALT  42886  axc5c4c711toc5  43094  axc5c4c711toc4  43095  axc5c4c711toc7  43096  axc5c4c711to11  43097  pm2.43bgbi  43211  pm2.43cbi  43212  hbimpg  43248  hbimpgVD  43598  ax6e2ndeqVD  43603  ax6e2ndeqALT  43625  ralimralim  43703  confun  45584  confun5  45588  adh-jarrsc  45645  adh-minim  45646  adh-minimp  45658  f1cof1b  45720  iccpartnel  46041  fmtno4prmfac193  46176  prminf2  46191  zeo2ALTV  46274  fpprbasnn  46332  sbgoldbaltlem1  46382  nzerooringczr  46872  islinindfis  47032  lindslinindsimp2lem5  47045  zlmodzxznm  47080