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  827  pm5.31r  831  jao1i  857  olc  867  oibabs  952  pm2.74  975  tarski-bernays-ax2  1638  meredith  1639  tbw-bijust  1696  tbw-negdf  1697  tbw-ax2  1699  merco1  1711  nftht  1790  ala1  1811  exa1  1836  ax13b  2031  sbi2  2306  ax12vALT  2477  moabs  2546  moa1  2554  r19.35  3114  r19.35OLD  3115  r19.21v  3186  r19.37  3268  r19.12OLD  3321  eqvincg  3661  rr19.3v  3680  class2seteq  3726  ralidmw  4531  ralidm  4535  dvdemo2  5392  iunopeqop  5540  po2ne  5624  asymref2  6149  elfv2ex  6966  elovmpt3imp  7707  sorpssuni  7767  dfwe2  7809  ordunisuc2  7881  xpord3ind  8197  smo11  8420  omex  9712  r111  9844  kmlem12  10231  squeeze0  12198  nn0ge2m1nn  12622  nn0lt10b  12705  iccneg  13532  hashfzp1  14480  hash2prde  14519  hash2pwpr  14525  hashge2el2dif  14529  hash3tpde  14542  relexprel  15088  algcvgblem  16624  prm23ge5  16862  cshwshashlem1  17143  dfgrp2e  19003  gsmtrcl  19558  nzerooringczr  21514  symgmatr01lem  22680  cxpcn2  26807  logbgcd1irr  26855  rpdmgm  27086  bpos1  27345  2lgs  27469  2sqnn0  27500  umgrislfupgrlem  29157  uhgr2edg  29243  nbusgrvtxm1  29414  uvtx01vtx  29432  g0wlk0  29688  wlkonl1iedg  29701  wlkreslem  29705  crctcshwlkn0lem5  29847  0enwwlksnge1  29897  clwwlknonex2lem2  30140  frgr3vlem2  30306  frgrnbnb  30325  frgrregord013  30427  frgrogt3nreg  30429  2bornot2b  30496  stcltr2i  32307  mdsl1i  32353  prsiga  34095  logdivsqrle  34627  bnj1533  34828  bnj1176  34981  jath  35687  idinside  36048  tb-ax2  36350  bj-a1k  36510  bj-peircestab  36519  bj-currypeirce  36523  bj-andnotim  36554  bj-ssbeq  36619  bj-eqs  36641  bj-nnftht  36707  curryset  36912  currysetlem3  36915  wl-moae  37470  tsim3  38092  mpobi123f  38122  mptbi12f  38126  ac6s6  38132  ax12fromc15  38861  axc5c7toc5  38868  axc5c711toc5  38875  ax12f  38896  ax12eq  38897  ax12el  38898  ax12indi  38900  ax12indalem  38901  ax12inda2ALT  38902  ax12inda2  38903  atpsubN  39710  ifpim23g  43457  rp-fakeimass  43474  inintabss  43540  ntrneiiso  44053  spALT  44163  axc5c4c711toc5  44371  axc5c4c711toc4  44372  axc5c4c711toc7  44373  axc5c4c711to11  44374  pm2.43bgbi  44488  pm2.43cbi  44489  hbimpg  44525  hbimpgVD  44875  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  ralimralim  44983  confun  46854  confun5  46858  adh-jarrsc  46915  adh-minim  46916  adh-minimp  46928  f1cof1b  46992  iccpartnel  47312  fmtno4prmfac193  47447  prminf2  47462  zeo2ALTV  47545  fpprbasnn  47603  sbgoldbaltlem1  47653  uspgrimprop  47757  islinindfis  48178  lindslinindsimp2lem5  48191  zlmodzxznm  48226