MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Structured version   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  1376  ee10  1385  merco2  1510  equcomi  1691  19.8a  1762  spimt  1955  equs4  1997  ax10OLD  2032  ax11v2  2078  ax11v2OLD  2079  equveliOLD  2086  ax11eq  2270  ax11el  2271  ax11inda  2277  ax11v2-o  2278  pm13.183  3076  sbcth  3175  sbcth2  3244  ssun3  3512  ssun4  3513  uneqdifeq  3716  ralf0  3734  uniintsn  4087  rext  4412  exss  4426  uniopel  4460  wefrc  4576  ordun  4683  limsssuc  4830  tfisi  4838  finds1  4874  relop  5023  dmrnssfld  5129  iss  5189  sofld  5318  relcoi1  5398  nfunv  5484  funimass2  5527  fvbr0  5752  fvmptg  5804  fovcl  6175  ov3  6210  elovmpt2  6291  frxp  6456  oaordi  6789  oaword2  6796  omeulem1  6825  oeworde  6836  oelim2  6838  nnaordi  6861  oaabs2  6888  0domg  7234  limenpsi  7282  enp1i  7343  findcard2  7348  ordunifi  7357  fidomdm  7388  dffi3  7436  oismo  7509  wdom2d  7548  wdomima2g  7554  suc11reg  7574  elom3  7603  cantnfval2  7624  rankunb  7776  rankval4  7793  karden  7819  cardsn  7856  cardlim  7859  cardprclem  7866  fseqdom  7907  dfac12lem3  8025  kmlem2  8031  kmlem10  8039  cflim2  8143  cfslb2n  8148  fin23lem27  8208  axcc3  8318  axcc4  8319  acncc  8320  domtriomlem  8322  axdclem2  8400  imadomg  8412  alephval2  8447  alephreg  8457  axextnd  8466  fpwwe2lem10  8514  pwfseq  8539  gch2  8554  axgroth3  8706  inaprc  8711  nlt1pi  8783  indpi  8784  1re  9090  mul02lem2  9243  addid1  9246  fimaxre  9955  supmul1  9973  inelr  9990  rimul  9991  nnge1  10026  zneo  10352  uzindOLD  10364  ltweuz  11301  hashf1lem2  11705  climuni  12346  fsum2d  12555  fsumabs  12580  fsumrlim  12590  fsumo1  12591  fsumiun  12600  efne0  12698  ruclem13  12841  dvdslelem  12894  divalglem0  12913  prmreclem2  13285  prmreclem3  13286  mreexexd  13873  coaval  14223  xpcco  14280  pltirr  14420  frgpnabllem1  15484  ablfac1eulem  15630  mretopd  17156  fiuncmp  17467  ptcmpfi  17845  filtop  17887  supnfcls  18052  flimfnfcls  18060  alexsubALTlem2  18079  alexsubALTlem4  18081  trust  18259  rectbntr0  18863  fsumcn  18900  ovoliunlem3  19400  ovolicc2lem4  19416  dyadmax  19490  vitali  19505  itgfsum  19718  dvmptfsum  19859  fta1g  20090  fta1  20225  aannenlem1  20245  aalioulem3  20251  logltb  20494  logdmn0  20531  ang180lem2  20652  angpined  20671  mumullem2  20963  dchrisum0re  21207  chpdifbnd  21249  pntrlog2bnd  21278  pntibndlem3  21286  pnt3  21306  nbgraop  21436  isuvtx  21497  dvrunz  22021  hiidge0  22600  chsupval  22837  chsupcl  22842  chsupss  22844  ococin  22910  chsupval2  22912  ssjo  22949  h1de2i  23055  pjss2i  23182  pjssmii  23183  sto2i  23740  stge1i  23741  stle0i  23742  stlei  23743  stlesi  23744  stm1i  23746  staddi  23749  stadd3i  23751  golem1  23774  stcltrlem1  23779  mdexchi  23838  chirred  23898  atabsi  23904  abrexdomjm  23988  ifbieq12d2  24002  iocinif  24144  voliune  24585  volfiniune  24586  sibfof  24654  probdif  24678  kur14lem9  24900  relexp1  25131  fprod2d  25305  wfrlem5  25542  wfrlem16  25553  frrlem5  25586  nofv  25612  noprc  25636  sscoid  25758  limsucncmpi  26195  wl-adnestantALT  26218  supaddc  26237  abrexdom  26432  heiborlem10  26529  pellexlem3  26894  pell1234qrne0  26916  hbtlem6  27310  funressnfv  27968  faovcl  28040  frgrancvvdeqlem4  28422  sb5ALT  28609  eexinst01  28610  a9e2eq  28644  sineq0ALT  29049  bnj849  29296  ax10NEW7  29473  equveliNEW7  29528  ax11v2NEW7  29530  cvrnrefN  30080  pmod1i  30645  pmodN  30647  osumcllem11N  30763  pexmidlem8N  30774  pl42lem3N  30778  cdleme18b  31089  dochexmidlem8  32265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator