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  48  a1ddd  78  jarr  104  pm2.86d  105  pm2.86i  107  pm2.51  164  dfbi1ALT  203  pm5.1im  252  biimt  349  pm5.4  376  pm4.8  379  olc  398  simpl  472  pm4.45im  583  jao1i  821  pm2.74  887  oibabs  921  pm5.14  926  biort  936  dedlem0a  991  meredith  1557  tbw-bijust  1614  tbw-negdf  1615  tbw-ax2  1617  merco1  1629  nftht0  1709  ala1  1755  exa1  1756  ax13b  1951  ax12OLD  2329  sbi2  2381  ax12vALT  2416  moa1  2509  euim  2511  r19.12  3045  r19.27v  3052  r19.37  3067  eqvinc  3300  rr19.3v  3314  invdisjrab  4572  class2seteq  4759  dvdemo2  4830  iunopeqop  4906  asymref2  5432  iotanul  5783  elfv2ex  6139  elovmpt3imp  6788  sorpssuni  6844  sorpssint  6845  dfwe2  6873  ordunisuc2  6936  tfindsg  6952  findsg  6985  smo11  7348  omex  8423  r111  8521  kmlem12  8866  ltlen  10017  squeeze0  10805  elnnnn0b  11214  nn0ge2m1nn  11237  nn0lt10b  11316  znnn0nn  11365  iccneg  12164  hashfzp1  13078  hash2prde  13109  hash2pwpr  13115  hashge2el2dif  13117  scshwfzeqfzo  13423  relexprel  13627  nn0enne  14932  algcvgblem  15128  prm23ge5  15358  prmgaplem5  15597  prmgaplem6  15598  cshwshashlem1  15640  dfgrp2e  17271  gsmtrcl  17759  prmirred  19662  symgmatr01lem  20278  pmatcollpw3fi1  20412  cxpcn2  24287  rpdmgm  24551  bpos1  24808  2lgs  24932  umgrislfupgrlem  25788  usgra2edg  25911  nbgra0nb  25958  wlkdvspthlem  26137  usgrcyclnl2  26169  4cycl4dv  26195  nbhashuvtx1  26442  rusgrasn  26472  frgra3vlem2  26528  frgranbnb  26547  frgrancvvdeqlem2  26558  frgraregord013  26645  frgraogt3nreg  26647  2bornot2b  26712  stcltr2i  28518  mdsl1i  28564  eqvincg  28698  prsiga  29521  bnj1533  30176  bnj1176  30327  idinside  31361  tb-ax2  31549  bj-a1k  31705  bj-imim2ALT  31708  pm4.81ALT  31716  bj-andnotim  31746  bj-nftht  31769  bj-ssbeq  31816  bj-ssb0  31817  bj-ssb1a  31821  bj-eqs  31850  bj-stdpc4v  31942  bj-dvdemo2  31991  wl-jarri  32467  tsim3  33109  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  ax12fromc15  33208  axc5c7toc5  33215  axc5c711toc5  33222  ax12f  33243  ax12eq  33244  ax12el  33245  ax12indi  33247  ax12indalem  33248  ax12inda2ALT  33249  ax12inda2  33250  atpsubN  34057  ifpim23g  36859  rp-fakeimass  36876  inintabss  36903  ntrneiiso  37409  axc5c4c711toc5  37625  axc5c4c711toc4  37626  axc5c4c711toc7  37627  axc5c4c711to11  37628  pm2.43bgbi  37744  pm2.43cbi  37745  hbimpg  37791  hbimpgVD  38162  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  ralimralim  38279  confun  39755  confun5  39759  iccpartnel  39976  fmtno4prmfac193  40023  prminf2  40038  zeo2ALTV  40120  sgoldbaltlem1  40201  uhgr2edg  40435  nbusgrvtxm1  40607  uvtxa01vtx0  40623  g01wlk0  40860  wlkOnl1iedg  40873  1wlkreslem  40878  crctcsh1wlkn0lem5  41017  0enwwlksnge1  41060  frgr3vlem2  41444  frgrnbnb  41463  frgrncvvdeqlem2  41470  av-frgraregord013  41549  av-frgraogt3nreg  41551  nzerooringczr  41864  islinindfis  42032  lindslinindsimp2lem5  42045  zlmodzxznm  42080
  Copyright terms: Public domain W3C validator