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  213  pm5.1im  262  biimt  359  pm4.8  391  pm4.45im  826  pm5.31r  830  jao1i  856  olc  866  oibabs  949  pm2.74  972  tarski-bernays-ax2  1635  meredith  1636  tbw-bijust  1693  tbw-negdf  1694  tbw-ax2  1696  merco1  1708  nftht  1787  ala1  1808  exa1  1833  ax13b  2028  sbi2  2292  ax12vALT  2463  moabs  2532  moa1  2540  r19.35  3098  r19.35OLD  3099  r19.21v  3170  r19.37  3250  r19.12OLD  3303  eqvincg  3632  rr19.3v  3653  class2seteq  3697  ralidmw  4502  ralidm  4506  invdisjrab  5131  dvdemo2  5370  iunopeqop  5519  po2ne  5602  asymref2  6121  elfv2ex  6939  elovmpt3imp  7675  sorpssuni  7735  dfwe2  7774  ordunisuc2  7846  xpord3ind  8162  smo11  8386  omex  9679  r111  9811  kmlem12  10197  squeeze0  12163  nn0ge2m1nn  12587  nn0lt10b  12670  iccneg  13497  hashfzp1  14443  hash2prde  14484  hash2pwpr  14490  hashge2el2dif  14494  relexprel  15039  algcvgblem  16573  prm23ge5  16812  cshwshashlem1  17093  dfgrp2e  18953  gsmtrcl  19510  nzerooringczr  21466  symgmatr01lem  22643  cxpcn2  26771  logbgcd1irr  26819  rpdmgm  27050  bpos1  27309  2lgs  27433  2sqnn0  27464  umgrislfupgrlem  29055  uhgr2edg  29141  nbusgrvtxm1  29312  uvtx01vtx  29330  g0wlk0  29586  wlkonl1iedg  29599  wlkreslem  29603  crctcshwlkn0lem5  29745  0enwwlksnge1  29795  clwwlknonex2lem2  30038  frgr3vlem2  30204  frgrnbnb  30223  frgrregord013  30325  frgrogt3nreg  30327  2bornot2b  30394  stcltr2i  32205  mdsl1i  32251  prsiga  33977  logdivsqrle  34509  bnj1533  34710  bnj1176  34863  jath  35560  idinside  35921  tb-ax2  36109  bj-a1k  36260  bj-peircestab  36269  bj-currypeirce  36273  bj-andnotim  36306  bj-ssbeq  36370  bj-eqs  36392  bj-nnftht  36459  curryset  36666  currysetlem3  36669  wl-moae  37224  tsim3  37846  mpobi123f  37876  mptbi12f  37880  ac6s6  37886  ax12fromc15  38616  axc5c7toc5  38623  axc5c711toc5  38630  ax12f  38651  ax12eq  38652  ax12el  38653  ax12indi  38655  ax12indalem  38656  ax12inda2ALT  38657  ax12inda2  38658  atpsubN  39465  ifpim23g  43199  rp-fakeimass  43216  inintabss  43282  ntrneiiso  43795  spALT  43905  axc5c4c711toc5  44113  axc5c4c711toc4  44114  axc5c4c711toc7  44115  axc5c4c711to11  44116  pm2.43bgbi  44230  pm2.43cbi  44231  hbimpg  44267  hbimpgVD  44617  ax6e2ndeqVD  44622  ax6e2ndeqALT  44644  ralimralim  44719  confun  46590  confun5  46594  adh-jarrsc  46651  adh-minim  46652  adh-minimp  46664  f1cof1b  46726  iccpartnel  47046  fmtno4prmfac193  47181  prminf2  47196  zeo2ALTV  47279  fpprbasnn  47337  sbgoldbaltlem1  47387  uspgrimprop  47488  islinindfis  47868  lindslinindsimp2lem5  47881  zlmodzxznm  47916