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  pm2.51  166  dfbi1ALT  204  pm5.1im  253  biimt  349  pm5.4  376  pm4.8  379  simplOLD  469  pm4.45im  825  jao1i  847  olc  857  biort  921  pm5.14  931  oibabs  936  pm2.74  959  dedlem0a  1028  meredith  1714  tbw-bijust  1771  tbw-negdf  1772  tbw-ax2  1774  merco1  1786  nftht  1866  ala1  1889  exa1  1913  ax13b  2120  sbi2  2540  ax12vALT  2575  eumo  2647  moa1  2670  euim  2672  r19.12  3211  r19.27v  3218  r19.37  3234  eqvincg  3479  rr19.3v  3496  invdisjrab  4774  class2seteq  4965  dvdemo2  5032  iunopeqop  5115  asymref2  5653  elfv2ex  6372  elovmpt3imp  7040  sorpssuni  7096  sorpssint  7097  dfwe2  7131  ordunisuc2  7194  tfindsg  7210  findsg  7243  smo11  7617  omex  8707  r111  8805  kmlem12  9188  ltlen  10343  squeeze0  11131  elnnnn0b  11543  nn0ge2m1nn  11566  nn0lt10b  11645  znnn0nn  11695  iccneg  12499  hashfzp1  13419  hash2prde  13453  hash2pwpr  13459  hashge2el2dif  13463  scshwfzeqfzo  13780  relexprel  13986  algcvgblem  15497  prm23ge5  15726  prmgaplem5  15965  prmgaplem6  15966  cshwshashlem1  16008  dfgrp2e  17655  gsmtrcl  18142  prmirred  20057  symgmatr01lem  20677  pmatcollpw3fi1  20812  cxpcn2  24707  rpdmgm  24971  bpos1  25228  2lgs  25352  umgrislfupgrlem  26237  uhgr2edg  26321  nbusgrvtxm1  26503  uvtx01vtx  26524  uvtxa01vtx0OLD  26526  g0wlk0  26782  wlkonl1iedg  26795  wlkreslem  26800  crctcshwlkn0lem5  26941  0enwwlksnge1  26997  clwwlknonex2lem2  27283  frgr3vlem2  27455  frgrnbnb  27474  frgrregord013  27593  frgrogt3nreg  27595  2bornot2b  27661  stcltr2i  29473  mdsl1i  29519  prsiga  30533  logdivsqrle  31067  bnj1533  31259  bnj1176  31410  jath  31946  idinside  32527  tb-ax2  32715  bj-a1k  32871  bj-imim2ALT  32873  pm4.81ALT  32882  bj-andnotim  32909  bj-ssbeq  32964  bj-ssb0  32965  bj-ssb1a  32969  bj-eqs  32999  bj-stdpc4v  33089  bj-dvdemo2  33138  tsim3  34270  mpt2bi123f  34302  mptbi12f  34306  ac6s6  34311  ax12fromc15  34712  axc5c7toc5  34719  axc5c711toc5  34726  ax12f  34747  ax12eq  34748  ax12el  34749  ax12indi  34751  ax12indalem  34752  ax12inda2ALT  34753  ax12inda2  34754  atpsubN  35561  ifpim23g  38366  rp-fakeimass  38383  inintabss  38410  ntrneiiso  38915  axc5c4c711toc5  39129  axc5c4c711toc4  39130  axc5c4c711toc7  39131  axc5c4c711to11  39132  pm2.43bgbi  39248  pm2.43cbi  39249  hbimpg  39295  hbimpgVD  39662  ax6e2ndeqVD  39667  ax6e2ndeqALT  39689  ralimralim  39774  confun  41623  confun5  41627  iccpartnel  41899  fmtno4prmfac193  42010  prminf2  42025  zeo2ALTV  42107  sbgoldbaltlem1  42192  nzerooringczr  42597  islinindfis  42763  lindslinindsimp2lem5  42776  zlmodzxznm  42811