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  pm2.51  167  dfbi1ALT  206  pm5.1im  255  biimt  352  pm5.4  380  pm4.8  383  simplOLD  477  pm4.45im  863  jao1i  889  olc  899  biort  964  pm5.14  974  oibabs  979  pm2.74  1002  dedlem0a  1070  meredith  1740  tbw-bijust  1797  tbw-negdf  1798  tbw-ax2  1800  merco1  1812  nftht  1891  ala1  1912  exa1  1936  ax13b  2139  stdpc4v  2301  sbi2v  2336  sbi2  2524  ax12vALT  2560  moabs  2609  moa1  2620  moeuOLD  2671  euim  2705  r19.12  3273  r19.27v  3280  r19.37  3296  eqvincg  3547  rr19.3v  3564  invdisjrab  4860  class2seteq  5055  dvdemo2  5074  iunopeqop  5207  asymref2  5755  elfv2ex  6475  elovmpt3imp  7150  sorpssuni  7206  sorpssint  7207  dfwe2  7242  ordunisuc2  7305  tfindsg  7321  findsg  7354  smo11  7727  omex  8817  r111  8915  kmlem12  9298  ltlen  10457  squeeze0  11256  elnnnn0b  11664  nn0ge2m1nn  11687  nn0lt10b  11767  znnn0nn  11817  iccneg  12584  hashfzp1  13507  hash2prde  13541  hash2pwpr  13547  hashge2el2dif  13551  scshwfzeqfzo  13947  relexprel  14156  algcvgblem  15663  prm23ge5  15891  prmgaplem5  16130  prmgaplem6  16131  cshwshashlem1  16168  dfgrp2e  17802  gsmtrcl  18287  prmirred  20203  symgmatr01lem  20828  pmatcollpw3fi1  20963  cxpcn2  24889  logbgcd1irr  24934  rpdmgm  25164  bpos1  25421  2lgs  25545  umgrislfupgrlem  26420  uhgr2edg  26504  nbusgrvtxm1  26677  uvtx01vtx  26695  g0wlk0  26949  wlkonl1iedg  26962  wlkreslem  26968  wlkreslemOLD  26970  crctcshwlkn0lem5  27113  0enwwlksnge1  27163  clwwlknonex2lem2  27472  frgr3vlem2  27644  frgrnbnb  27663  frgrregord013  27799  frgrogt3nreg  27801  2bornot2b  27867  stcltr2i  29678  mdsl1i  29724  prsiga  30728  logdivsqrle  31266  bnj1533  31457  bnj1176  31608  jath  32142  idinside  32719  tb-ax2  32906  bj-a1k  33056  bj-andnotim  33091  bj-ssbeq  33157  bj-ssb0  33158  bj-ssb1a  33162  bj-eqs  33191  bj-dvdemo2  33321  wl-moae  33837  wl-dv-sb  33867  tsim3  34472  mpt2bi123f  34504  mptbi12f  34508  ac6s6  34514  ax12fromc15  34973  axc5c7toc5  34980  axc5c711toc5  34987  ax12f  35008  ax12eq  35009  ax12el  35010  ax12indi  35012  ax12indalem  35013  ax12inda2ALT  35014  ax12inda2  35015  atpsubN  35821  ifpim23g  38675  rp-fakeimass  38692  inintabss  38718  ntrneiiso  39222  axc5c4c711toc5  39435  axc5c4c711toc4  39436  axc5c4c711toc7  39437  axc5c4c711to11  39438  pm2.43bgbi  39554  pm2.43cbi  39555  hbimpg  39591  hbimpgVD  39951  ax6e2ndeqVD  39956  ax6e2ndeqALT  39978  ralimralim  40063  confun  41893  confun5  41897  iccpartnel  42255  fmtno4prmfac193  42308  prminf2  42323  zeo2ALTV  42405  sbgoldbaltlem1  42490  nzerooringczr  42912  islinindfis  43078  lindslinindsimp2lem5  43091  zlmodzxznm  43126