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  828  pm5.31r  832  jao1i  858  olc  868  oibabs  953  pm2.74  976  tarski-bernays-ax2  1636  meredith  1637  tbw-bijust  1694  tbw-negdf  1695  tbw-ax2  1697  merco1  1709  nftht  1788  ala1  1809  exa1  1834  ax13b  2028  sbi2  2300  ax12vALT  2471  moabs  2540  moa1  2548  r19.35  3105  r19.35OLD  3106  r19.21v  3177  r19.37  3259  r19.12OLD  3312  eqvincg  3647  rr19.3v  3666  class2seteq  3712  ralidmw  4513  ralidm  4517  dvdemo2  5379  iunopeqop  5530  po2ne  5612  asymref2  6139  elfv2ex  6952  elovmpt3imp  7689  sorpssuni  7750  dfwe2  7792  ordunisuc2  7864  xpord3ind  8179  smo11  8402  omex  9680  r111  9812  kmlem12  10199  squeeze0  12168  nn0ge2m1nn  12593  nn0lt10b  12677  iccneg  13508  hashfzp1  14466  hash2prde  14505  hash2pwpr  14511  hashge2el2dif  14515  hash3tpde  14528  relexprel  15074  algcvgblem  16610  prm23ge5  16848  cshwshashlem1  17129  dfgrp2e  18993  gsmtrcl  19548  nzerooringczr  21508  symgmatr01lem  22674  cxpcn2  26803  logbgcd1irr  26851  rpdmgm  27082  bpos1  27341  2lgs  27465  2sqnn0  27496  umgrislfupgrlem  29153  uhgr2edg  29239  nbusgrvtxm1  29410  uvtx01vtx  29428  g0wlk0  29684  wlkonl1iedg  29697  wlkreslem  29701  crctcshwlkn0lem5  29843  0enwwlksnge1  29893  clwwlknonex2lem2  30136  frgr3vlem2  30302  frgrnbnb  30321  frgrregord013  30423  frgrogt3nreg  30425  2bornot2b  30492  stcltr2i  32303  mdsl1i  32349  prsiga  34111  logdivsqrle  34643  bnj1533  34844  bnj1176  34997  jath  35704  idinside  36065  tb-ax2  36366  bj-a1k  36526  bj-peircestab  36535  bj-currypeirce  36539  bj-andnotim  36570  bj-ssbeq  36635  bj-eqs  36657  bj-nnftht  36723  curryset  36928  currysetlem3  36931  wl-moae  37496  tsim3  38118  mpobi123f  38148  mptbi12f  38152  ac6s6  38158  ax12fromc15  38886  axc5c7toc5  38893  axc5c711toc5  38900  ax12f  38921  ax12eq  38922  ax12el  38923  ax12indi  38925  ax12indalem  38926  ax12inda2ALT  38927  ax12inda2  38928  atpsubN  39735  ifpim23g  43484  rp-fakeimass  43501  inintabss  43567  ntrneiiso  44080  spALT  44190  axc5c4c711toc5  44397  axc5c4c711toc4  44398  axc5c4c711toc7  44399  axc5c4c711to11  44400  pm2.43bgbi  44514  pm2.43cbi  44515  hbimpg  44551  hbimpgVD  44901  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  ralimralim  45020  confun  46888  confun5  46892  adh-jarrsc  46949  adh-minim  46950  adh-minimp  46962  f1cof1b  47026  iccpartnel  47362  fmtno4prmfac193  47497  prminf2  47512  zeo2ALTV  47595  fpprbasnn  47653  sbgoldbaltlem1  47703  elclnbgrelnbgr  47749  uspgrimprop  47810  islinindfis  48294  lindslinindsimp2lem5  48307  zlmodzxznm  48342