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  1640  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  tbw-ax2  1701  merco1  1713  nftht  1792  ala1  1813  exa1  1838  ax13b  2032  sbi2  2302  ax12vALT  2468  moabs  2537  moa1  2545  r19.35  3089  r19.35OLD  3090  r19.21v  3159  r19.37  3241  eqvincg  3617  rr19.3v  3636  class2seteq  3678  ralidmw  4474  ralidm  4478  dvdemo2  5332  iunopeqop  5484  po2ne  5565  asymref2  6093  elfv2ex  6907  elovmpt3imp  7649  sorpssuni  7711  dfwe2  7753  ordunisuc2  7823  xpord3ind  8138  smo11  8336  omex  9603  r111  9735  kmlem12  10122  squeeze0  12093  nn0ge2m1nn  12519  nn0lt10b  12603  iccneg  13440  hashfzp1  14403  hash2prde  14442  hash2pwpr  14448  hashge2el2dif  14452  hash3tpde  14465  relexprel  15012  algcvgblem  16554  prm23ge5  16793  cshwshashlem1  17073  dfgrp2e  18902  gsmtrcl  19453  nzerooringczr  21397  symgmatr01lem  22547  cxpcn2  26663  logbgcd1irr  26711  rpdmgm  26942  bpos1  27201  2lgs  27325  2sqnn0  27356  umgrislfupgrlem  29056  uhgr2edg  29142  nbusgrvtxm1  29313  uvtx01vtx  29331  g0wlk0  29587  wlkonl1iedg  29600  wlkreslem  29604  crctcshwlkn0lem5  29751  0enwwlksnge1  29801  clwwlknonex2lem2  30044  frgr3vlem2  30210  frgrnbnb  30229  frgrregord013  30331  frgrogt3nreg  30333  2bornot2b  30400  stcltr2i  32211  mdsl1i  32257  prsiga  34128  logdivsqrle  34648  bnj1533  34849  bnj1176  35002  onvf1odlem1  35097  jath  35719  idinside  36079  tb-ax2  36379  bj-a1k  36539  bj-peircestab  36548  bj-currypeirce  36552  bj-andnotim  36583  bj-ssbeq  36648  bj-eqs  36670  bj-nnftht  36736  curryset  36941  currysetlem3  36944  wl-moae  37511  tsim3  38133  mpobi123f  38163  mptbi12f  38167  ac6s6  38173  ax12fromc15  38905  axc5c7toc5  38912  axc5c711toc5  38919  ax12f  38940  ax12eq  38941  ax12el  38942  ax12indi  38944  ax12indalem  38945  ax12inda2ALT  38946  ax12inda2  38947  atpsubN  39754  ifpim23g  43491  rp-fakeimass  43508  inintabss  43574  ntrneiiso  44087  spALT  44197  axc5c4c711toc5  44398  axc5c4c711toc4  44399  axc5c4c711toc7  44400  axc5c4c711to11  44401  pm2.43bgbi  44514  pm2.43cbi  44515  hbimpg  44551  hbimpgVD  44900  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  dfbi1ALTa  44936  simprimi  44937  ralimralim  45082  confun  46944  confun5  46948  adh-jarrsc  47005  adh-minim  47006  adh-minimp  47018  f1cof1b  47082  iccpartnel  47443  fmtno4prmfac193  47578  prminf2  47593  zeo2ALTV  47676  fpprbasnn  47734  sbgoldbaltlem1  47784  elclnbgrelnbgr  47830  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  islinindfis  48442  lindslinindsimp2lem5  48455  zlmodzxznm  48490