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  1672  meredith  1673  tbw-bijust  1730  tbw-negdf  1731  tbw-ax2  1733  merco1  1745  nftht  1824  ala1  1845  exa1  1870  ax13b  2064  sbrimvw  2127  sbi2  2335  ax12vALT  2498  moabs  2568  moa1  2576  r19.35  3120  r19.21v  3187  r19.37  3265  eqvincg  3601  rr19.3v  3620  class2seteq  3661  r19.3rzv  4458  ralidmw  4471  ralidm  4472  dvdemo2  5335  iunopeqop  5493  iunopeqopOLD  5494  po2ne  5574  asymref2  6110  elfv2ex  6928  elovmpt3imp  7678  sorpssuni  7748  xpord3ind  8173  omex  9644  kmlem12  10240  squeeze0  12220  nn0ge2m1nn  12676  nn0lt10b  12761  iccneg  13603  hashfzp1  14576  hash2prde  14615  hash2pwpr  14621  hashge2el2dif  14625  hash3tpde  14638  relexprel  15192  algcvgblem  16752  prm23ge5  16993  cshwshashlem1  17273  dfgrp2e  19174  gsmtrcl  19730  nzerooringczr  21786  symgmatr01lem  22968  cxpcn2  27074  logbgcd1irr  27122  rpdmgm  27352  bpos1  27610  2lgs  27734  umgrislfupgrlem  29700  uhgr2edg  29789  nbusgrvtxm1  29960  uvtx01vtx  29978  g0wlk0  30231  wlkonl1iedg  30244  wlkreslem  30248  crctcshwlkn0lem5  30403  0enwwlksnge1  30453  clwwlknonex2lem2  30699  frgr3vlem2  30875  frgrnbnb  30894  frgrregord013  30996  frgrogt3nreg  30998  2bornot2b  31065  stcltr2i  32877  mdsl1i  32923  prsiga  34805  logdivsqrle  35321  bnj1533  35524  bnj1176  35677  axprALT2  35776  onvf1odlem1  35924  jath  36532  idinside  36891  tb-ax2  37214  bj-peircestab  37462  bj-currypeirce  37468  bj-andnotim  37500  bj-ssbeq  37594  bj-eqs  37617  bj-alnnf  37681  curryset  37901  currysetlem3  37904  wl-moae  38491  tsim3  39107  mpobi123f  39137  mptbi12f  39141  ac6s6  39147  ax12fromc15  40005  axc5c7toc5  40012  axc5c711toc5  40019  ax12f  40040  ax12eq  40041  ax12el  40042  ax12indi  40044  ax12indalem  40045  ax12inda2ALT  40046  ax12inda2  40047  atpsubN  40853  ifpim23g  44538  rp-fakeimass  44555  inintabss  44621  ntrneiiso  45133  spALT  45243  axc5c4c711toc5  45428  axc5c4c711toc4  45429  axc5c4c711toc7  45430  axc5c4c711to11  45431  pm2.43bgbi  45542  pm2.43cbi  45543  hbimpg  45579  hbimpgVD  45928  ax6e2ndeqVD  45933  ax6e2ndeqALT  45955  dfbi1ALTa  45971  simprimi  45972  ralimralim  46140  confun  48051  confun5  48055  adh-jarrsc  48112  adh-minim  48113  adh-minimp  48125  f1cof1b  48189  iccpartnel  48562  fmtno4prmfac193  48700  prminf2  48715  zeo2ALTV  48811  fpprbasnn  48869  sbgoldbaltlem1  48919  pgnbgreunbgrlem2lem1  49254  pgnbgreunbgrlem2lem2  49255  pgnbgreunbgrlem2lem3  49256  islinindfis  49603  lindslinindsimp2lem5  49616  zlmodzxznm  49651