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  47  a1ddd  77  jarr  103  pm2.86d  104  pm2.86i  106  pm2.51  163  dfbi1ALT  202  pm5.1im  251  biimt  348  pm5.4  375  pm4.8  378  olc  397  simpl  471  pm4.45im  582  jao1i  820  pm2.74  886  oibabs  920  pm5.14  925  biort  935  dedlem0a  990  meredith  1556  tbw-bijust  1613  tbw-negdf  1614  tbw-ax2  1616  merco1  1628  nftht0  1708  ala1  1754  exa1  1755  ax13b  1950  ax12OLD  2328  sbi2  2380  ax12vALT  2415  moa1  2508  euim  2510  r19.12  3044  r19.27v  3051  r19.37  3066  eqvinc  3299  rr19.3v  3313  invdisjrab  4566  class2seteq  4754  dvdemo2  4825  asymref2  5419  iotanul  5769  elfv2ex  6124  elovmpt3imp  6765  sorpssuni  6821  sorpssint  6822  dfwe2  6850  ordunisuc2  6913  tfindsg  6929  findsg  6962  smo11  7325  omex  8400  r111  8498  kmlem12  8843  ltlen  9989  squeeze0  10775  elnnnn0b  11184  nn0ge2m1nn  11207  nn0lt10b  11272  znnn0nn  11321  iccneg  12120  hashfzp1  13030  hash2prde  13061  hash2pwpr  13065  hashge2el2dif  13067  scshwfzeqfzo  13369  relexprel  13573  nn0enne  14878  algcvgblem  15074  prm23ge5  15304  prmgaplem5  15543  prmgaplem6  15544  cshwshashlem1  15586  dfgrp2e  17217  gsmtrcl  17705  prmirred  19607  symgmatr01lem  20220  pmatcollpw3fi1  20354  cxpcn2  24204  rpdmgm  24468  bpos1  24725  2lgs  24849  usgra2edg  25677  nbgra0nb  25724  wlkdvspthlem  25903  usgrcyclnl2  25935  4cycl4dv  25961  nbhashuvtx1  26208  rusgrasn  26238  frgra3vlem2  26294  frgranbnb  26313  frgrancvvdeqlem2  26324  frgraregord013  26411  frgraogt3nreg  26413  2bornot2b  26478  stcltr2i  28324  mdsl1i  28370  eqvincg  28504  prsiga  29327  bnj1533  29982  bnj1176  30133  idinside  31167  tb-ax2  31355  bj-a1k  31511  bj-imim2ALT  31514  pm4.81ALT  31522  bj-andnotim  31552  bj-nftht  31575  bj-ssbeq  31622  bj-ssb0  31623  bj-ssb1a  31627  bj-eqs  31656  bj-stdpc4v  31748  bj-dvdemo2  31797  wl-jarri  32263  tsim3  32905  mpt2bi123f  32937  mptbi12f  32941  ac6s6  32946  ax12fromc15  33004  axc5c7toc5  33011  axc5c711toc5  33018  ax12f  33039  ax12eq  33040  ax12el  33041  ax12indi  33043  ax12indalem  33044  ax12inda2ALT  33045  ax12inda2  33046  atpsubN  33853  ifpim23g  36655  rp-fakeimass  36672  inintabss  36699  ntrneiiso  37205  axc5c4c711toc5  37421  axc5c4c711toc4  37422  axc5c4c711toc7  37423  axc5c4c711to11  37424  pm2.43bgbi  37540  pm2.43cbi  37541  hbimpg  37587  hbimpgVD  37958  ax6e2ndeqVD  37963  ax6e2ndeqALT  37985  ralimralim  38075  confun  39552  confun5  39556  iccpartnel  39774  fmtno4prmfac193  39821  prminf2  39836  zeo2ALTV  39918  sgoldbaltlem1  39999  iunopeqop  40124  umgrislfupgrlem  40342  uhgr2edg  40430  nbusgrvtxm1  40602  uvtxa01vtx0  40618  g01wlk0  40855  wlkOnl1iedg  40868  1wlkreslem  40873  crctcsh1wlkn0lem5  41012  0enwwlksnge1  41055  frgr3vlem2  41439  frgrnbnb  41458  frgrncvvdeqlem2  41465  av-frgraregord013  41544  av-frgraogt3nreg  41546  nzerooringczr  41859  islinindfis  42027  lindslinindsimp2lem5  42040  zlmodzxznm  42075
  Copyright terms: Public domain W3C validator