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, 29-Dec-1992.) (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 setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpisyl  18  mp2OLD  19  syl6mpi  62  mp2ani  678  mp3an3  1303  merco2  1543  equcomi  1731  equviniv  1741  19.8a  1793  spimt  1949  equs4  1983  ax12v2  2033  2ax6elem  2157  ax12eq  2241  ax12el  2242  ax12inda  2248  ax12v2-o  2249  pm13.183  3095  sbcth  3196  sbcth2  3276  ssun3  3516  ssun4  3517  uneqdifeq  3762  ralf0  3781  uniintsn  4160  rext  4535  exss  4550  uniopel  4590  wefrc  4709  ordun  4815  relop  4985  dmrnssfld  5093  iss  5149  sofld  5281  relcoi1  5361  nfunv  5444  funimass2  5487  fvbr0  5706  fvmptg  5767  fovcl  6190  ov3  6222  elovmpt2  6302  limsssuc  6456  tfisi  6464  finds1  6500  frxp  6677  tfrlem1  6827  oaordi  6977  oaword2  6984  omeulem1  7013  oeworde  7024  oelim2  7026  nnaordi  7049  oaabs2  7076  0domg  7430  limenpsi  7478  enp1i  7539  findcard2  7544  ordunifi  7554  fidomdm  7585  dffi3  7673  oismo  7746  wdom2d  7787  wdomima2g  7793  suc11reg  7817  elom3  7846  cantnfval2  7869  cantnfval2OLD  7899  rankunb  8049  rankval4  8066  karden  8094  cardsn  8131  cardlim  8134  cardprclem  8141  fseqdom  8188  dfac12lem3  8306  kmlem2  8312  kmlem10  8320  cflim2  8424  cfslb2n  8429  fin23lem27  8489  axcc3  8599  axcc4  8600  acncc  8601  domtriomlem  8603  axdclem2  8681  imadomg  8693  alephval2  8728  alephreg  8738  axextnd  8747  fpwwe2lem10  8798  pwfseq  8823  gch2  8834  axgroth3  8990  inaprc  8995  nlt1pi  9067  indpi  9068  1re  9377  mul02lem2  9538  addid1  9541  fimaxre  10269  supmul1  10287  inelr  10304  rimul  10305  nnge1  10340  zneo  10716  uzindOLD  10728  ltweuz  11776  hash2pwpr  12174  hashf1lem2  12201  climuni  13022  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  efne0  13373  ruclem13  13516  dvdslelem  13569  divalglem0  13589  prmreclem2  13970  prmreclem3  13971  mreexexd  14578  coaval  14928  xpcco  14985  pltirr  15125  frgpnabllem1  16342  ablfac1eulem  16561  mdetunilem9  18401  mretopd  18671  fiuncmp  18982  ptcmpfi  19361  filtop  19403  supnfcls  19568  flimfnfcls  19576  alexsubALTlem2  19595  alexsubALTlem4  19597  trust  19779  rectbntr0  20384  fsumcn  20421  ovoliunlem3  20962  ovolicc2lem4  20978  dyadmax  21053  vitali  21068  itgfsum  21279  dvmptfsum  21422  fta1g  21614  fta1  21749  aannenlem1  21769  aalioulem3  21775  logltb  22023  logdmn0  22060  ang180lem2  22181  angpined  22200  mumullem2  22493  dchrisum0re  22737  chpdifbnd  22779  pntrlog2bnd  22808  pntibndlem3  22816  pnt3  22836  nbgraop  23286  isuvtx  23347  dvrunz  23871  hiidge0  24451  chsupval  24689  chsupcl  24694  chsupss  24696  ococin  24762  chsupval2  24764  ssjo  24801  h1de2i  24907  pjss2i  25034  pjssmii  25035  sto2i  25592  stge1i  25593  stle0i  25594  stlei  25595  stlesi  25596  stm1i  25598  staddi  25601  stadd3i  25603  golem1  25626  stcltrlem1  25631  mdexchi  25690  chirred  25750  atabsi  25756  rmoeq  25822  abrexdomjm  25839  ifbieq12d2  25854  iocinif  26022  voliune  26597  volfiniune  26598  sibfof  26678  probdif  26755  kur14lem9  27054  relexp1  27284  fprod2d  27443  wfrlem5  27679  wfrlem16  27690  frrlem5  27723  nofv  27749  noprc  27773  sscoid  27895  limsucncmpi  28243  wl-embantALT  28303  supaddc  28370  abrexdom  28577  heiborlem10  28672  pellexlem3  29125  pell1234qrne0  29147  hbtlem6  29438  funressnfv  29987  faovcl  30059  hashrabsn1  30186  0eusgraiff0rgra  30505  frgrancvvdeqlem4  30579  scmatid  30805  pmatcollpw2lem  30820  zlmodzxznm  30928  3impexpbicom  31043  sb5ALT  31117  eexinst01  31118  ax6e2eq  31153  sineq0ALT  31560  bnj849  31805  bj-alequex  32061  bj-spimtv  32071  bj-equs4v  32102  bj-axc15v  32122  bj-exlimmpi  32261  cvrnrefN  32767  pmod1i  33332  pmodN  33334  osumcllem11N  33450  pexmidlem8N  33461  pl42lem3N  33465  cdleme18b  33776  dochexmidlem8  34952
  Copyright terms: Public domain W3C validator