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  1686  19.8a  1754  equs4  1944  ax10OLD  1988  equveli  2023  ax11v2  2026  ax11eq  2227  ax11el  2228  ax11inda  2234  ax11v2-o  2235  pm13.183  3019  sbcth  3118  sbcth2  3187  ssun3  3455  ssun4  3456  uneqdifeq  3659  ralf0  3677  uniintsn  4029  rext  4353  exss  4367  uniopel  4401  wefrc  4517  ordun  4623  limsssuc  4770  tfisi  4778  finds1  4814  relop  4963  dmrnssfld  5069  iss  5129  sofld  5258  relcoi1  5338  nfunv  5424  funimass2  5467  fvbr0  5692  fvmptg  5743  fovcl  6114  ov3  6149  elovmpt2  6230  frxp  6392  oaordi  6725  oaword2  6732  omeulem1  6761  oeworde  6772  oelim2  6774  nnaordi  6797  oaabs2  6824  0domg  7170  limenpsi  7218  enp1i  7279  findcard2  7284  ordunifi  7293  fidomdm  7324  dffi3  7371  oismo  7442  wdom2d  7481  wdomima2g  7487  suc11reg  7507  elom3  7536  cantnfval2  7557  rankunb  7709  rankval4  7726  karden  7752  cardsn  7789  cardlim  7792  cardprclem  7799  fseqdom  7840  dfac12lem3  7958  kmlem2  7964  kmlem10  7972  cflim2  8076  cfslb2n  8081  fin23lem27  8141  axcc3  8251  axcc4  8252  acncc  8253  domtriomlem  8255  axdclem2  8333  imadomg  8345  alephval2  8380  alephreg  8390  axextnd  8399  fpwwe2lem10  8447  pwfseq  8472  gch2  8487  axgroth3  8639  inaprc  8644  nlt1pi  8716  indpi  8717  1re  9023  mul02lem2  9175  addid1  9178  fimaxre  9887  supmul1  9905  inelr  9922  rimul  9923  nnge1  9958  zneo  10284  uzindOLD  10296  ltweuz  11228  hashf1lem2  11632  climuni  12273  fsum2d  12482  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  efne0  12625  ruclem13  12768  dvdslelem  12821  divalglem0  12840  prmreclem2  13212  prmreclem3  13213  mreexexd  13800  coaval  14150  xpcco  14207  pltirr  14347  frgpnabllem1  15411  ablfac1eulem  15557  mretopd  17079  fiuncmp  17389  ptcmpfi  17766  filtop  17808  supnfcls  17973  flimfnfcls  17981  alexsubALTlem2  18000  alexsubALTlem4  18002  trust  18180  rectbntr0  18734  fsumcn  18771  ovoliunlem3  19267  ovolicc2lem4  19283  dyadmax  19357  vitali  19372  itgfsum  19585  dvmptfsum  19726  fta1g  19957  fta1  20092  aannenlem1  20112  aalioulem3  20118  logltb  20361  logdmn0  20398  ang180lem2  20519  angpined  20538  mumullem2  20830  dchrisum0re  21074  chpdifbnd  21116  pntrlog2bnd  21145  pntibndlem3  21153  pnt3  21173  nbgraop  21302  isuvtx  21363  dvrunz  21869  hiidge0  22448  chsupval  22685  chsupcl  22690  chsupss  22692  ococin  22758  chsupval2  22760  ssjo  22797  h1de2i  22903  pjss2i  23030  pjssmii  23031  sto2i  23588  stge1i  23589  stle0i  23590  stlei  23591  stlesi  23592  stm1i  23594  staddi  23597  stadd3i  23599  golem1  23622  stcltrlem1  23627  mdexchi  23686  chirred  23746  atabsi  23752  abrexdomjm  23832  ifbieq12d2  23846  iocinif  23980  voliune  24379  volfiniune  24380  probdif  24457  kur14lem9  24679  relexp1  24910  wfrlem5  25284  wfrlem16  25295  tfrALTlem  25300  frrlem5  25309  nofv  25335  noprc  25359  dffun10  25477  limsucncmpi  25909  wl-adnestantALT  25932  supaddc  25947  abrexdom  26123  heiborlem10  26220  pellexlem3  26585  pell1234qrne0  26607  hbtlem6  27002  funressnfv  27661  faovcl  27733  frgrancvvdeqlem4  27785  sb5ALT  27952  eexinst01  27953  a9e2eq  27987  bnj849  28634  ax10NEW7  28811  equveliNEW7  28864  ax11v2NEW7  28866  cvrnrefN  29397  pmod1i  29962  pmodN  29964  osumcllem11N  30080  pexmidlem8N  30091  pl42lem3N  30095  cdleme18b  30406  dochexmidlem8  31582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator