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  213  pm5.1im  262  biimt  361  pm4.8  393  pm4.45im  825  pm5.31r  829  jao1i  855  olc  865  oibabs  949  pm2.74  972  tarski-bernays-ax2  1643  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  tbw-ax2  1704  merco1  1716  nftht  1795  ala1  1816  exa1  1840  ax13b  2035  sbi2  2299  ax12vALT  2469  moabs  2543  moa1  2551  r19.21v  3113  r19.12OLD  3258  r19.35  3271  r19.37  3273  eqvincg  3578  rr19.3v  3598  ss2abdv  3997  ralidmw  4438  ralidm  4442  invdisjrab  5060  class2seteq  5277  dvdemo2  5297  iunopeqop  5435  po2ne  5519  asymref2  6022  elfv2ex  6815  elovmpt3imp  7526  sorpssuni  7585  dfwe2  7624  ordunisuc2  7691  smo11  8195  omex  9401  r111  9533  kmlem12  9917  squeeze0  11878  nn0ge2m1nn  12302  nn0lt10b  12382  iccneg  13204  hashfzp1  14146  hash2prde  14184  hash2pwpr  14190  hashge2el2dif  14194  relexprel  14750  algcvgblem  16282  prm23ge5  16516  cshwshashlem1  16797  dfgrp2e  18605  gsmtrcl  19124  symgmatr01lem  21802  cxpcn2  25899  logbgcd1irr  25944  rpdmgm  26174  bpos1  26431  2lgs  26555  2sqnn0  26586  umgrislfupgrlem  27492  uhgr2edg  27575  nbusgrvtxm1  27746  uvtx01vtx  27764  g0wlk0  28019  wlkonl1iedg  28033  wlkreslem  28037  crctcshwlkn0lem5  28179  0enwwlksnge1  28229  clwwlknonex2lem2  28472  frgr3vlem2  28638  frgrnbnb  28657  frgrregord013  28759  frgrogt3nreg  28761  2bornot2b  28828  stcltr2i  30637  mdsl1i  30683  prsiga  32099  logdivsqrle  32630  bnj1533  32832  bnj1176  32985  jath  33672  idinside  34386  tb-ax2  34573  bj-a1k  34724  bj-peircestab  34733  bj-currypeirce  34737  bj-andnotim  34770  bj-ssbeq  34834  bj-eqs  34856  bj-nnftht  34923  curryset  35135  currysetlem3  35138  wl-moae  35675  tsim3  36290  mpobi123f  36320  mptbi12f  36324  ac6s6  36330  ax12fromc15  36919  axc5c7toc5  36926  axc5c711toc5  36933  ax12f  36954  ax12eq  36955  ax12el  36956  ax12indi  36958  ax12indalem  36959  ax12inda2ALT  36960  ax12inda2  36961  atpsubN  37767  ifpim23g  41102  rp-fakeimass  41119  inintabss  41186  ntrneiiso  41701  spALT  41812  axc5c4c711toc5  42020  axc5c4c711toc4  42021  axc5c4c711toc7  42022  axc5c4c711to11  42023  pm2.43bgbi  42137  pm2.43cbi  42138  hbimpg  42174  hbimpgVD  42524  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  ralimralim  42631  confun  44434  confun5  44438  adh-jarrsc  44495  adh-minim  44496  adh-minimp  44508  f1cof1b  44569  iccpartnel  44890  fmtno4prmfac193  45025  prminf2  45040  zeo2ALTV  45123  fpprbasnn  45181  sbgoldbaltlem1  45231  nzerooringczr  45630  islinindfis  45790  lindslinindsimp2lem5  45803  zlmodzxznm  45838