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  350  pm5.4  377  pm4.8  380  olc  399  simpl  473  pm4.45im  584  jao1i  824  pm2.74  890  oibabs  924  pm5.14  929  biort  937  dedlem0a  999  meredith  1564  tbw-bijust  1621  tbw-negdf  1622  tbw-ax2  1624  merco1  1636  nftht  1716  ala1  1739  exa1  1763  ax13b  1962  ax12OLD  2339  sbi2  2391  ax12vALT  2426  moa1  2519  euim  2521  r19.12  3059  r19.27v  3066  r19.37  3081  eqvinc  3324  rr19.3v  3339  invdisjrab  4630  class2seteq  4824  dvdemo2  4894  iunopeqop  4971  asymref2  5501  elfv2ex  6216  elovmpt3imp  6875  sorpssuni  6931  sorpssint  6932  dfwe2  6966  ordunisuc2  7029  tfindsg  7045  findsg  7078  smo11  7446  omex  8525  r111  8623  kmlem12  8968  ltlen  10123  squeeze0  10911  elnnnn0b  11322  nn0ge2m1nn  11345  nn0lt10b  11424  znnn0nn  11474  iccneg  12278  hashfzp1  13201  hash2prde  13235  hash2pwpr  13241  hashge2el2dif  13245  scshwfzeqfzo  13553  relexprel  13760  algcvgblem  15271  prm23ge5  15501  prmgaplem5  15740  prmgaplem6  15741  cshwshashlem1  15783  dfgrp2e  17429  gsmtrcl  17917  prmirred  19824  symgmatr01lem  20440  pmatcollpw3fi1  20574  cxpcn2  24468  rpdmgm  24732  bpos1  24989  2lgs  25113  umgrislfupgrlem  25998  uhgr2edg  26081  nbusgrvtxm1  26262  uvtxa01vtx0  26278  g0wlk0  26529  wlkonl1iedg  26542  wlkreslem  26547  crctcshwlkn0lem5  26687  0enwwlksnge1  26730  frgr3vlem2  27118  frgrnbnb  27137  frgrregord013  27223  frgrogt3nreg  27225  2bornot2b  27290  stcltr2i  29104  mdsl1i  29150  eqvincg  29284  prsiga  30168  logdivsqrle  30702  bnj1533  30896  bnj1176  31047  jath  31584  idinside  32166  tb-ax2  32354  bj-a1k  32510  bj-imim2ALT  32513  pm4.81ALT  32521  bj-andnotim  32548  bj-ssbeq  32602  bj-ssb0  32603  bj-ssb1a  32607  bj-eqs  32638  bj-stdpc4v  32729  bj-dvdemo2  32778  wl-jarri  33259  tsim3  33910  mpt2bi123f  33942  mptbi12f  33946  ac6s6  33951  ax12fromc15  34009  axc5c7toc5  34016  axc5c711toc5  34023  ax12f  34044  ax12eq  34045  ax12el  34046  ax12indi  34048  ax12indalem  34049  ax12inda2ALT  34050  ax12inda2  34051  atpsubN  34858  ifpim23g  37659  rp-fakeimass  37676  inintabss  37703  ntrneiiso  38209  axc5c4c711toc5  38423  axc5c4c711toc4  38424  axc5c4c711toc7  38425  axc5c4c711to11  38426  pm2.43bgbi  38543  pm2.43cbi  38544  hbimpg  38590  hbimpgVD  38960  ax6e2ndeqVD  38965  ax6e2ndeqALT  38987  ralimralim  39073  confun  40869  confun5  40873  iccpartnel  41138  fmtno4prmfac193  41250  prminf2  41265  zeo2ALTV  41347  sbgoldbaltlem1  41432  nzerooringczr  41837  islinindfis  42003  lindslinindsimp2lem5  42016  zlmodzxznm  42051
  Copyright terms: Public domain W3C validator