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  1304  merco2  1544  equcomi  1733  equviniv  1743  19.8a  1797  19.8aOLD  1798  aev  1881  spimt  1961  equs4  1995  ax12v2  2043  2ax6elem  2166  ax12eq  2251  ax12el  2252  ax12inda  2258  ax12v2-o  2259  pm13.183  3205  sbcth  3307  sbcth2  3387  ssun3  3628  ssun4  3629  uneqdifeq  3874  ralf0  3893  uniintsn  4272  rext  4647  exss  4662  uniopel  4702  wefrc  4821  ordun  4927  relop  5097  dmrnssfld  5205  iss  5261  sofld  5393  relcoi1  5473  nfunv  5556  funimass2  5599  fvbr0  5819  fvmptg  5880  fovcl  6304  ov3  6336  elovmpt2  6416  limsssuc  6570  tfisi  6578  finds1  6614  frxp  6791  tfrlem1  6944  oaordi  7094  oaword2  7101  omeulem1  7130  oeworde  7141  oelim2  7143  nnaordi  7166  oaabs2  7193  0domg  7547  limenpsi  7595  enp1i  7657  findcard2  7662  ordunifi  7672  fidomdm  7703  dffi3  7791  oismo  7864  wdom2d  7905  wdomima2g  7911  suc11reg  7935  elom3  7964  cantnfval2  7987  cantnfval2OLD  8017  rankunb  8167  rankval4  8184  karden  8212  cardsn  8249  cardlim  8252  cardprclem  8259  fseqdom  8306  dfac12lem3  8424  kmlem2  8430  kmlem10  8438  cflim2  8542  cfslb2n  8547  fin23lem27  8607  axcc3  8717  axcc4  8718  acncc  8719  domtriomlem  8721  axdclem2  8799  imadomg  8811  alephval2  8846  alephreg  8856  axextnd  8865  fpwwe2lem10  8916  pwfseq  8941  gch2  8952  axgroth3  9108  inaprc  9113  nlt1pi  9185  indpi  9186  1re  9495  mul02lem2  9656  addid1  9659  fimaxre  10387  supmul1  10405  inelr  10422  rimul  10423  nnge1  10458  zneo  10834  uzindOLD  10846  ltweuz  11900  hash2pwpr  12299  hashf1lem2  12326  climuni  13147  fsum2d  13355  fsumabs  13381  fsumrlim  13391  fsumo1  13392  fsumiun  13401  efne0  13498  ruclem13  13641  dvdslelem  13694  divalglem0  13714  prmreclem2  14095  prmreclem3  14096  mreexexd  14704  coaval  15054  xpcco  15111  pltirr  15251  frgpnabllem1  16471  ablfac1eulem  16694  mdetunilem9  18557  mretopd  18827  fiuncmp  19138  ptcmpfi  19517  filtop  19559  supnfcls  19724  flimfnfcls  19732  alexsubALTlem2  19751  alexsubALTlem4  19753  trust  19935  rectbntr0  20540  fsumcn  20577  ovoliunlem3  21118  ovolicc2lem4  21134  dyadmax  21210  vitali  21225  itgfsum  21436  dvmptfsum  21579  fta1g  21771  fta1  21906  aannenlem1  21926  aalioulem3  21932  logltb  22180  logdmn0  22217  ang180lem2  22338  angpined  22357  mumullem2  22650  dchrisum0re  22894  chpdifbnd  22936  pntrlog2bnd  22965  pntibndlem3  22973  pnt3  22993  nbgraop  23486  isuvtx  23547  dvrunz  24071  hiidge0  24651  chsupval  24889  chsupcl  24894  chsupss  24896  ococin  24962  chsupval2  24964  ssjo  25001  h1de2i  25107  pjss2i  25234  pjssmii  25235  sto2i  25792  stge1i  25793  stle0i  25794  stlei  25795  stlesi  25796  stm1i  25798  staddi  25801  stadd3i  25803  golem1  25826  stcltrlem1  25831  mdexchi  25890  chirred  25950  atabsi  25956  rmoeq  26022  abrexdomjm  26039  ifbieq12d2  26054  iocinif  26215  voliune  26788  volfiniune  26789  sibfof  26869  probdif  26946  kur14lem9  27245  relexp1  27476  fprod2d  27635  wfrlem5  27871  wfrlem16  27882  frrlem5  27915  nofv  27941  noprc  27965  sscoid  28087  limsucncmpi  28434  wl-embantALT  28499  supaddc  28564  abrexdom  28771  heiborlem10  28866  pellexlem3  29319  pell1234qrne0  29341  hbtlem6  29632  funressnfv  30181  faovcl  30253  hashrabsn1  30380  0eusgraiff0rgra  30699  frgrancvvdeqlem4  30773  scmatid  31047  zlmodzxznm  31157  3impexpbicom  31473  sb5ALT  31547  eexinst01  31548  ax6e2eq  31583  sineq0ALT  31990  bnj849  32235  bj-alequex  32521  bj-spimtv  32531  bj-equs4v  32562  bj-axc15v  32582  bj-exlimmpi  32729  cvrnrefN  33250  pmod1i  33815  pmodN  33817  osumcllem11N  33933  pexmidlem8N  33944  pl42lem3N  33948  cdleme18b  34259  dochexmidlem8  35435
  Copyright terms: Public domain W3C validator