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  2065  sbrimvw  2128  sbi2  2337  ax12vALT  2500  moabs  2570  moa1  2578  r19.35  3122  r19.21v  3189  r19.37  3267  eqvincg  3605  rr19.3v  3624  class2seteq  3665  r19.3rzv  4462  ralidmw  4475  ralidm  4476  dvdemo2  5343  iunopeqop  5502  iunopeqopOLD  5503  po2ne  5583  asymref2  6115  elfv2ex  6925  elovmpt3imp  7674  sorpssuni  7736  xpord3ind  8157  omex  9625  kmlem12  10167  squeeze0  12143  nn0ge2m1nn  12599  nn0lt10b  12684  iccneg  13525  hashfzp1  14496  hash2prde  14535  hash2pwpr  14541  hashge2el2dif  14545  hash3tpde  14558  relexprel  15112  algcvgblem  16669  prm23ge5  16909  cshwshashlem1  17189  dfgrp2e  19086  gsmtrcl  19642  nzerooringczr  21692  symgmatr01lem  22874  cxpcn2  26979  logbgcd1irr  27027  rpdmgm  27257  bpos1  27515  2lgs  27639  umgrislfupgrlem  29563  uhgr2edg  29652  nbusgrvtxm1  29823  uvtx01vtx  29841  g0wlk0  30094  wlkonl1iedg  30107  wlkreslem  30111  crctcshwlkn0lem5  30266  0enwwlksnge1  30316  clwwlknonex2lem2  30562  frgr3vlem2  30738  frgrnbnb  30757  frgrregord013  30859  frgrogt3nreg  30861  2bornot2b  30928  stcltr2i  32740  mdsl1i  32786  prsiga  34626  logdivsqrle  35143  bnj1533  35346  bnj1176  35499  axprALT2  35602  onvf1odlem1  35685  jath  36289  idinside  36649  tb-ax2  36988  bj-peircestab  37236  bj-currypeirce  37242  bj-andnotim  37274  bj-ssbeq  37368  bj-eqs  37391  bj-alnnf  37455  curryset  37675  currysetlem3  37678  wl-moae  38264  tsim3  38865  mpobi123f  38895  mptbi12f  38899  ac6s6  38905  ax12fromc15  39763  axc5c7toc5  39770  axc5c711toc5  39777  ax12f  39798  ax12eq  39799  ax12el  39800  ax12indi  39802  ax12indalem  39803  ax12inda2ALT  39804  ax12inda2  39805  atpsubN  40611  ifpim23g  44320  rp-fakeimass  44337  inintabss  44403  ntrneiiso  44916  spALT  45026  axc5c4c711toc5  45211  axc5c4c711toc4  45212  axc5c4c711toc7  45213  axc5c4c711to11  45214  pm2.43bgbi  45325  pm2.43cbi  45326  hbimpg  45362  hbimpgVD  45711  ax6e2ndeqVD  45716  ax6e2ndeqALT  45738  dfbi1ALTa  45747  simprimi  45748  ralimralim  45900  confun  47812  confun5  47816  adh-jarrsc  47873  adh-minim  47874  adh-minimp  47886  f1cof1b  47950  iccpartnel  48323  fmtno4prmfac193  48461  prminf2  48476  zeo2ALTV  48572  fpprbasnn  48630  sbgoldbaltlem1  48680  pgnbgreunbgrlem2lem1  49015  pgnbgreunbgrlem2lem2  49016  pgnbgreunbgrlem2lem3  49017  islinindfis  49364  lindslinindsimp2lem5  49377  zlmodzxznm  49412