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  1641  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  tbw-ax2  1702  merco1  1714  nftht  1793  ala1  1814  exa1  1839  ax13b  2033  sbi2  2304  ax12vALT  2469  moabs  2538  moa1  2546  r19.35  3090  r19.21v  3157  r19.37  3235  eqvincg  3603  rr19.3v  3622  class2seteq  3663  ralidmw  4458  ralidm  4462  dvdemo2  5312  iunopeqop  5461  po2ne  5540  asymref2  6064  elfv2ex  6865  elovmpt3imp  7603  sorpssuni  7665  dfwe2  7707  ordunisuc2  7774  xpord3ind  8086  smo11  8284  omex  9533  r111  9665  kmlem12  10050  squeeze0  12022  nn0ge2m1nn  12448  nn0lt10b  12532  iccneg  13369  hashfzp1  14335  hash2prde  14374  hash2pwpr  14380  hashge2el2dif  14384  hash3tpde  14397  relexprel  14943  algcvgblem  16485  prm23ge5  16724  cshwshashlem1  17004  dfgrp2e  18873  gsmtrcl  19426  nzerooringczr  21415  symgmatr01lem  22566  cxpcn2  26681  logbgcd1irr  26729  rpdmgm  26960  bpos1  27219  2lgs  27343  2sqnn0  27374  umgrislfupgrlem  29098  uhgr2edg  29184  nbusgrvtxm1  29355  uvtx01vtx  29373  g0wlk0  29627  wlkonl1iedg  29640  wlkreslem  29644  crctcshwlkn0lem5  29790  0enwwlksnge1  29840  clwwlknonex2lem2  30083  frgr3vlem2  30249  frgrnbnb  30268  frgrregord013  30370  frgrogt3nreg  30372  2bornot2b  30439  stcltr2i  32250  mdsl1i  32296  prsiga  34139  logdivsqrle  34658  bnj1533  34859  bnj1176  35012  onvf1odlem1  35135  jath  35757  idinside  36117  tb-ax2  36417  bj-a1k  36577  bj-peircestab  36586  bj-currypeirce  36590  bj-andnotim  36621  bj-ssbeq  36686  bj-eqs  36708  bj-nnftht  36774  curryset  36979  currysetlem3  36982  wl-moae  37549  tsim3  38171  mpobi123f  38201  mptbi12f  38205  ac6s6  38211  ax12fromc15  38943  axc5c7toc5  38950  axc5c711toc5  38957  ax12f  38978  ax12eq  38979  ax12el  38980  ax12indi  38982  ax12indalem  38983  ax12inda2ALT  38984  ax12inda2  38985  atpsubN  39791  ifpim23g  43527  rp-fakeimass  43544  inintabss  43610  ntrneiiso  44123  spALT  44233  axc5c4c711toc5  44434  axc5c4c711toc4  44435  axc5c4c711toc7  44436  axc5c4c711to11  44437  pm2.43bgbi  44549  pm2.43cbi  44550  hbimpg  44586  hbimpgVD  44935  ax6e2ndeqVD  44940  ax6e2ndeqALT  44962  dfbi1ALTa  44971  simprimi  44972  ralimralim  45117  confun  46969  confun5  46973  adh-jarrsc  47030  adh-minim  47031  adh-minimp  47043  f1cof1b  47107  iccpartnel  47468  fmtno4prmfac193  47603  prminf2  47618  zeo2ALTV  47701  fpprbasnn  47759  sbgoldbaltlem1  47809  elclnbgrelnbgr  47855  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  islinindfis  48480  lindslinindsimp2lem5  48493  zlmodzxznm  48528