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  262  biimt  360  pm4.8  393  pm4.45im  826  pm5.31r  830  jao1i  856  olc  866  oibabs  950  pm2.74  973  tarski-bernays-ax2  1642  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  tbw-ax2  1703  merco1  1715  nftht  1794  ala1  1815  exa1  1840  ax13b  2035  sbi2  2298  ax12vALT  2468  moabs  2537  moa1  2545  r19.35  3108  r19.35OLD  3109  r19.21v  3179  r19.37  3259  r19.12OLD  3312  eqvincg  3636  rr19.3v  3657  class2seteq  3700  ss2abdv  4060  ralidmw  4507  ralidm  4511  invdisjrab  5134  dvdemo2  5372  iunopeqop  5521  po2ne  5604  asymref2  6118  elfv2ex  6937  elovmpt3imp  7665  sorpssuni  7724  dfwe2  7763  ordunisuc2  7835  xpord3ind  8144  smo11  8366  omex  9640  r111  9772  kmlem12  10158  squeeze0  12119  nn0ge2m1nn  12543  nn0lt10b  12626  iccneg  13451  hashfzp1  14393  hash2prde  14433  hash2pwpr  14439  hashge2el2dif  14443  relexprel  14988  algcvgblem  16516  prm23ge5  16750  cshwshashlem1  17031  dfgrp2e  18850  gsmtrcl  19386  symgmatr01lem  22162  cxpcn2  26261  logbgcd1irr  26306  rpdmgm  26536  bpos1  26793  2lgs  26917  2sqnn0  26948  umgrislfupgrlem  28420  uhgr2edg  28503  nbusgrvtxm1  28674  uvtx01vtx  28692  g0wlk0  28947  wlkonl1iedg  28960  wlkreslem  28964  crctcshwlkn0lem5  29106  0enwwlksnge1  29156  clwwlknonex2lem2  29399  frgr3vlem2  29565  frgrnbnb  29584  frgrregord013  29686  frgrogt3nreg  29688  2bornot2b  29755  stcltr2i  31566  mdsl1i  31612  prsiga  33198  logdivsqrle  33731  bnj1533  33932  bnj1176  34085  jath  34769  idinside  35131  tb-ax2  35361  bj-a1k  35512  bj-peircestab  35521  bj-currypeirce  35525  bj-andnotim  35558  bj-ssbeq  35622  bj-eqs  35644  bj-nnftht  35711  curryset  35919  currysetlem3  35922  wl-moae  36477  tsim3  37092  mpobi123f  37122  mptbi12f  37126  ac6s6  37132  ax12fromc15  37867  axc5c7toc5  37874  axc5c711toc5  37881  ax12f  37902  ax12eq  37903  ax12el  37904  ax12indi  37906  ax12indalem  37907  ax12inda2ALT  37908  ax12inda2  37909  atpsubN  38716  ifpim23g  42334  rp-fakeimass  42351  inintabss  42417  ntrneiiso  42930  spALT  43041  axc5c4c711toc5  43249  axc5c4c711toc4  43250  axc5c4c711toc7  43251  axc5c4c711to11  43252  pm2.43bgbi  43366  pm2.43cbi  43367  hbimpg  43403  hbimpgVD  43753  ax6e2ndeqVD  43758  ax6e2ndeqALT  43780  ralimralim  43858  confun  45734  confun5  45738  adh-jarrsc  45795  adh-minim  45796  adh-minimp  45808  f1cof1b  45870  iccpartnel  46191  fmtno4prmfac193  46326  prminf2  46341  zeo2ALTV  46424  fpprbasnn  46482  sbgoldbaltlem1  46532  nzerooringczr  47055  islinindfis  47214  lindslinindsimp2lem5  47227  zlmodzxznm  47262