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  3087  r19.21v  3154  r19.37  3232  eqvincg  3605  rr19.3v  3624  class2seteq  3666  ralidmw  4461  ralidm  4465  dvdemo2  5316  iunopeqop  5468  po2ne  5547  asymref2  6070  elfv2ex  6870  elovmpt3imp  7610  sorpssuni  7672  dfwe2  7714  ordunisuc2  7784  xpord3ind  8096  smo11  8294  omex  9558  r111  9690  kmlem12  10075  squeeze0  12047  nn0ge2m1nn  12473  nn0lt10b  12557  iccneg  13394  hashfzp1  14357  hash2prde  14396  hash2pwpr  14402  hashge2el2dif  14406  hash3tpde  14419  relexprel  14965  algcvgblem  16507  prm23ge5  16746  cshwshashlem1  17026  dfgrp2e  18861  gsmtrcl  19414  nzerooringczr  21406  symgmatr01lem  22557  cxpcn2  26673  logbgcd1irr  26721  rpdmgm  26952  bpos1  27211  2lgs  27335  2sqnn0  27366  umgrislfupgrlem  29086  uhgr2edg  29172  nbusgrvtxm1  29343  uvtx01vtx  29361  g0wlk0  29615  wlkonl1iedg  29628  wlkreslem  29632  crctcshwlkn0lem5  29778  0enwwlksnge1  29828  clwwlknonex2lem2  30071  frgr3vlem2  30237  frgrnbnb  30256  frgrregord013  30358  frgrogt3nreg  30360  2bornot2b  30427  stcltr2i  32238  mdsl1i  32284  prsiga  34117  logdivsqrle  34637  bnj1533  34838  bnj1176  34991  onvf1odlem1  35095  jath  35717  idinside  36077  tb-ax2  36377  bj-a1k  36537  bj-peircestab  36546  bj-currypeirce  36550  bj-andnotim  36581  bj-ssbeq  36646  bj-eqs  36668  bj-nnftht  36734  curryset  36939  currysetlem3  36942  wl-moae  37509  tsim3  38131  mpobi123f  38161  mptbi12f  38165  ac6s6  38171  ax12fromc15  38903  axc5c7toc5  38910  axc5c711toc5  38917  ax12f  38938  ax12eq  38939  ax12el  38940  ax12indi  38942  ax12indalem  38943  ax12inda2ALT  38944  ax12inda2  38945  atpsubN  39752  ifpim23g  43488  rp-fakeimass  43505  inintabss  43571  ntrneiiso  44084  spALT  44194  axc5c4c711toc5  44395  axc5c4c711toc4  44396  axc5c4c711toc7  44397  axc5c4c711to11  44398  pm2.43bgbi  44511  pm2.43cbi  44512  hbimpg  44548  hbimpgVD  44897  ax6e2ndeqVD  44902  ax6e2ndeqALT  44924  dfbi1ALTa  44933  simprimi  44934  ralimralim  45079  confun  46943  confun5  46947  adh-jarrsc  47004  adh-minim  47005  adh-minimp  47017  f1cof1b  47081  iccpartnel  47442  fmtno4prmfac193  47577  prminf2  47592  zeo2ALTV  47675  fpprbasnn  47733  sbgoldbaltlem1  47783  elclnbgrelnbgr  47829  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  islinindfis  48454  lindslinindsimp2lem5  48467  zlmodzxznm  48502