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  2306  ax12vALT  2471  moabs  2541  moa1  2549  r19.35  3092  r19.21v  3159  r19.37  3237  eqvincg  3600  rr19.3v  3619  class2seteq  3660  r19.3rzv  4454  ralidmw  4467  ralidm  4468  dvdemo2  5317  iunopeqop  5467  po2ne  5546  asymref2  6072  elfv2ex  6875  elovmpt3imp  7613  sorpssuni  7675  dfwe2  7717  ordunisuc2  7784  xpord3ind  8096  smo11  8294  omex  9550  r111  9685  kmlem12  10070  squeeze0  12043  nn0ge2m1nn  12469  nn0lt10b  12552  iccneg  13386  hashfzp1  14352  hash2prde  14391  hash2pwpr  14397  hashge2el2dif  14401  hash3tpde  14414  relexprel  14960  algcvgblem  16502  prm23ge5  16741  cshwshashlem1  17021  dfgrp2e  18891  gsmtrcl  19443  nzerooringczr  21433  symgmatr01lem  22595  cxpcn2  26710  logbgcd1irr  26758  rpdmgm  26989  bpos1  27248  2lgs  27372  2sqnn0  27403  umgrislfupgrlem  29144  uhgr2edg  29230  nbusgrvtxm1  29401  uvtx01vtx  29419  g0wlk0  29673  wlkonl1iedg  29686  wlkreslem  29690  crctcshwlkn0lem5  29836  0enwwlksnge1  29886  clwwlknonex2lem2  30132  frgr3vlem2  30298  frgrnbnb  30317  frgrregord013  30419  frgrogt3nreg  30421  2bornot2b  30488  stcltr2i  32299  mdsl1i  32345  prsiga  34237  logdivsqrle  34756  bnj1533  34957  bnj1176  35110  onvf1odlem1  35246  jath  35868  idinside  36227  tb-ax2  36527  bj-a1k  36687  bj-peircestab  36696  bj-currypeirce  36700  bj-andnotim  36731  bj-ssbeq  36797  bj-eqs  36819  bj-nnftht  36885  curryset  37090  currysetlem3  37093  wl-moae  37660  tsim3  38272  mpobi123f  38302  mptbi12f  38306  ac6s6  38312  ax12fromc15  39104  axc5c7toc5  39111  axc5c711toc5  39118  ax12f  39139  ax12eq  39140  ax12el  39141  ax12indi  39143  ax12indalem  39144  ax12inda2ALT  39145  ax12inda2  39146  atpsubN  39952  ifpim23g  43678  rp-fakeimass  43695  inintabss  43761  ntrneiiso  44274  spALT  44384  axc5c4c711toc5  44585  axc5c4c711toc4  44586  axc5c4c711toc7  44587  axc5c4c711to11  44588  pm2.43bgbi  44700  pm2.43cbi  44701  hbimpg  44737  hbimpgVD  45086  ax6e2ndeqVD  45091  ax6e2ndeqALT  45113  dfbi1ALTa  45122  simprimi  45123  ralimralim  45268  confun  47127  confun5  47131  adh-jarrsc  47188  adh-minim  47189  adh-minimp  47201  f1cof1b  47265  iccpartnel  47626  fmtno4prmfac193  47761  prminf2  47776  zeo2ALTV  47859  fpprbasnn  47917  sbgoldbaltlem1  47967  elclnbgrelnbgr  48013  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  islinindfis  48637  lindslinindsimp2lem5  48650  zlmodzxznm  48685