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  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  397  pm4.45im  840  pm5.31r  844  jao1i  871  olc  881  oibabs  966  pm2.74  990  tarski-bernays-ax2  1668  meredith  1669  tbw-bijust  1726  tbw-negdf  1727  tbw-ax2  1729  merco1  1741  nftht  1820  ala1  1841  exa1  1866  ax13b  2060  sbrimvw  2123  sbi2  2335  ax12vALT  2499  moabs  2569  moa1  2577  r19.35  3121  r19.21v  3188  r19.37  3266  eqvincg  3606  rr19.3v  3625  class2seteq  3666  r19.3rzv  4463  ralidmw  4476  ralidm  4477  dvdemo2  5345  iunopeqop  5504  iunopeqopOLD  5505  po2ne  5585  asymref2  6117  elfv2ex  6924  elovmpt3imp  7667  sorpssuni  7729  xpord3ind  8151  omex  9611  kmlem12  10144  squeeze0  12117  nn0ge2m1nn  12573  nn0lt10b  12657  iccneg  13498  hashfzp1  14467  hash2prde  14506  hash2pwpr  14512  hashge2el2dif  14516  hash3tpde  14529  relexprel  15075  algcvgblem  16634  prm23ge5  16874  cshwshashlem1  17154  dfgrp2e  19029  gsmtrcl  19585  nzerooringczr  21609  symgmatr01lem  22789  cxpcn2  26887  logbgcd1irr  26935  rpdmgm  27165  bpos1  27423  2lgs  27547  umgrislfupgrlem  29438  uhgr2edg  29524  nbusgrvtxm1  29695  uvtx01vtx  29713  g0wlk0  29966  wlkonl1iedg  29979  wlkreslem  29983  crctcshwlkn0lem5  30129  0enwwlksnge1  30179  clwwlknonex2lem2  30425  frgr3vlem2  30591  frgrnbnb  30610  frgrregord013  30712  frgrogt3nreg  30714  2bornot2b  30781  stcltr2i  32593  mdsl1i  32639  prsiga  34487  logdivsqrle  35003  bnj1533  35206  bnj1176  35359  axprALT2  35467  onvf1odlem1  35541  jath  36171  idinside  36530  tb-ax2  36839  bj-peircestab  37087  bj-currypeirce  37093  bj-andnotim  37125  bj-ssbeq  37219  bj-eqs  37242  bj-alnnf  37306  curryset  37526  currysetlem3  37529  wl-moae  38115  tsim3  38727  mpobi123f  38757  mptbi12f  38761  ac6s6  38767  ax12fromc15  39625  axc5c7toc5  39632  axc5c711toc5  39639  ax12f  39660  ax12eq  39661  ax12el  39662  ax12indi  39664  ax12indalem  39665  ax12inda2ALT  39666  ax12inda2  39667  atpsubN  40473  ifpim23g  44169  rp-fakeimass  44186  inintabss  44252  ntrneiiso  44765  spALT  44875  axc5c4c711toc5  45060  axc5c4c711toc4  45061  axc5c4c711toc7  45062  axc5c4c711to11  45063  pm2.43bgbi  45174  pm2.43cbi  45175  hbimpg  45211  hbimpgVD  45560  ax6e2ndeqVD  45565  ax6e2ndeqALT  45587  dfbi1ALTa  45596  simprimi  45597  ralimralim  45749  confun  47621  confun5  47625  adh-jarrsc  47682  adh-minim  47683  adh-minimp  47695  f1cof1b  47759  iccpartnel  48132  fmtno4prmfac193  48270  prminf2  48285  zeo2ALTV  48381  fpprbasnn  48439  sbgoldbaltlem1  48489  pgnbgreunbgrlem2lem1  48824  pgnbgreunbgrlem2lem2  48825  pgnbgreunbgrlem2lem3  48826  islinindfis  49174  lindslinindsimp2lem5  49187  zlmodzxznm  49222