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  1648  ax10  1886  equveli  1930  ax11v2  1934  ax11eq  2134  ax11el  2135  ax11inda  2141  ax11v2-o  2142  pm13.183  2910  sbcth  3007  sbcth2  3076  ssun3  3342  ssun4  3343  uneqdifeq  3544  ralf0  3562  uniintsn  3901  rext  4224  exss  4238  uniopel  4272  wefrc  4389  ordun  4496  limsssuc  4643  tfisi  4651  finds1  4687  relop  4836  dmrnssfld  4940  iss  5000  sofld  5123  relcoi1  5203  nfunv  5287  funimass2  5328  fvbr0  5551  fvmptg  5602  fovcl  5951  ov3  5986  elovmpt2  6066  frxp  6227  oaordi  6546  oaword2  6553  omeulem1  6582  oeworde  6593  oelim2  6595  nnaordi  6618  oaabs2  6645  sbthlem1  6973  0domg  6990  limenpsi  7038  enp1i  7095  findcard2  7100  ordunifi  7109  fidomdm  7140  dffi3  7186  oismo  7257  wdom2d  7296  wdomima2g  7302  suc11reg  7322  elom3  7351  cantnfval2  7372  rankunb  7524  rankval4  7541  karden  7567  cardsn  7604  cardlim  7607  cardprclem  7614  fseqdom  7655  dfac12lem3  7773  kmlem2  7779  kmlem10  7787  cflim2  7891  cfslb2n  7896  fin23lem27  7956  axcc3  8066  axcc4  8067  acncc  8068  domtriomlem  8070  axdclem2  8149  imadomg  8161  alephval2  8196  alephreg  8206  axextnd  8215  fpwwe2lem10  8263  pwfseq  8288  gch2  8303  axgroth3  8455  inaprc  8460  nlt1pi  8532  indpi  8533  1re  8839  mul02lem2  8991  addid1  8994  fimaxre  9703  supmul1  9721  inelr  9738  rimul  9739  nnge1  9774  zneo  10096  uzindOLD  10108  ltweuz  11026  hashf1lem2  11396  climuni  12028  fsum2d  12236  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  efne0  12379  ruclem13  12522  dvdslelem  12575  divalglem0  12594  prmreclem2  12966  prmreclem3  12967  mreexexd  13552  coaval  13902  xpcco  13959  pltirr  14099  frgpnabllem1  15163  ablfac1eulem  15309  mretopd  16831  fiuncmp  17133  ptcmpfi  17506  filtop  17552  supnfcls  17717  flimfnfcls  17725  alexsubALTlem2  17744  alexsubALTlem4  17746  rectbntr0  18339  fsumcn  18376  bcthlem2  18749  ovoliunlem3  18865  ovolicc2lem4  18881  dyadmax  18955  vitali  18970  itgfsum  19183  dvmptfsum  19324  fta1g  19555  fta1  19690  aannenlem1  19710  aalioulem3  19716  logltb  19955  logdmn0  19989  ang180lem2  20110  angpined  20129  mumullem2  20420  dchrisum0re  20664  chpdifbnd  20706  pntrlog2bnd  20735  pntibndlem3  20743  pnt3  20763  dvrunz  21102  hiidge0  21679  chsupval  21916  chsupcl  21921  chsupss  21923  ococin  21989  chsupval2  21991  ssjo  22028  h1de2i  22134  pjss2i  22261  pjssmii  22262  sto2i  22819  stge1i  22820  stle0i  22821  stlei  22822  stlesi  22823  stm1i  22825  staddi  22828  stadd3i  22830  golem1  22853  stcltrlem1  22858  mdexchi  22917  chirred  22977  atabsi  22983  abrexdomjm  23167  ctex  23338  probdif  23625  kur14lem9  23747  relexp1  24029  wfrlem5  24262  wfrlem16  24273  tfrALTlem  24278  frrlem5  24287  nofv  24313  noprc  24337  dffun10  24455  limsucncmpi  24886  wl-adnestantALT  24909  supaddc  24927  intopcoaconlem3  25550  lemindclsbu  26006  abrexdom  26416  heiborlem10  26555  pellexlem3  26927  pell1234qrne0  26949  hbtlem6  27344  funressnfv  28002  faovcl  28071  nbgraop  28151  isuvtx  28171  sb5ALT  28344  eexinst01  28345  a9e2eq  28379  bnj849  29030  a12stdy1-x12  29184  a12stdy1  29199  ax9lem1  29213  ax9vax9  29231  cvrnrefN  29545  pmod1i  30110  pmodN  30112  osumcllem11N  30228  pexmidlem8N  30239  pl42lem3N  30243  cdleme18b  30554  dochexmidlem8  31730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator