MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Unicode version

Theorem mpi 16
Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypotheses
Ref Expression
mpi.1  |-  ps
mpi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpi  |-  ( ph  ->  ch )

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3  |-  ps
21a1i 10 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2  17  syl6mpi  58  mp2ani  659  mp3an3  1267  3impexpbicom  1372  ee10  1381  merco2  1506  equcomi  1684  19.8a  1752  ax10  1957  equveli  2001  ax11v2  2005  ax11eq  2206  ax11el  2207  ax11inda  2213  ax11v2-o  2214  pm13.183  2993  sbcth  3091  sbcth2  3160  ssun3  3428  ssun4  3429  uneqdifeq  3631  ralf0  3649  uniintsn  4001  rext  4325  exss  4339  uniopel  4373  wefrc  4490  ordun  4597  limsssuc  4744  tfisi  4752  finds1  4788  relop  4937  dmrnssfld  5041  iss  5101  sofld  5224  relcoi1  5304  nfunv  5388  funimass2  5431  fvbr0  5656  fvmptg  5707  fovcl  6075  ov3  6110  elovmpt2  6191  frxp  6353  oaordi  6686  oaword2  6693  omeulem1  6722  oeworde  6733  oelim2  6735  nnaordi  6758  oaabs2  6785  sbthlem1  7114  0domg  7131  limenpsi  7179  enp1i  7240  findcard2  7245  ordunifi  7254  fidomdm  7285  dffi3  7331  oismo  7402  wdom2d  7441  wdomima2g  7447  suc11reg  7467  elom3  7496  cantnfval2  7517  rankunb  7669  rankval4  7686  karden  7712  cardsn  7749  cardlim  7752  cardprclem  7759  fseqdom  7800  dfac12lem3  7918  kmlem2  7924  kmlem10  7932  cflim2  8036  cfslb2n  8041  fin23lem27  8101  axcc3  8211  axcc4  8212  acncc  8213  domtriomlem  8215  axdclem2  8294  imadomg  8306  alephval2  8341  alephreg  8351  axextnd  8360  fpwwe2lem10  8408  pwfseq  8433  gch2  8448  axgroth3  8600  inaprc  8605  nlt1pi  8677  indpi  8678  1re  8984  mul02lem2  9136  addid1  9139  fimaxre  9848  supmul1  9866  inelr  9883  rimul  9884  nnge1  9919  zneo  10245  uzindOLD  10257  ltweuz  11188  hashf1lem2  11592  climuni  12233  fsum2d  12442  fsumabs  12467  fsumrlim  12477  fsumo1  12478  fsumiun  12487  efne0  12585  ruclem13  12728  dvdslelem  12781  divalglem0  12800  prmreclem2  13172  prmreclem3  13173  mreexexd  13760  coaval  14110  xpcco  14167  pltirr  14307  frgpnabllem1  15371  ablfac1eulem  15517  mretopd  17046  fiuncmp  17348  ptcmpfi  17721  filtop  17763  supnfcls  17928  flimfnfcls  17936  alexsubALTlem2  17955  alexsubALTlem4  17957  rectbntr0  18551  fsumcn  18588  bcthlem2  18962  ovoliunlem3  19078  ovolicc2lem4  19094  dyadmax  19168  vitali  19183  itgfsum  19396  dvmptfsum  19537  fta1g  19768  fta1  19903  aannenlem1  19923  aalioulem3  19929  logltb  20172  logdmn0  20209  ang180lem2  20330  angpined  20349  mumullem2  20641  dchrisum0re  20885  chpdifbnd  20927  pntrlog2bnd  20956  pntibndlem3  20964  pnt3  20984  nbgraop  21106  isuvtx  21167  dvrunz  21532  hiidge0  22111  chsupval  22348  chsupcl  22353  chsupss  22355  ococin  22421  chsupval2  22423  ssjo  22460  h1de2i  22566  pjss2i  22693  pjssmii  22694  sto2i  23251  stge1i  23252  stle0i  23253  stlei  23254  stlesi  23255  stm1i  23257  staddi  23260  stadd3i  23262  golem1  23285  stcltrlem1  23290  mdexchi  23349  chirred  23409  atabsi  23415  abrexdomjm  23504  ctex  23624  trust  23853  probdif  24247  kur14lem9  24469  relexp1  24699  wfrlem5  25086  wfrlem16  25097  tfrALTlem  25102  frrlem5  25111  nofv  25137  noprc  25161  dffun10  25279  limsucncmpi  25711  wl-adnestantALT  25734  supaddc  25750  abrexdom  25997  heiborlem10  26135  pellexlem3  26507  pell1234qrne0  26529  hbtlem6  26924  funressnfv  27584  faovcl  27656  frgrancvvdeqlem4  27856  sb5ALT  28023  eexinst01  28024  a9e2eq  28058  bnj849  28709  ax10NEW7  28886  equveliNEW7  28939  ax11v2NEW7  28941  a12stdy1-x12  29170  a12stdy1  29185  ax9lem1  29199  ax9vax9  29217  cvrnrefN  29531  pmod1i  30096  pmodN  30098  osumcllem11N  30214  pexmidlem8N  30225  pl42lem3N  30229  cdleme18b  30540  dochexmidlem8  31716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator