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  1673  meredith  1674  tbw-bijust  1731  tbw-negdf  1732  tbw-ax2  1734  merco1  1746  nftht  1825  ala1  1846  exa1  1871  ax13b  2065  sbrimvw  2128  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  5490  iunopeqopOLD  5491  po2ne  5571  asymref2  6105  elfv2ex  6916  elovmpt3imp  7666  sorpssuni  7731  xpord3ind  8151  omex  9622  kmlem12  10211  squeeze0  12189  nn0ge2m1nn  12645  nn0lt10b  12730  iccneg  13572  hashfzp1  14543  hash2prde  14582  hash2pwpr  14588  hashge2el2dif  14592  hash3tpde  14605  relexprel  15159  algcvgblem  16714  prm23ge5  16954  cshwshashlem1  17234  dfgrp2e  19135  gsmtrcl  19691  nzerooringczr  21747  symgmatr01lem  22929  cxpcn2  27037  logbgcd1irr  27085  rpdmgm  27315  bpos1  27573  2lgs  27697  umgrislfupgrlem  29633  uhgr2edg  29722  nbusgrvtxm1  29893  uvtx01vtx  29911  g0wlk0  30164  wlkonl1iedg  30177  wlkreslem  30181  crctcshwlkn0lem5  30336  0enwwlksnge1  30386  clwwlknonex2lem2  30632  frgr3vlem2  30808  frgrnbnb  30827  frgrregord013  30929  frgrogt3nreg  30931  2bornot2b  30998  stcltr2i  32810  mdsl1i  32856  prsiga  34696  logdivsqrle  35213  bnj1533  35416  bnj1176  35569  axprALT2  35664  onvf1odlem1  35807  jath  36411  idinside  36771  tb-ax2  37094  bj-peircestab  37342  bj-currypeirce  37348  bj-andnotim  37380  bj-ssbeq  37474  bj-eqs  37497  bj-alnnf  37561  curryset  37781  currysetlem3  37784  wl-moae  38368  tsim3  38984  mpobi123f  39014  mptbi12f  39018  ac6s6  39024  ax12fromc15  39882  axc5c7toc5  39889  axc5c711toc5  39896  ax12f  39917  ax12eq  39918  ax12el  39919  ax12indi  39921  ax12indalem  39922  ax12inda2ALT  39923  ax12inda2  39924  atpsubN  40730  ifpim23g  44439  rp-fakeimass  44456  inintabss  44522  ntrneiiso  45035  spALT  45145  axc5c4c711toc5  45330  axc5c4c711toc4  45331  axc5c4c711toc7  45332  axc5c4c711to11  45333  pm2.43bgbi  45444  pm2.43cbi  45445  hbimpg  45481  hbimpgVD  45830  ax6e2ndeqVD  45835  ax6e2ndeqALT  45857  dfbi1ALTa  45866  simprimi  45867  ralimralim  46019  confun  47931  confun5  47935  adh-jarrsc  47992  adh-minim  47993  adh-minimp  48005  f1cof1b  48069  iccpartnel  48442  fmtno4prmfac193  48580  prminf2  48595  zeo2ALTV  48691  fpprbasnn  48749  sbgoldbaltlem1  48799  pgnbgreunbgrlem2lem1  49134  pgnbgreunbgrlem2lem2  49135  pgnbgreunbgrlem2lem3  49136  islinindfis  49483  lindslinindsimp2lem5  49496  zlmodzxznm  49531