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  102  pm2.86d  103  pm2.86i  105  pm2.51  160  dfbi1ALT  199  pm5.1im  248  biimt  344  pm5.4  371  pm4.8  374  olc  393  simpl  466  pm4.45im  577  pm2.64  816  pm2.74  877  pm2.82  883  oibabs  911  pm5.14  916  biort  926  dedlem0a  981  meredith  1554  tbw-bijust  1611  tbw-negdf  1612  tbw-ax2  1614  merco1  1626  ala1  1741  exa1  1742  ax13b  1913  ax12  2224  sbi2  2276  ax12vALT  2311  moa1  2404  euim  2406  r19.12  2938  r19.27v  2945  r19.37  2960  eqvinc  3189  rr19.3v  3203  invdisjrab  4423  class2seteq  4609  dvdemo2  4677  asymref2  5267  iotanul  5612  elfv2ex  5963  elovmpt3imp  6600  sorpssuni  6656  sorpssint  6657  dfwe2  6685  ordunisuc2  6748  tfindsg  6764  findsg  6797  smo11  7160  omex  8233  r111  8331  kmlem12  8676  ltlen  9820  squeeze0  10598  elnnnn0b  11005  nn0ge2m1nn  11025  nn0lt10b  11089  znnn0nn  11137  iccneg  11849  hash2prde  12754  hash2pwpr  12758  hashge2el2dif  12760  scshwfzeqfzo  13061  relexprel  13262  algcvgblem  14698  prmgaplem5  15187  prmgaplem6  15188  cshwshashlem1  15227  gsmtrcl  17318  prmirred  19224  symgmatr01lem  19836  pmatcollpw3fi1  19970  cxpcn2  23847  rpdmgm  24111  bpos1  24372  usgra2edg  25270  nbgra0nb  25318  wlkdvspthlem  25498  usgrcyclnl2  25530  4cycl4dv  25556  nbhashuvtx1  25803  rusgrasn  25833  frgra3vlem2  25889  frgranbnb  25908  frgrancvvdeqlem2  25919  frgraregord013  26006  frgraogt3nreg  26008  2bornot2b  26062  stcltr2i  28091  mdsl1i  28137  eqvincg  28271  prsiga  29108  bnj1533  29815  bnj1176  29966  idinside  31002  tb-ax2  31189  bj-a1k  31314  bj-imim2ALT  31317  pm4.81ALT  31326  bj-andnotim  31356  bj-nftht  31379  bj-ssbeq  31422  bj-ssb0  31423  bj-ssb1a  31427  bj-eqs  31456  bj-stdpc4v  31547  bj-ax12v  31561  bj-dvdemo2  31600  wl-jarri  32062  tsim3  32610  mpt2bi123f  32642  mptbi12f  32646  ac6s6  32651  prtlem1  32655  ax12o  32708  axc5c7toc5  32716  axc5c711toc5  32723  ax12f  32744  ax12eq  32745  ax12el  32746  ax12indi  32748  ax12indalem  32749  ax12inda2ALT  32750  ax12inda2  32751  atpsubN  33558  ifpim23g  36379  rp-fakeimass  36396  inintabss  36423  ntrneiiso  36902  axc5c4c711toc5  37110  axc5c4c711toc4  37111  axc5c4c711toc7  37112  axc5c4c711to11  37113  pm2.43bgbi  37230  pm2.43cbi  37231  hbimpg  37277  hbimpgVD  37649  ax6e2ndeqVD  37654  ax6e2ndeqALT  37676  ralimralim  37770  confun  39047  confun5  39051  iccpartnel  39272  zeo2ALTV  39320  sgoldbaltlem1  39400  iunopeqop  39526  umgrislfupgrlem  39747  uhgr2edg  39835  nbusgrvtxm1  40007  uvtxa01vtx0  40023  g01wlk0  40260  wlkOnl1iedg  40273  1wlkreslem  40278  crctcsh1wlkn0lem5  40417  0enwwlksnge1  40460  frgr3vlem2  40844  frgrnbnb  40863  frgrncvvdeqlem2  40870  av-frgraregord013  40949  av-frgraogt3nreg  40951  nzerooringczr  41264  islinindfis  41432  lindslinindsimp2lem5  41445  zlmodzxznm  41480  nn0enne  41515
  Copyright terms: Public domain W3C validator