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  173  dfbi1ALT  217  pm5.1im  266  biimt  364  pm4.8  396  pm4.45im  828  pm5.31r  832  jao1i  858  olc  868  oibabs  952  pm2.74  975  tarski-bernays-ax2  1648  meredith  1649  tbw-bijust  1706  tbw-negdf  1707  tbw-ax2  1709  merco1  1721  nftht  1800  ala1  1821  exa1  1845  ax13b  2040  sbi2  2305  ax12vALT  2470  moabs  2544  moa1  2552  r19.12OLD  3255  r19.35  3270  r19.37  3272  eqvincg  3571  rr19.3v  3592  ss2abdv  3994  ralidmw  4436  ralidm  4440  invdisjrab  5056  class2seteq  5270  dvdemo2  5291  iunopeqop  5428  po2ne  5509  asymref2  6010  elfv2ex  6794  elovmpt3imp  7501  sorpssuni  7560  dfwe2  7599  ordunisuc2  7663  smo11  8143  omex  9306  r111  9439  kmlem12  9823  squeeze0  11783  nn0ge2m1nn  12207  nn0lt10b  12287  iccneg  13108  hashfzp1  14049  hash2prde  14087  hash2pwpr  14093  hashge2el2dif  14097  relexprel  14653  algcvgblem  16185  prm23ge5  16419  cshwshashlem1  16700  dfgrp2e  18495  gsmtrcl  19014  symgmatr01lem  21685  cxpcn2  25779  logbgcd1irr  25824  rpdmgm  26054  bpos1  26311  2lgs  26435  2sqnn0  26466  umgrislfupgrlem  27370  uhgr2edg  27453  nbusgrvtxm1  27624  uvtx01vtx  27642  g0wlk0  27896  wlkonl1iedg  27910  wlkreslem  27914  crctcshwlkn0lem5  28055  0enwwlksnge1  28105  clwwlknonex2lem2  28348  frgr3vlem2  28514  frgrnbnb  28533  frgrregord013  28635  frgrogt3nreg  28637  2bornot2b  28704  stcltr2i  30513  mdsl1i  30559  prsiga  31974  logdivsqrle  32505  bnj1533  32707  bnj1176  32860  jath  33549  idinside  34288  tb-ax2  34475  bj-a1k  34626  bj-peircestab  34635  bj-currypeirce  34639  bj-andnotim  34672  bj-ssbeq  34736  bj-eqs  34758  bj-nnftht  34825  curryset  35037  currysetlem3  35040  wl-moae  35581  tsim3  36196  mpobi123f  36226  mptbi12f  36230  ac6s6  36236  ax12fromc15  36825  axc5c7toc5  36832  axc5c711toc5  36839  ax12f  36860  ax12eq  36861  ax12el  36862  ax12indi  36864  ax12indalem  36865  ax12inda2ALT  36866  ax12inda2  36867  atpsubN  37673  ifpim23g  40972  rp-fakeimass  40989  inintabss  41047  ntrneiiso  41563  spALT  41674  axc5c4c711toc5  41882  axc5c4c711toc4  41883  axc5c4c711toc7  41884  axc5c4c711to11  41885  pm2.43bgbi  41999  pm2.43cbi  42000  hbimpg  42036  hbimpgVD  42386  ax6e2ndeqVD  42391  ax6e2ndeqALT  42413  ralimralim  42493  confun  44294  confun5  44298  adh-jarrsc  44355  adh-minim  44356  adh-minimp  44368  f1cof1b  44429  iccpartnel  44751  fmtno4prmfac193  44886  prminf2  44901  zeo2ALTV  44984  fpprbasnn  45042  sbgoldbaltlem1  45092  nzerooringczr  45491  islinindfis  45651  lindslinindsimp2lem5  45664  zlmodzxznm  45699