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 used by:  a1i  11  ax1w  13  id  23  idALT  24  a1d  26  a1dd  51  a1ddd  81  jarr  107  jarri  108  pm2.86d  109  conax1  171  dfbi1ALT  217  pm5.1im  266  biimt  363  pm4.8  398  pm4.45im  841  pm5.31r  845  jao1i  872  olc  882  oibabs  966  pm2.74  990  tarski-bernays-ax2  1673  meredith  1674  tbw-bijust  1731  tbw-negdf  1732  tbw-ax2  1734  merco1  1746  nftht  1825  ala1  1846  exa1  1871  ax13b  2067  sbrimvw  2130  sbi2  2339  ax12vALT  2501  moabs  2571  moa1  2579  r19.35  3124  r19.21v  3191  r19.37  3269  eqvincg  3605  rr19.3v  3624  class2seteq  3665  r19.3rzv  4462  ralidmw  4475  ralidm  4476  dvdemo2  5340  iunopeqop  5498  iunopeqopOLD  5499  po2ne  5579  asymref2  6122  elfv2ex  6948  elovmpt3imp  7699  sorpssuni  7769  xpord3ind  8197  omex  9668  kmlem12  10264  squeeze0  12244  nn0ge2m1nn  12700  nn0lt10b  12785  iccneg  13627  hashfzp1  14600  hash2prde  14639  hash2pwpr  14645  hashge2el2dif  14649  hash3tpde  14662  relexprel  15218  algcvgblem  16778  prm23ge5  17019  cshwshashlem1  17299  dfgrp2e  19200  gsmtrcl  19757  nzerooringczr  21813  symgmatr01lem  22995  cxpcn2  27101  logbgcd1irr  27149  rpdmgm  27379  bpos1  27637  2lgs  27761  umgrislfupgrlem  29727  uhgr2edg  29816  nbusgrvtxm1  29987  uvtx01vtx  30005  g0wlk0  30258  wlkonl1iedg  30271  wlkreslem  30275  crctcshwlkn0lem5  30430  0enwwlksnge1  30480  clwwlknonex2lem2  30726  frgr3vlem2  30902  frgrnbnb  30921  frgrregord013  31023  frgrogt3nreg  31025  2bornot2b  31092  stcltr2i  32904  mdsl1i  32950  prsiga  34830  logdivsqrle  35346  bnj1533  35549  bnj1176  35702  axprALT2  35815  onvf1odlem1  36030  jath  36667  idinside  37026  tb-ax2  37349  bj-peircestab  37597  bj-currypeirce  37603  bj-andnotim  37635  bj-ssbeq  37729  bj-eqs  37752  bj-alnnf  37816  curryset  38036  currysetlem3  38039  wl-moae  38639  tsim3  39255  mpobi123f  39285  mptbi12f  39289  ac6s6  39295  ax12fromc15  40153  axc5c7toc5  40160  axc5c711toc5  40167  ax12f  40188  ax12eq  40189  ax12el  40190  ax12indi  40192  ax12indalem  40193  ax12inda2ALT  40194  ax12inda2  40195  atpsubN  41001  ifpim23g  44686  rp-fakeimass  44703  inintabss  44769  ntrneiiso  45281  spALT  45391  axc5c4c711toc5  45576  axc5c4c711toc4  45577  axc5c4c711toc7  45578  axc5c4c711to11  45579  pm2.43bgbi  45689  pm2.43cbi  45690  hbimpg  45726  hbimpgVD  46075  ax6e2ndeqVD  46080  ax6e2ndeqALT  46102  dfbi1ALTa  46122  simprimi  46123  ralimralim  46301  confun  48212  confun5  48216  adh-jarrsc  48273  adh-minim  48274  adh-minimp  48286  f1cof1b  48350  iccpartnel  48723  fmtno4prmfac193  48861  prminf2  48876  zeo2ALTV  48972  fpprbasnn  49030  sbgoldbaltlem1  49080  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  islinindfis  49764  lindslinindsimp2lem5  49777  zlmodzxznm  49812