MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 wph . 2 wff 𝜑
2 wps . . 3 wff 𝜓
32, 1wi 4 . 2 wff (𝜓𝜑)
41, 3wi 4 1 wff (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
This axiom is referenced by:  a1i  11  id  22  idALT  23  a1d  25  a1dd  50  a1ddd  80  jarr  106  pm2.86d  107  pm2.86i  109  pm2.51  165  dfbi1ALT  204  pm5.1im  253  biimt  349  pm5.4  376  pm4.8  379  olc  398  simplOLD  475  pm4.45im  586  jao1i  860  pm2.74  927  oibabs  961  pm5.14  966  biort  974  dedlem0a  1030  meredith  1703  tbw-bijust  1760  tbw-negdf  1761  tbw-ax2  1763  merco1  1775  nftht  1855  ala1  1878  exa1  1902  ax13b  2103  ax12OLD  2469  sbi2  2518  ax12vALT  2553  eumo  2624  moa1  2647  euim  2649  r19.12  3189  r19.27v  3196  r19.37  3212  eqvincg  3456  rr19.3v  3473  invdisjrab  4779  class2seteq  4970  dvdemo2  5040  iunopeqop  5119  asymref2  5659  elfv2ex  6378  elovmpt3imp  7043  sorpssuni  7099  sorpssint  7100  dfwe2  7134  ordunisuc2  7197  tfindsg  7213  findsg  7246  smo11  7618  omex  8701  r111  8799  kmlem12  9146  ltlen  10301  squeeze0  11089  elnnnn0b  11500  nn0ge2m1nn  11523  nn0lt10b  11602  znnn0nn  11652  iccneg  12457  hashfzp1  13381  hash2prde  13415  hash2pwpr  13421  hashge2el2dif  13425  scshwfzeqfzo  13743  relexprel  13949  algcvgblem  15463  prm23ge5  15693  prmgaplem5  15932  prmgaplem6  15933  cshwshashlem1  15975  dfgrp2e  17620  gsmtrcl  18107  prmirred  20016  symgmatr01lem  20632  pmatcollpw3fi1  20766  cxpcn2  24657  rpdmgm  24921  bpos1  25178  2lgs  25302  umgrislfupgrlem  26187  uhgr2edg  26270  nbusgrvtxm1  26450  uvtx01vtx  26471  uvtxa01vtx0OLD  26473  g0wlk0  26729  wlkonl1iedg  26742  wlkreslem  26747  crctcshwlkn0lem5  26888  0enwwlksnge1  26944  clwwlknonex2lem2  27228  frgr3vlem2  27399  frgrnbnb  27418  frgrregord013  27534  frgrogt3nreg  27536  2bornot2b  27602  stcltr2i  29414  mdsl1i  29460  prsiga  30474  logdivsqrle  31008  bnj1533  31200  bnj1176  31351  jath  31887  idinside  32468  tb-ax2  32656  bj-a1k  32812  bj-imim2ALT  32815  pm4.81ALT  32823  bj-andnotim  32850  bj-ssbeq  32904  bj-ssb0  32905  bj-ssb1a  32909  bj-eqs  32940  bj-stdpc4v  33031  bj-dvdemo2  33080  wl-jarri  33570  tsim3  34221  mpt2bi123f  34253  mptbi12f  34257  ac6s6  34262  ax12fromc15  34663  axc5c7toc5  34670  axc5c711toc5  34677  ax12f  34698  ax12eq  34699  ax12el  34700  ax12indi  34702  ax12indalem  34703  ax12inda2ALT  34704  ax12inda2  34705  atpsubN  35511  ifpim23g  38311  rp-fakeimass  38328  inintabss  38355  ntrneiiso  38860  axc5c4c711toc5  39074  axc5c4c711toc4  39075  axc5c4c711toc7  39076  axc5c4c711to11  39077  pm2.43bgbi  39194  pm2.43cbi  39195  hbimpg  39241  hbimpgVD  39608  ax6e2ndeqVD  39613  ax6e2ndeqALT  39635  ralimralim  39721  confun  41581  confun5  41585  iccpartnel  41853  fmtno4prmfac193  41964  prminf2  41979  zeo2ALTV  42061  sbgoldbaltlem1  42146  nzerooringczr  42551  islinindfis  42717  lindslinindsimp2lem5  42730  zlmodzxznm  42765
  Copyright terms: Public domain W3C validator