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  361  pm4.8  393  pm4.45im  825  pm5.31r  829  jao1i  855  olc  865  oibabs  949  pm2.74  972  tarski-bernays-ax2  1647  meredith  1648  tbw-bijust  1705  tbw-negdf  1706  tbw-ax2  1708  merco1  1720  nftht  1799  ala1  1820  exa1  1844  ax13b  2039  sbi2  2303  ax12vALT  2471  moabs  2545  moa1  2553  r19.12OLD  3256  r19.35  3271  r19.37  3273  eqvincg  3579  rr19.3v  3600  ss2abdv  4002  ralidmw  4444  ralidm  4448  invdisjrab  5065  class2seteq  5281  dvdemo2  5301  iunopeqop  5438  po2ne  5519  asymref2  6020  elfv2ex  6810  elovmpt3imp  7518  sorpssuni  7577  dfwe2  7616  ordunisuc2  7683  smo11  8184  omex  9377  r111  9532  kmlem12  9916  squeeze0  11876  nn0ge2m1nn  12300  nn0lt10b  12380  iccneg  13201  hashfzp1  14142  hash2prde  14180  hash2pwpr  14186  hashge2el2dif  14190  relexprel  14746  algcvgblem  16278  prm23ge5  16512  cshwshashlem1  16793  dfgrp2e  18601  gsmtrcl  19120  symgmatr01lem  21798  cxpcn2  25895  logbgcd1irr  25940  rpdmgm  26170  bpos1  26427  2lgs  26551  2sqnn0  26582  umgrislfupgrlem  27488  uhgr2edg  27571  nbusgrvtxm1  27742  uvtx01vtx  27760  g0wlk0  28014  wlkonl1iedg  28028  wlkreslem  28032  crctcshwlkn0lem5  28173  0enwwlksnge1  28223  clwwlknonex2lem2  28466  frgr3vlem2  28632  frgrnbnb  28651  frgrregord013  28753  frgrogt3nreg  28755  2bornot2b  28822  stcltr2i  30631  mdsl1i  30677  prsiga  32093  logdivsqrle  32624  bnj1533  32826  bnj1176  32979  jath  33666  idinside  34380  tb-ax2  34567  bj-a1k  34718  bj-peircestab  34727  bj-currypeirce  34731  bj-andnotim  34764  bj-ssbeq  34828  bj-eqs  34850  bj-nnftht  34917  curryset  35129  currysetlem3  35132  wl-moae  35669  tsim3  36284  mpobi123f  36314  mptbi12f  36318  ac6s6  36324  ax12fromc15  36913  axc5c7toc5  36920  axc5c711toc5  36927  ax12f  36948  ax12eq  36949  ax12el  36950  ax12indi  36952  ax12indalem  36953  ax12inda2ALT  36954  ax12inda2  36955  atpsubN  37761  ifpim23g  41079  rp-fakeimass  41096  inintabss  41154  ntrneiiso  41669  spALT  41780  axc5c4c711toc5  41988  axc5c4c711toc4  41989  axc5c4c711toc7  41990  axc5c4c711to11  41991  pm2.43bgbi  42105  pm2.43cbi  42106  hbimpg  42142  hbimpgVD  42492  ax6e2ndeqVD  42497  ax6e2ndeqALT  42519  ralimralim  42599  confun  44400  confun5  44404  adh-jarrsc  44461  adh-minim  44462  adh-minimp  44474  f1cof1b  44535  iccpartnel  44857  fmtno4prmfac193  44992  prminf2  45007  zeo2ALTV  45090  fpprbasnn  45148  sbgoldbaltlem1  45198  nzerooringczr  45597  islinindfis  45757  lindslinindsimp2lem5  45770  zlmodzxznm  45805