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  1646  ax10  1884  equveli  1928  ax11v2  1932  ax11eq  2132  ax11el  2133  ax11inda  2139  ax11v2-o  2140  pm13.183  2908  sbcth  3005  sbcth2  3074  ssun3  3340  ssun4  3341  uneqdifeq  3542  ralf0  3560  uniintsn  3899  rext  4222  exss  4236  uniopel  4270  wefrc  4387  ordun  4494  limsssuc  4641  tfisi  4649  finds1  4685  relop  4834  dmrnssfld  4938  iss  4998  sofld  5121  relcoi1  5201  nfunv  5285  funimass2  5326  fvbr0  5549  fvmptg  5600  fovcl  5949  ov3  5984  elovmpt2  6064  frxp  6225  oaordi  6544  oaword2  6551  omeulem1  6580  oeworde  6591  oelim2  6593  nnaordi  6616  oaabs2  6643  sbthlem1  6971  0domg  6988  limenpsi  7036  enp1i  7093  findcard2  7098  ordunifi  7107  fidomdm  7138  dffi3  7184  oismo  7255  wdom2d  7294  wdomima2g  7300  suc11reg  7320  elom3  7349  cantnfval2  7370  rankunb  7522  rankval4  7539  karden  7565  cardsn  7602  cardlim  7605  cardprclem  7612  fseqdom  7653  dfac12lem3  7771  kmlem2  7777  kmlem10  7785  cflim2  7889  cfslb2n  7894  fin23lem27  7954  axcc3  8064  axcc4  8065  acncc  8066  domtriomlem  8068  axdclem2  8147  imadomg  8159  alephval2  8194  alephreg  8204  axextnd  8213  fpwwe2lem10  8261  pwfseq  8286  gch2  8301  axgroth3  8453  inaprc  8458  nlt1pi  8530  indpi  8531  1re  8837  mul02lem2  8989  addid1  8992  fimaxre  9701  supmul1  9719  inelr  9736  rimul  9737  nnge1  9772  zneo  10094  uzindOLD  10106  ltweuz  11024  hashf1lem2  11394  climuni  12026  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  efne0  12377  ruclem13  12520  dvdslelem  12573  divalglem0  12592  prmreclem2  12964  prmreclem3  12965  mreexexd  13550  coaval  13900  xpcco  13957  pltirr  14097  frgpnabllem1  15161  ablfac1eulem  15307  mretopd  16829  fiuncmp  17131  ptcmpfi  17504  filtop  17550  supnfcls  17715  flimfnfcls  17723  alexsubALTlem2  17742  alexsubALTlem4  17744  rectbntr0  18337  fsumcn  18374  bcthlem2  18747  ovoliunlem3  18863  ovolicc2lem4  18879  dyadmax  18953  vitali  18968  itgfsum  19181  dvmptfsum  19322  fta1g  19553  fta1  19688  aannenlem1  19708  aalioulem3  19714  logltb  19953  logdmn0  19987  ang180lem2  20108  angpined  20127  mumullem2  20418  dchrisum0re  20662  chpdifbnd  20704  pntrlog2bnd  20733  pntibndlem3  20741  pnt3  20761  dvrunz  21100  hiidge0  21677  chsupval  21914  chsupcl  21919  chsupss  21921  ococin  21987  chsupval2  21989  ssjo  22026  h1de2i  22132  pjss2i  22259  pjssmii  22260  sto2i  22817  stge1i  22818  stle0i  22819  stlei  22820  stlesi  22821  stm1i  22823  staddi  22826  stadd3i  22828  golem1  22851  stcltrlem1  22856  mdexchi  22915  chirred  22975  atabsi  22981  abrexdomjm  23165  ctex  23336  probdif  23623  kur14lem9  23745  relexp1  24027  wfrlem5  24260  wfrlem16  24271  tfrALTlem  24276  frrlem5  24285  nofv  24311  noprc  24335  dffun10  24453  limsucncmpi  24884  wl-adnestantALT  24907  intopcoaconlem3  25539  lemindclsbu  25995  abrexdom  26405  heiborlem10  26544  pellexlem3  26916  pell1234qrne0  26938  hbtlem6  27333  funressnfv  27991  faovcl  28060  nbgraop  28140  isuvtx  28160  sb5ALT  28288  eexinst01  28289  a9e2eq  28323  bnj849  28957  a12stdy1-x12  29111  a12stdy1  29126  ax9lem1  29140  ax9vax9  29158  cvrnrefN  29472  pmod1i  30037  pmodN  30039  osumcllem11N  30155  pexmidlem8N  30166  pl42lem3N  30170  cdleme18b  30481  dochexmidlem8  31657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator