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  pm2.86d  107  pm2.86i  109  pm2.51  165  dfbi1ALT  204  pm5.1im  253  biimt  350  pm5.4  377  pm4.8  380  olc  399  simpl  473  pm4.45im  585  jao1i  825  pm2.74  891  oibabs  925  pm5.14  930  biort  938  dedlem0a  1000  meredith  1566  tbw-bijust  1623  tbw-negdf  1624  tbw-ax2  1626  merco1  1638  nftht  1718  ala1  1741  exa1  1765  ax13b  1964  ax12OLD  2341  sbi2  2393  ax12vALT  2428  moa1  2521  euim  2523  r19.12  3063  r19.27v  3070  r19.37  3086  eqvincg  3329  rr19.3v  3345  invdisjrab  4639  class2seteq  4833  dvdemo2  4903  iunopeqop  4981  asymref2  5513  elfv2ex  6229  elovmpt3imp  6890  sorpssuni  6946  sorpssint  6947  dfwe2  6981  ordunisuc2  7044  tfindsg  7060  findsg  7093  smo11  7461  omex  8540  r111  8638  kmlem12  8983  ltlen  10138  squeeze0  10926  elnnnn0b  11337  nn0ge2m1nn  11360  nn0lt10b  11439  znnn0nn  11489  iccneg  12293  hashfzp1  13218  hash2prde  13252  hash2pwpr  13258  hashge2el2dif  13262  scshwfzeqfzo  13572  relexprel  13779  algcvgblem  15290  prm23ge5  15520  prmgaplem5  15759  prmgaplem6  15760  cshwshashlem1  15802  dfgrp2e  17448  gsmtrcl  17936  prmirred  19843  symgmatr01lem  20459  pmatcollpw3fi1  20593  cxpcn2  24487  rpdmgm  24751  bpos1  25008  2lgs  25132  umgrislfupgrlem  26017  uhgr2edg  26100  nbusgrvtxm1  26281  uvtxa01vtx0  26297  g0wlk0  26548  wlkonl1iedg  26561  wlkreslem  26566  crctcshwlkn0lem5  26706  0enwwlksnge1  26749  frgr3vlem2  27138  frgrnbnb  27157  frgrregord013  27253  frgrogt3nreg  27255  2bornot2b  27320  stcltr2i  29134  mdsl1i  29180  prsiga  30194  logdivsqrle  30728  bnj1533  30922  bnj1176  31073  jath  31609  idinside  32191  tb-ax2  32379  bj-a1k  32535  bj-imim2ALT  32538  pm4.81ALT  32546  bj-andnotim  32573  bj-ssbeq  32627  bj-ssb0  32628  bj-ssb1a  32632  bj-eqs  32663  bj-stdpc4v  32754  bj-dvdemo2  32803  wl-jarri  33288  tsim3  33939  mpt2bi123f  33971  mptbi12f  33975  ac6s6  33980  ax12fromc15  34190  axc5c7toc5  34197  axc5c711toc5  34204  ax12f  34225  ax12eq  34226  ax12el  34227  ax12indi  34229  ax12indalem  34230  ax12inda2ALT  34231  ax12inda2  34232  atpsubN  35039  ifpim23g  37840  rp-fakeimass  37857  inintabss  37884  ntrneiiso  38389  axc5c4c711toc5  38603  axc5c4c711toc4  38604  axc5c4c711toc7  38605  axc5c4c711to11  38606  pm2.43bgbi  38723  pm2.43cbi  38724  hbimpg  38770  hbimpgVD  39140  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  ralimralim  39253  confun  41106  confun5  41110  iccpartnel  41374  fmtno4prmfac193  41485  prminf2  41500  zeo2ALTV  41582  sbgoldbaltlem1  41667  nzerooringczr  42072  islinindfis  42238  lindslinindsimp2lem5  42251  zlmodzxznm  42286