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  171  dfbi1ALT  215  pm5.1im  264  biimt  362  pm4.8  393  pm4.45im  823  pm5.31r  827  jao1i  852  olc  862  oibabs  945  pm2.74  968  tarski-bernays-ax2  1632  meredith  1633  tbw-bijust  1690  tbw-negdf  1691  tbw-ax2  1693  merco1  1705  nftht  1784  ala1  1805  exa1  1829  ax13b  2030  sbi2  2302  sbi2vOLD  2316  ax12vALT  2487  sbi2ALT  2603  moabs  2621  moa1  2631  euimOLD  2698  r19.27vOLD  3185  r19.12  3324  r19.12OLD  3327  r19.35  3341  r19.37  3343  eqvincg  3640  rr19.3v  3660  invdisjrab  5044  class2seteq  5247  dvdemo2  5267  iunopeqop  5403  po2ne  5483  asymref2  5971  elfv2ex  6705  elovmpt3imp  7391  sorpssuni  7447  dfwe2  7484  ordunisuc2  7547  smo11  7992  omex  9095  r111  9193  kmlem12  9576  squeeze0  11532  nn0ge2m1nn  11953  nn0lt10b  12033  iccneg  12848  hashfzp1  13782  hash2prde  13818  hash2pwpr  13824  hashge2el2dif  13828  relexprel  14388  algcvgblem  15911  prm23ge5  16142  cshwshashlem1  16419  dfgrp2e  18069  gsmtrcl  18575  symgmatr01lem  21192  cxpcn2  25254  logbgcd1irr  25299  rpdmgm  25530  bpos1  25787  2lgs  25911  2sqnn0  25942  umgrislfupgrlem  26835  uhgr2edg  26918  nbusgrvtxm1  27089  uvtx01vtx  27107  g0wlk0  27361  wlkonl1iedg  27375  wlkreslem  27379  crctcshwlkn0lem5  27520  0enwwlksnge1  27570  clwwlknonex2lem2  27815  frgr3vlem2  27981  frgrnbnb  28000  frgrregord013  28102  frgrogt3nreg  28104  2bornot2b  28171  stcltr2i  29980  mdsl1i  30026  prsiga  31290  logdivsqrle  31821  bnj1533  32024  bnj1176  32175  jath  32856  idinside  33443  tb-ax2  33630  bj-a1k  33781  bj-peircestab  33786  bj-currypeirce  33790  bj-andnotim  33820  bj-ssbeq  33884  bj-eqs  33906  bj-nnftht  33968  curryset  34155  currysetlem3  34158  wl-moae  34639  tsim3  35293  mpobi123f  35323  mptbi12f  35327  ac6s6  35333  ax12fromc15  35923  axc5c7toc5  35930  axc5c711toc5  35937  ax12f  35958  ax12eq  35959  ax12el  35960  ax12indi  35962  ax12indalem  35963  ax12inda2ALT  35964  ax12inda2  35965  atpsubN  36771  ifpim23g  39741  rp-fakeimass  39758  inintabss  39818  ntrneiiso  40321  spALT  40435  axc5c4c711toc5  40614  axc5c4c711toc4  40615  axc5c4c711toc7  40616  axc5c4c711to11  40617  pm2.43bgbi  40731  pm2.43cbi  40732  hbimpg  40768  hbimpgVD  41118  ax6e2ndeqVD  41123  ax6e2ndeqALT  41145  ralimralim  41225  confun  43056  confun5  43060  adh-jarrsc  43117  adh-minim  43118  adh-minimp  43130  iccpartnel  43445  fmtno4prmfac193  43582  prminf2  43597  zeo2ALTV  43683  fpprbasnn  43741  sbgoldbaltlem1  43791  nzerooringczr  44241  islinindfis  44402  lindslinindsimp2lem5  44415  zlmodzxznm  44450
  Copyright terms: Public domain W3C validator