MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Unicode version

Theorem mpi 16
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 10 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2  17  syl6mpi  58  mp2ani  659  mp3an3  1266  3impexpbicom  1357  ee10  1366  merco2  1491  equcomi  1647  ax10  1886  equveli  1931  ax11v2  1935  ax11eq  2133  ax11el  2134  ax11inda  2140  ax11v2-o  2141  pm13.183  2909  sbcth  3006  sbcth2  3075  ssun3  3341  ssun4  3342  uneqdifeq  3543  ralf0  3561  uniintsn  3900  rext  4221  exss  4235  uniopel  4269  wefrc  4386  ordun  4493  limsssuc  4640  tfisi  4648  finds1  4684  relop  4833  dmrnssfld  4937  iss  4997  sofld  5120  relcoi1  5199  nfunv  5251  funimass2  5292  fvbr0  5511  fvmptg  5562  fovcl  5911  ov3  5946  elovmpt2  6026  frxp  6187  oaordi  6540  oaword2  6547  omeulem1  6576  oeworde  6587  oelim2  6589  nnaordi  6612  oaabs2  6639  sbthlem1  6967  0domg  6984  limenpsi  7032  enp1i  7089  findcard2  7094  ordunifi  7103  fidomdm  7134  dffi3  7180  oismo  7251  wdom2d  7290  wdomima2g  7296  suc11reg  7316  elom3  7345  cantnfval2  7366  rankunb  7518  rankval4  7535  karden  7561  cardsn  7598  cardlim  7601  cardprclem  7608  fseqdom  7649  dfac12lem3  7767  kmlem2  7773  kmlem10  7781  cflim2  7885  cfslb2n  7890  fin23lem27  7950  axcc3  8060  axcc4  8061  acncc  8062  domtriomlem  8064  axdclem2  8143  imadomg  8155  alephval2  8190  alephreg  8200  axextnd  8209  fpwwe2lem10  8257  pwfseq  8282  gch2  8297  axgroth3  8449  inaprc  8454  nlt1pi  8526  indpi  8527  1re  8833  mul02lem2  8985  addid1  8988  fimaxre  9697  supmul1  9715  inelr  9732  rimul  9733  nnge1  9768  zneo  10090  uzindOLD  10102  ltweuz  11020  hashf1lem2  11390  climuni  12022  fsum2d  12230  fsumabs  12255  fsumrlim  12265  fsumo1  12266  fsumiun  12275  efne0  12373  ruclem13  12516  dvdslelem  12569  divalglem0  12588  prmreclem2  12960  prmreclem3  12961  mreexexd  13546  coaval  13896  xpcco  13953  pltirr  14093  frgpnabllem1  15157  ablfac1eulem  15303  mretopd  16825  fiuncmp  17127  ptcmpfi  17500  filtop  17546  supnfcls  17711  flimfnfcls  17719  alexsubALTlem2  17738  alexsubALTlem4  17740  rectbntr0  18333  fsumcn  18370  bcthlem2  18743  ovoliunlem3  18859  ovolicc2lem4  18875  dyadmax  18949  vitali  18964  itgfsum  19177  dvmptfsum  19318  fta1g  19549  fta1  19684  aannenlem1  19704  aalioulem3  19710  logltb  19949  logdmn0  19983  ang180lem2  20104  angpined  20123  mumullem2  20414  dchrisum0re  20658  chpdifbnd  20700  pntrlog2bnd  20729  pntibndlem3  20737  pnt3  20757  dvrunz  21094  hiidge0  21673  chsupval  21910  chsupcl  21915  chsupss  21917  ococin  21983  chsupval2  21985  ssjo  22022  h1de2i  22128  pjss2i  22255  pjssmii  22256  sto2i  22813  stge1i  22814  stle0i  22815  stlei  22816  stlesi  22817  stm1i  22819  staddi  22822  stadd3i  22824  golem1  22847  stcltrlem1  22852  mdexchi  22911  chirred  22971  atabsi  22977  kur14lem9  23152  relexp1  23434  wfrlem5  23664  wfrlem16  23675  tfrALTlem  23680  frrlem5  23689  nofv  23714  noprc  23738  elfuns  23864  limsucncmpi  24294  wl-adnestantALT  24317  intopcoaconlem3  24950  lemindclsbu  25406  abrexdom  25816  heiborlem10  25955  pellexlem3  26327  pell1234qrne0  26349  hbtlem6  26744  funressnfv  27382  faovcl  27451  sb5ALT  27571  eexinst01  27572  a9e2eq  27606  bnj849  28236  a12stdy1-x12  28390  a12stdy1  28405  ax9lem1  28419  ax9vax9  28437  cvrnrefN  28751  pmod1i  29316  pmodN  29318  osumcllem11N  29434  pexmidlem8N  29445  pl42lem3N  29449  cdleme18b  29760  dochexmidlem8  30936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator