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  173  dfbi1ALT  217  pm5.1im  266  biimt  364  pm4.8  396  pm4.45im  826  pm5.31r  830  jao1i  855  olc  865  oibabs  949  pm2.74  972  tarski-bernays-ax2  1642  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  tbw-ax2  1703  merco1  1715  nftht  1794  ala1  1815  exa1  1839  ax13b  2039  sbi2  2306  ax12vALT  2481  sbi2ALT  2583  moabs  2601  moa1  2610  euimOLD  2679  r19.12  3283  r19.35  3295  r19.37  3297  eqvincg  3589  rr19.3v  3607  ss2abdv  3991  invdisjrab  5016  class2seteq  5220  dvdemo2  5240  iunopeqop  5376  po2ne  5453  asymref2  5944  elfv2ex  6686  elovmpt3imp  7382  sorpssuni  7438  dfwe2  7476  ordunisuc2  7539  smo11  7984  omex  9090  r111  9188  kmlem12  9572  squeeze0  11532  nn0ge2m1nn  11952  nn0lt10b  12032  iccneg  12850  hashfzp1  13788  hash2prde  13824  hash2pwpr  13830  hashge2el2dif  13834  relexprel  14390  algcvgblem  15911  prm23ge5  16142  cshwshashlem1  16421  dfgrp2e  18121  gsmtrcl  18636  symgmatr01lem  21258  cxpcn2  25335  logbgcd1irr  25380  rpdmgm  25610  bpos1  25867  2lgs  25991  2sqnn0  26022  umgrislfupgrlem  26915  uhgr2edg  26998  nbusgrvtxm1  27169  uvtx01vtx  27187  g0wlk0  27441  wlkonl1iedg  27455  wlkreslem  27459  crctcshwlkn0lem5  27600  0enwwlksnge1  27650  clwwlknonex2lem2  27893  frgr3vlem2  28059  frgrnbnb  28078  frgrregord013  28180  frgrogt3nreg  28182  2bornot2b  28249  stcltr2i  30058  mdsl1i  30104  prsiga  31500  logdivsqrle  32031  bnj1533  32234  bnj1176  32387  jath  33071  idinside  33658  tb-ax2  33845  bj-a1k  33996  bj-peircestab  34001  bj-currypeirce  34005  bj-andnotim  34035  bj-ssbeq  34099  bj-eqs  34121  bj-nnftht  34185  curryset  34381  currysetlem3  34384  wl-moae  34921  tsim3  35570  mpobi123f  35600  mptbi12f  35604  ac6s6  35610  ax12fromc15  36201  axc5c7toc5  36208  axc5c711toc5  36215  ax12f  36236  ax12eq  36237  ax12el  36238  ax12indi  36240  ax12indalem  36241  ax12inda2ALT  36242  ax12inda2  36243  atpsubN  37049  ifpim23g  40203  rp-fakeimass  40220  inintabss  40278  ntrneiiso  40794  spALT  40907  axc5c4c711toc5  41106  axc5c4c711toc4  41107  axc5c4c711toc7  41108  axc5c4c711to11  41109  pm2.43bgbi  41223  pm2.43cbi  41224  hbimpg  41260  hbimpgVD  41610  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  ralimralim  41717  confun  43532  confun5  43536  adh-jarrsc  43593  adh-minim  43594  adh-minimp  43606  iccpartnel  43955  fmtno4prmfac193  44090  prminf2  44105  zeo2ALTV  44189  fpprbasnn  44247  sbgoldbaltlem1  44297  nzerooringczr  44696  islinindfis  44858  lindslinindsimp2lem5  44871  zlmodzxznm  44906