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  216  pm5.1im  265  biimt  362  pm4.8  396  pm4.45im  838  pm5.31r  842  jao1i  869  olc  879  oibabs  964  pm2.74  988  tarski-bernays-ax2  1662  meredith  1663  tbw-bijust  1720  tbw-negdf  1721  tbw-ax2  1723  merco1  1735  nftht  1814  ala1  1835  exa1  1860  ax13b  2054  sbrimvw  2126  sbi2  2338  ax12vALT  2502  moabs  2572  moa1  2580  r19.35  3122  r19.21v  3189  r19.37  3267  eqvincg  3609  rr19.3v  3628  class2seteq  3669  r19.3rzv  4459  ralidmw  4472  ralidm  4473  dvdemo2  5333  iunopeqop  5492  iunopeqopOLD  5493  po2ne  5573  asymref2  6106  elfv2ex  6912  elovmpt3imp  7655  sorpssuni  7717  dfwe2  7759  ordunisuc2  7826  xpord3ind  8138  smo11  8337  omex  9600  r111  9735  kmlem12  10120  squeeze0  12097  nn0ge2m1nn  12553  nn0lt10b  12637  iccneg  13478  hashfzp1  14446  hash2prde  14485  hash2pwpr  14491  hashge2el2dif  14495  hash3tpde  14508  relexprel  15054  algcvgblem  16613  prm23ge5  16853  cshwshashlem1  17133  dfgrp2e  19007  gsmtrcl  19558  nzerooringczr  21534  symgmatr01lem  22715  cxpcn2  26813  logbgcd1irr  26861  rpdmgm  27091  bpos1  27349  2lgs  27473  2sqnn0  27504  umgrislfupgrlem  29325  uhgr2edg  29411  nbusgrvtxm1  29582  uvtx01vtx  29600  g0wlk0  29853  wlkonl1iedg  29866  wlkreslem  29870  crctcshwlkn0lem5  30016  0enwwlksnge1  30066  clwwlknonex2lem2  30312  frgr3vlem2  30478  frgrnbnb  30497  frgrregord013  30599  frgrogt3nreg  30601  2bornot2b  30668  stcltr2i  32480  mdsl1i  32526  prsiga  34430  logdivsqrle  34946  bnj1533  35149  bnj1176  35302  axprALT2  35409  onvf1odlem1  35450  jath  36080  idinside  36439  tb-ax2  36749  bj-a1k  36987  bj-peircestab  36998  bj-currypeirce  37004  bj-andnotim  37036  bj-ssbeq  37130  bj-eqs  37153  bj-alnnf  37217  curryset  37436  currysetlem3  37439  wl-moae  38024  tsim3  38636  mpobi123f  38666  mptbi12f  38670  ac6s6  38676  ax12fromc15  39534  axc5c7toc5  39541  axc5c711toc5  39548  ax12f  39569  ax12eq  39570  ax12el  39571  ax12indi  39573  ax12indalem  39574  ax12inda2ALT  39575  ax12inda2  39576  atpsubN  40382  ifpim23g  44076  rp-fakeimass  44093  inintabss  44159  ntrneiiso  44672  spALT  44782  axc5c4c711toc5  44983  axc5c4c711toc4  44984  axc5c4c711toc7  44985  axc5c4c711to11  44986  pm2.43bgbi  45098  pm2.43cbi  45099  hbimpg  45135  hbimpgVD  45484  ax6e2ndeqVD  45489  ax6e2ndeqALT  45511  dfbi1ALTa  45520  simprimi  45521  ralimralim  45666  confun  47538  confun5  47542  adh-jarrsc  47599  adh-minim  47600  adh-minimp  47612  f1cof1b  47676  iccpartnel  48049  fmtno4prmfac193  48187  prminf2  48202  zeo2ALTV  48298  fpprbasnn  48356  sbgoldbaltlem1  48406  elclnbgrelnbgr  48452  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem2lem3  48743  islinindfis  49076  lindslinindsimp2lem5  49089  zlmodzxznm  49124