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  827  pm5.31r  831  jao1i  858  olc  868  oibabs  953  pm2.74  976  tarski-bernays-ax2  1640  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  tbw-ax2  1701  merco1  1713  nftht  1792  ala1  1813  exa1  1838  ax13b  2032  sbi2  2302  ax12vALT  2467  moabs  2536  moa1  2544  r19.35  3087  r19.21v  3154  r19.37  3232  eqvincg  3605  rr19.3v  3624  class2seteq  3666  ralidmw  4461  ralidm  4465  dvdemo2  5316  iunopeqop  5468  po2ne  5547  asymref2  6070  elfv2ex  6870  elovmpt3imp  7610  sorpssuni  7672  dfwe2  7714  ordunisuc2  7784  xpord3ind  8096  smo11  8294  omex  9558  r111  9690  kmlem12  10075  squeeze0  12046  nn0ge2m1nn  12472  nn0lt10b  12556  iccneg  13393  hashfzp1  14356  hash2prde  14395  hash2pwpr  14401  hashge2el2dif  14405  hash3tpde  14418  relexprel  14964  algcvgblem  16506  prm23ge5  16745  cshwshashlem1  17025  dfgrp2e  18860  gsmtrcl  19413  nzerooringczr  21405  symgmatr01lem  22556  cxpcn2  26672  logbgcd1irr  26720  rpdmgm  26951  bpos1  27210  2lgs  27334  2sqnn0  27365  umgrislfupgrlem  29085  uhgr2edg  29171  nbusgrvtxm1  29342  uvtx01vtx  29360  g0wlk0  29614  wlkonl1iedg  29627  wlkreslem  29631  crctcshwlkn0lem5  29777  0enwwlksnge1  29827  clwwlknonex2lem2  30070  frgr3vlem2  30236  frgrnbnb  30255  frgrregord013  30357  frgrogt3nreg  30359  2bornot2b  30426  stcltr2i  32237  mdsl1i  32283  prsiga  34097  logdivsqrle  34617  bnj1533  34818  bnj1176  34971  onvf1odlem1  35075  jath  35697  idinside  36057  tb-ax2  36357  bj-a1k  36517  bj-peircestab  36526  bj-currypeirce  36530  bj-andnotim  36561  bj-ssbeq  36626  bj-eqs  36648  bj-nnftht  36714  curryset  36919  currysetlem3  36922  wl-moae  37489  tsim3  38111  mpobi123f  38141  mptbi12f  38145  ac6s6  38151  ax12fromc15  38883  axc5c7toc5  38890  axc5c711toc5  38897  ax12f  38918  ax12eq  38919  ax12el  38920  ax12indi  38922  ax12indalem  38923  ax12inda2ALT  38924  ax12inda2  38925  atpsubN  39732  ifpim23g  43468  rp-fakeimass  43485  inintabss  43551  ntrneiiso  44064  spALT  44174  axc5c4c711toc5  44375  axc5c4c711toc4  44376  axc5c4c711toc7  44377  axc5c4c711to11  44378  pm2.43bgbi  44491  pm2.43cbi  44492  hbimpg  44528  hbimpgVD  44877  ax6e2ndeqVD  44882  ax6e2ndeqALT  44904  dfbi1ALTa  44913  simprimi  44914  ralimralim  45059  confun  46924  confun5  46928  adh-jarrsc  46985  adh-minim  46986  adh-minimp  46998  f1cof1b  47062  iccpartnel  47423  fmtno4prmfac193  47558  prminf2  47573  zeo2ALTV  47656  fpprbasnn  47714  sbgoldbaltlem1  47764  elclnbgrelnbgr  47810  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  islinindfis  48435  lindslinindsimp2lem5  48448  zlmodzxznm  48483