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  jarri  107  pm2.86d  108  conax1  173  dfbi1ALT  217  pm5.1im  266  biimt  364  pm4.8  396  pm4.45im  826  pm5.31r  830  jao1i  855  olc  865  oibabs  949  pm2.74  972  tarski-bernays-ax2  1642  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  tbw-ax2  1703  merco1  1715  nftht  1794  ala1  1815  exa1  1839  ax13b  2040  sbi2  2312  sbi2vOLD  2326  ax12vALT  2494  sbi2ALT  2609  moabs  2627  moa1  2636  euimOLD  2705  r19.27vOLD  3179  r19.12  3316  r19.35  3332  r19.37  3334  eqvincg  3626  rr19.3v  3644  invdisjrab  5033  class2seteq  5236  dvdemo2  5256  iunopeqop  5392  po2ne  5470  asymref2  5958  elfv2ex  6692  elovmpt3imp  7385  sorpssuni  7441  dfwe2  7479  ordunisuc2  7542  smo11  7984  omex  9090  r111  9188  kmlem12  9572  squeeze0  11528  nn0ge2m1nn  11950  nn0lt10b  12030  iccneg  12848  hashfzp1  13786  hash2prde  13822  hash2pwpr  13828  hashge2el2dif  13832  relexprel  14387  algcvgblem  15908  prm23ge5  16139  cshwshashlem1  16418  dfgrp2e  18118  gsmtrcl  18633  symgmatr01lem  21248  cxpcn2  25324  logbgcd1irr  25369  rpdmgm  25599  bpos1  25856  2lgs  25980  2sqnn0  26011  umgrislfupgrlem  26904  uhgr2edg  26987  nbusgrvtxm1  27158  uvtx01vtx  27176  g0wlk0  27430  wlkonl1iedg  27444  wlkreslem  27448  crctcshwlkn0lem5  27589  0enwwlksnge1  27639  clwwlknonex2lem2  27882  frgr3vlem2  28048  frgrnbnb  28067  frgrregord013  28169  frgrogt3nreg  28171  2bornot2b  28238  stcltr2i  30047  mdsl1i  30093  prsiga  31408  logdivsqrle  31939  bnj1533  32142  bnj1176  32295  jath  32976  idinside  33563  tb-ax2  33750  bj-a1k  33901  bj-peircestab  33906  bj-currypeirce  33910  bj-andnotim  33940  bj-ssbeq  34004  bj-eqs  34026  bj-nnftht  34089  curryset  34285  currysetlem3  34288  wl-moae  34821  tsim3  35470  mpobi123f  35500  mptbi12f  35504  ac6s6  35510  ax12fromc15  36101  axc5c7toc5  36108  axc5c711toc5  36115  ax12f  36136  ax12eq  36137  ax12el  36138  ax12indi  36140  ax12indalem  36141  ax12inda2ALT  36142  ax12inda2  36143  atpsubN  36949  ifpim23g  40035  rp-fakeimass  40052  inintabss  40110  ntrneiiso  40629  spALT  40742  axc5c4c711toc5  40942  axc5c4c711toc4  40943  axc5c4c711toc7  40944  axc5c4c711to11  40945  pm2.43bgbi  41059  pm2.43cbi  41060  hbimpg  41096  hbimpgVD  41446  ax6e2ndeqVD  41451  ax6e2ndeqALT  41473  ralimralim  41553  confun  43374  confun5  43378  adh-jarrsc  43435  adh-minim  43436  adh-minimp  43448  iccpartnel  43797  fmtno4prmfac193  43932  prminf2  43947  zeo2ALTV  44031  fpprbasnn  44089  sbgoldbaltlem1  44139  nzerooringczr  44538  islinindfis  44699  lindslinindsimp2lem5  44712  zlmodzxznm  44747
  Copyright terms: Public domain W3C validator