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  828  pm5.31r  832  jao1i  859  olc  869  oibabs  954  pm2.74  977  tarski-bernays-ax2  1642  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  tbw-ax2  1703  merco1  1715  nftht  1794  ala1  1815  exa1  1840  ax13b  2034  sbi2  2309  ax12vALT  2474  moabs  2544  moa1  2552  r19.35  3096  r19.21v  3163  r19.37  3241  eqvincg  3591  rr19.3v  3610  class2seteq  3651  r19.3rzv  4444  ralidmw  4457  ralidm  4458  dvdemo2  5315  iunopeqop  5473  po2ne  5552  asymref2  6078  elfv2ex  6881  elovmpt3imp  7621  sorpssuni  7683  dfwe2  7725  ordunisuc2  7792  xpord3ind  8103  smo11  8301  omex  9561  r111  9696  kmlem12  10081  squeeze0  12056  nn0ge2m1nn  12504  nn0lt10b  12588  iccneg  13422  hashfzp1  14390  hash2prde  14429  hash2pwpr  14435  hashge2el2dif  14439  hash3tpde  14452  relexprel  14998  algcvgblem  16543  prm23ge5  16783  cshwshashlem1  17063  dfgrp2e  18936  gsmtrcl  19488  nzerooringczr  21457  symgmatr01lem  22615  cxpcn2  26707  logbgcd1irr  26755  rpdmgm  26985  bpos1  27243  2lgs  27367  2sqnn0  27398  umgrislfupgrlem  29188  uhgr2edg  29274  nbusgrvtxm1  29445  uvtx01vtx  29463  g0wlk0  29716  wlkonl1iedg  29729  wlkreslem  29733  crctcshwlkn0lem5  29879  0enwwlksnge1  29929  clwwlknonex2lem2  30175  frgr3vlem2  30341  frgrnbnb  30360  frgrregord013  30462  frgrogt3nreg  30464  2bornot2b  30531  stcltr2i  32343  mdsl1i  32389  prsiga  34272  logdivsqrle  34791  bnj1533  34991  bnj1176  35144  axprALT2  35250  onvf1odlem1  35282  jath  35904  idinside  36263  tb-ax2  36563  bj-a1k  36801  bj-peircestab  36812  bj-currypeirce  36818  bj-andnotim  36850  bj-ssbeq  36944  bj-eqs  36967  bj-alnnf  37031  curryset  37250  currysetlem3  37253  wl-moae  37838  tsim3  38450  mpobi123f  38480  mptbi12f  38484  ac6s6  38490  ax12fromc15  39348  axc5c7toc5  39355  axc5c711toc5  39362  ax12f  39383  ax12eq  39384  ax12el  39385  ax12indi  39387  ax12indalem  39388  ax12inda2ALT  39389  ax12inda2  39390  atpsubN  40196  ifpim23g  43919  rp-fakeimass  43936  inintabss  44002  ntrneiiso  44515  spALT  44625  axc5c4c711toc5  44826  axc5c4c711toc4  44827  axc5c4c711toc7  44828  axc5c4c711to11  44829  pm2.43bgbi  44941  pm2.43cbi  44942  hbimpg  44978  hbimpgVD  45327  ax6e2ndeqVD  45332  ax6e2ndeqALT  45354  dfbi1ALTa  45363  simprimi  45364  ralimralim  45509  confun  47378  confun5  47382  adh-jarrsc  47439  adh-minim  47440  adh-minimp  47452  f1cof1b  47516  iccpartnel  47889  fmtno4prmfac193  48027  prminf2  48042  zeo2ALTV  48138  fpprbasnn  48196  sbgoldbaltlem1  48246  elclnbgrelnbgr  48292  pgnbgreunbgrlem2lem1  48581  pgnbgreunbgrlem2lem2  48582  pgnbgreunbgrlem2lem3  48583  islinindfis  48916  lindslinindsimp2lem5  48929  zlmodzxznm  48964