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 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  671  mp3an3  1296  3impexpbicom  1414  merco2  1546  equcomi  1730  equviniv  1740  19.8a  1792  spimt  1948  equs4  1982  ax12v2  2032  2sb6rflem1  2159  ax12eq  2243  ax12el  2244  ax12inda  2250  ax12v2-o  2251  pm13.183  3089  sbcth  3189  sbcth2  3269  ssun3  3509  ssun4  3510  uneqdifeq  3755  ralf0  3774  uniintsn  4153  rext  4528  exss  4543  uniopel  4583  wefrc  4701  ordun  4807  relop  4977  dmrnssfld  5085  iss  5142  sofld  5274  relcoi1  5354  nfunv  5437  funimass2  5480  fvbr0  5699  fvmptg  5760  fovcl  6184  ov3  6216  elovmpt2  6296  limsssuc  6450  tfisi  6458  finds1  6494  frxp  6671  tfrlem1  6821  oaordi  6973  oaword2  6980  omeulem1  7009  oeworde  7020  oelim2  7022  nnaordi  7045  oaabs2  7072  0domg  7426  limenpsi  7474  enp1i  7535  findcard2  7540  ordunifi  7550  fidomdm  7581  dffi3  7669  oismo  7742  wdom2d  7783  wdomima2g  7789  suc11reg  7813  elom3  7842  cantnfval2  7865  cantnfval2OLD  7895  rankunb  8045  rankval4  8062  karden  8090  cardsn  8127  cardlim  8130  cardprclem  8137  fseqdom  8184  dfac12lem3  8302  kmlem2  8308  kmlem10  8316  cflim2  8420  cfslb2n  8425  fin23lem27  8485  axcc3  8595  axcc4  8596  acncc  8597  domtriomlem  8599  axdclem2  8677  imadomg  8689  alephval2  8724  alephreg  8734  axextnd  8743  fpwwe2lem10  8794  pwfseq  8819  gch2  8830  axgroth3  8986  inaprc  8991  nlt1pi  9063  indpi  9064  1re  9373  mul02lem2  9534  addid1  9537  fimaxre  10265  supmul1  10283  inelr  10300  rimul  10301  nnge1  10336  zneo  10712  uzindOLD  10724  ltweuz  11768  hash2pwpr  12166  hashf1lem2  12193  climuni  13014  fsum2d  13222  fsumabs  13247  fsumrlim  13257  fsumo1  13258  fsumiun  13267  efne0  13364  ruclem13  13507  dvdslelem  13560  divalglem0  13580  prmreclem2  13961  prmreclem3  13962  mreexexd  14569  coaval  14919  xpcco  14976  pltirr  15116  frgpnabllem1  16331  ablfac1eulem  16547  mdetunilem9  18268  mretopd  18538  fiuncmp  18849  ptcmpfi  19228  filtop  19270  supnfcls  19435  flimfnfcls  19443  alexsubALTlem2  19462  alexsubALTlem4  19464  trust  19646  rectbntr0  20251  fsumcn  20288  ovoliunlem3  20829  ovolicc2lem4  20845  dyadmax  20920  vitali  20935  itgfsum  21146  dvmptfsum  21289  fta1g  21524  fta1  21659  aannenlem1  21679  aalioulem3  21685  logltb  21933  logdmn0  21970  ang180lem2  22091  angpined  22110  mumullem2  22403  dchrisum0re  22647  chpdifbnd  22689  pntrlog2bnd  22718  pntibndlem3  22726  pnt3  22746  nbgraop  23158  isuvtx  23219  dvrunz  23743  hiidge0  24323  chsupval  24561  chsupcl  24566  chsupss  24568  ococin  24634  chsupval2  24636  ssjo  24673  h1de2i  24779  pjss2i  24906  pjssmii  24907  sto2i  25464  stge1i  25465  stle0i  25466  stlei  25467  stlesi  25468  stm1i  25470  staddi  25473  stadd3i  25475  golem1  25498  stcltrlem1  25503  mdexchi  25562  chirred  25622  atabsi  25628  rmoeq  25695  abrexdomjm  25712  ifbieq12d2  25727  iocinif  25894  voliune  26499  volfiniune  26500  sibfof  26574  probdif  26651  kur14lem9  26950  relexp1  27180  fprod2d  27339  wfrlem5  27575  wfrlem16  27586  frrlem5  27619  nofv  27645  noprc  27669  sscoid  27791  limsucncmpi  28139  wl-embantALT  28199  supaddc  28261  abrexdom  28468  heiborlem10  28563  pellexlem3  29017  pell1234qrne0  29039  hbtlem6  29330  funressnfv  29880  faovcl  29952  hashrabsn1  30079  0eusgraiff0rgra  30398  frgrancvvdeqlem4  30472  zlmodzxznm  30748  sb5ALT  30931  eexinst01  30932  ax6e2eq  30967  sineq0ALT  31375  bnj849  31620  bj-alequex  31835  bj-spimtv  31845  bj-equs4v  31876  bj-axc15v  31896  bj-vtoclgf  32006  cvrnrefN  32500  pmod1i  33065  pmodN  33067  osumcllem11N  33183  pexmidlem8N  33194  pl42lem3N  33198  cdleme18b  33509  dochexmidlem8  34685
  Copyright terms: Public domain W3C validator