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  172  dfbi1ALT  216  pm5.1im  265  biimt  363  pm4.8  395  pm4.45im  825  pm5.31r  829  jao1i  854  olc  864  oibabs  948  pm2.74  971  tarski-bernays-ax2  1641  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  tbw-ax2  1702  merco1  1714  nftht  1793  ala1  1814  exa1  1838  ax13b  2039  sbi2  2310  sbi2vOLD  2324  ax12vALT  2492  sbi2ALT  2607  moabs  2625  moa1  2635  euimOLD  2702  r19.27vOLD  3185  r19.12  3324  r19.12OLD  3327  r19.35  3341  r19.37  3343  eqvincg  3641  rr19.3v  3661  invdisjrab  5052  class2seteq  5255  dvdemo2  5275  iunopeqop  5411  po2ne  5489  asymref2  5977  elfv2ex  6711  elovmpt3imp  7402  sorpssuni  7458  dfwe2  7496  ordunisuc2  7559  smo11  8001  omex  9106  r111  9204  kmlem12  9587  squeeze0  11543  nn0ge2m1nn  11965  nn0lt10b  12045  iccneg  12859  hashfzp1  13793  hash2prde  13829  hash2pwpr  13835  hashge2el2dif  13839  relexprel  14398  algcvgblem  15921  prm23ge5  16152  cshwshashlem1  16429  dfgrp2e  18129  gsmtrcl  18644  symgmatr01lem  21262  cxpcn2  25327  logbgcd1irr  25372  rpdmgm  25602  bpos1  25859  2lgs  25983  2sqnn0  26014  umgrislfupgrlem  26907  uhgr2edg  26990  nbusgrvtxm1  27161  uvtx01vtx  27179  g0wlk0  27433  wlkonl1iedg  27447  wlkreslem  27451  crctcshwlkn0lem5  27592  0enwwlksnge1  27642  clwwlknonex2lem2  27887  frgr3vlem2  28053  frgrnbnb  28072  frgrregord013  28174  frgrogt3nreg  28176  2bornot2b  28243  stcltr2i  30052  mdsl1i  30098  prsiga  31390  logdivsqrle  31921  bnj1533  32124  bnj1176  32277  jath  32958  idinside  33545  tb-ax2  33732  bj-a1k  33883  bj-peircestab  33888  bj-currypeirce  33892  bj-andnotim  33922  bj-ssbeq  33986  bj-eqs  34008  bj-nnftht  34070  curryset  34260  currysetlem3  34263  wl-moae  34771  tsim3  35425  mpobi123f  35455  mptbi12f  35459  ac6s6  35465  ax12fromc15  36056  axc5c7toc5  36063  axc5c711toc5  36070  ax12f  36091  ax12eq  36092  ax12el  36093  ax12indi  36095  ax12indalem  36096  ax12inda2ALT  36097  ax12inda2  36098  atpsubN  36904  ifpim23g  39910  rp-fakeimass  39927  inintabss  39987  ntrneiiso  40490  spALT  40603  axc5c4c711toc5  40783  axc5c4c711toc4  40784  axc5c4c711toc7  40785  axc5c4c711to11  40786  pm2.43bgbi  40900  pm2.43cbi  40901  hbimpg  40937  hbimpgVD  41287  ax6e2ndeqVD  41292  ax6e2ndeqALT  41314  ralimralim  41394  confun  43224  confun5  43228  adh-jarrsc  43285  adh-minim  43286  adh-minimp  43298  iccpartnel  43647  fmtno4prmfac193  43784  prminf2  43799  zeo2ALTV  43885  fpprbasnn  43943  sbgoldbaltlem1  43993  nzerooringczr  44392  islinindfis  44553  lindslinindsimp2lem5  44566  zlmodzxznm  44601