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

Theorem mpi 17
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 11 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2ALT  18  syl6mpi  60  mp2ani  660  mp3an3  1268  3impexpbicom  1373  ee10  1382  merco2  1507  equcomi  1687  19.8a  1758  equs4  1951  spimt  1953  ax10OLD  1998  ax11v2  2025  ax11v2OLD  2026  equveliOLD  2045  ax11eq  2251  ax11el  2252  ax11inda  2258  ax11v2-o  2259  pm13.183  3044  sbcth  3143  sbcth2  3212  ssun3  3480  ssun4  3481  uneqdifeq  3684  ralf0  3702  uniintsn  4055  rext  4380  exss  4394  uniopel  4428  wefrc  4544  ordun  4650  limsssuc  4797  tfisi  4805  finds1  4841  relop  4990  dmrnssfld  5096  iss  5156  sofld  5285  relcoi1  5365  nfunv  5451  funimass2  5494  fvbr0  5719  fvmptg  5771  fovcl  6142  ov3  6177  elovmpt2  6258  frxp  6423  oaordi  6756  oaword2  6763  omeulem1  6792  oeworde  6803  oelim2  6805  nnaordi  6828  oaabs2  6855  0domg  7201  limenpsi  7249  enp1i  7310  findcard2  7315  ordunifi  7324  fidomdm  7355  dffi3  7402  oismo  7473  wdom2d  7512  wdomima2g  7518  suc11reg  7538  elom3  7567  cantnfval2  7588  rankunb  7740  rankval4  7757  karden  7783  cardsn  7820  cardlim  7823  cardprclem  7830  fseqdom  7871  dfac12lem3  7989  kmlem2  7995  kmlem10  8003  cflim2  8107  cfslb2n  8112  fin23lem27  8172  axcc3  8282  axcc4  8283  acncc  8284  domtriomlem  8286  axdclem2  8364  imadomg  8376  alephval2  8411  alephreg  8421  axextnd  8430  fpwwe2lem10  8478  pwfseq  8503  gch2  8518  axgroth3  8670  inaprc  8675  nlt1pi  8747  indpi  8748  1re  9054  mul02lem2  9207  addid1  9210  fimaxre  9919  supmul1  9937  inelr  9954  rimul  9955  nnge1  9990  zneo  10316  uzindOLD  10328  ltweuz  11264  hashf1lem2  11668  climuni  12309  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  fsumiun  12563  efne0  12661  ruclem13  12804  dvdslelem  12857  divalglem0  12876  prmreclem2  13248  prmreclem3  13249  mreexexd  13836  coaval  14186  xpcco  14243  pltirr  14383  frgpnabllem1  15447  ablfac1eulem  15593  mretopd  17119  fiuncmp  17429  ptcmpfi  17806  filtop  17848  supnfcls  18013  flimfnfcls  18021  alexsubALTlem2  18040  alexsubALTlem4  18042  trust  18220  rectbntr0  18824  fsumcn  18861  ovoliunlem3  19361  ovolicc2lem4  19377  dyadmax  19451  vitali  19466  itgfsum  19679  dvmptfsum  19820  fta1g  20051  fta1  20186  aannenlem1  20206  aalioulem3  20212  logltb  20455  logdmn0  20492  ang180lem2  20613  angpined  20632  mumullem2  20924  dchrisum0re  21168  chpdifbnd  21210  pntrlog2bnd  21239  pntibndlem3  21247  pnt3  21267  nbgraop  21397  isuvtx  21458  dvrunz  21982  hiidge0  22561  chsupval  22798  chsupcl  22803  chsupss  22805  ococin  22871  chsupval2  22873  ssjo  22910  h1de2i  23016  pjss2i  23143  pjssmii  23144  sto2i  23701  stge1i  23702  stle0i  23703  stlei  23704  stlesi  23705  stm1i  23707  staddi  23710  stadd3i  23712  golem1  23735  stcltrlem1  23740  mdexchi  23799  chirred  23859  atabsi  23865  abrexdomjm  23949  ifbieq12d2  23963  iocinif  24105  voliune  24546  volfiniune  24547  sibfof  24615  probdif  24639  kur14lem9  24861  relexp1  25092  fprod2d  25266  wfrlem5  25482  wfrlem16  25493  tfrALTlem  25498  frrlem5  25507  nofv  25533  noprc  25557  dffun10  25675  limsucncmpi  26107  wl-adnestantALT  26130  supaddc  26145  abrexdom  26330  heiborlem10  26427  pellexlem3  26792  pell1234qrne0  26814  hbtlem6  27209  funressnfv  27867  faovcl  27939  frgrancvvdeqlem4  28144  sb5ALT  28328  eexinst01  28329  a9e2eq  28363  bnj849  29014  ax10NEW7  29191  equveliNEW7  29244  ax11v2NEW7  29246  cvrnrefN  29777  pmod1i  30342  pmodN  30344  osumcllem11N  30460  pexmidlem8N  30471  pl42lem3N  30475  cdleme18b  30786  dochexmidlem8  31962
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator