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  1563  tbw-bijust  1620  tbw-negdf  1621  tbw-ax2  1623  merco1  1635  nftht  1715  ala1  1738  exa1  1762  ax13b  1961  ax12OLD  2340  sbi2  2392  ax12vALT  2427  moa1  2520  euim  2522  r19.12  3056  r19.27v  3063  r19.37  3078  eqvinc  3313  rr19.3v  3328  invdisjrab  4602  class2seteq  4793  dvdemo2  4864  iunopeqop  4941  asymref2  5472  elfv2ex  6186  elovmpt3imp  6843  sorpssuni  6899  sorpssint  6900  dfwe2  6928  ordunisuc2  6991  tfindsg  7007  findsg  7040  smo11  7406  omex  8484  r111  8582  kmlem12  8927  ltlen  10082  squeeze0  10870  elnnnn0b  11281  nn0ge2m1nn  11304  nn0lt10b  11383  znnn0nn  11433  iccneg  12235  hashfzp1  13158  hash2prde  13190  hash2pwpr  13196  hashge2el2dif  13200  scshwfzeqfzo  13509  relexprel  13713  algcvgblem  15214  prm23ge5  15444  prmgaplem5  15683  prmgaplem6  15684  cshwshashlem1  15726  dfgrp2e  17369  gsmtrcl  17857  prmirred  19762  symgmatr01lem  20378  pmatcollpw3fi1  20512  cxpcn2  24387  rpdmgm  24651  bpos1  24908  2lgs  25032  umgrislfupgrlem  25912  uhgr2edg  25993  nbusgrvtxm1  26168  uvtxa01vtx0  26184  g0wlk0  26417  wlkonl1iedg  26430  wlkreslem  26435  crctcshwlkn0lem5  26575  0enwwlksnge1  26618  frgr3vlem2  27002  frgrnbnb  27021  frgrncvvdeqlem2  27028  frgrregord013  27107  frgrogt3nreg  27109  2bornot2b  27174  stcltr2i  28980  mdsl1i  29026  eqvincg  29160  prsiga  29972  bnj1533  30627  bnj1176  30778  idinside  31830  tb-ax2  32018  bj-a1k  32174  bj-imim2ALT  32177  pm4.81ALT  32185  bj-andnotim  32212  bj-ssbeq  32266  bj-ssb0  32267  bj-ssb1a  32271  bj-eqs  32302  bj-stdpc4v  32394  bj-dvdemo2  32443  wl-jarri  32917  tsim3  33568  mpt2bi123f  33600  mptbi12f  33604  ac6s6  33609  ax12fromc15  33667  axc5c7toc5  33674  axc5c711toc5  33681  ax12f  33702  ax12eq  33703  ax12el  33704  ax12indi  33706  ax12indalem  33707  ax12inda2ALT  33708  ax12inda2  33709  atpsubN  34516  ifpim23g  37318  rp-fakeimass  37335  inintabss  37362  ntrneiiso  37868  axc5c4c711toc5  38082  axc5c4c711toc4  38083  axc5c4c711toc7  38084  axc5c4c711to11  38085  pm2.43bgbi  38202  pm2.43cbi  38203  hbimpg  38249  hbimpgVD  38620  ax6e2ndeqVD  38625  ax6e2ndeqALT  38647  ralimralim  38735  confun  40407  confun5  40411  iccpartnel  40669  fmtno4prmfac193  40781  prminf2  40796  zeo2ALTV  40878  sgoldbaltlem1  40959  nzerooringczr  41357  islinindfis  41523  lindslinindsimp2lem5  41536  zlmodzxznm  41571
  Copyright terms: Public domain W3C validator