MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1 Structured version   Unicode 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  ph and  ps to the assertion of  ph simply." (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-1  |-  ( ph  ->  ( ps  ->  ph )
)

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2  wff  ph
2 wps . . 3  wff  ps
32, 1wi 4 . 2  wff  ( ps 
->  ph )
41, 3wi 4 1  wff  ( ph  ->  ( ps  ->  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  a1i  11  id  21  id1  22  a1d  24  a1dd  45  jarr  94  pm2.86i  95  pm2.86d  96  pm2.51  148  dfbi1gb  187  pm5.1im  231  biimt  327  pm5.4  353  pm4.8  356  olc  375  simpl  445  pm4.45im  547  pm2.64  766  pm2.74  821  pm2.82  827  oibabs  853  pm5.14  858  biort  868  dedlem0a  920  meredith  1414  tbw-bijust  1473  tbw-negdf  1474  tbw-ax2  1476  merco1  1488  ax12b  1702  ax11dgen  1738  19.38  1813  nfimdOLD  1829  hbimdOLD  1836  hbimOLD  1838  a16gOLD  2050  stdpc4  2092  sbi2  2135  ax11v  2174  ax11  2234  ax46to4  2242  ax467to4  2249  ax11f  2271  ax11eq  2272  ax11el  2273  ax11indi  2275  ax11indalem  2276  ax11inda2ALT  2277  ax11inda2  2278  morimv  2331  euim  2333  alral  2766  r19.12  2821  r19.27av  2846  r19.37  2859  eqvinc  3065  rr19.3v  3079  class2seteq  4371  dvdemo2  4403  dfwe2  4765  ordunisuc2  4827  tfindsg  4843  findsg  4875  asymref2  5254  iotanul  5436  sorpssuni  6534  sorpssint  6535  smo11  6629  omex  7601  r111  7704  kmlem12  8046  fin1a2lem10  8294  domtriomlem  8327  ltlen  9180  squeeze0  9918  elnnnn0b  10269  iccneg  11023  hash2prde  11693  algcvgblem  13073  prmirred  16780  cxpcn2  20635  bpos1  21072  usgra2edg  21407  nbgra0nb  21446  nbcusgra  21477  wlkdvspthlem  21612  usgrcyclnl2  21633  4cycl4dv  21659  2bornot2b  21763  stcltr2i  23783  mdsl1i  23829  eqvincg  23966  prsiga  24519  rpdmgm  24814  hbimtg  25439  idinside  26023  tb-ax2  26134  wl-jarri  26217  a1i4  26313  prtlem1  26704  ax4567to4  27593  ax4567to5  27594  ax4567to6  27595  ax4567to7  27596  cshwssizelem1a  28313  cshwssizelem3  28316  cshwssizelem4a  28317  nbhashuvtx1  28431  frgra3vlem2  28465  frgranbnb  28484  frgrancvvdeqlem2  28494  pm2.43bgbi  28674  pm2.43cbi  28675  hbimpg  28715  hbimpgVD  29090  a9e2ndeqVD  29095  a9e2ndeqALT  29117  bnj1533  29297  bnj1176  29448  a16gNEW7  29620  stdpc4NEW7  29629  sbi2NEW7  29638  ax11vNEW7  29669  atpsubN  30624
  Copyright terms: Public domain W3C validator