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  1664  ax10  1897  equveli  1941  ax11v2  1945  ax11eq  2145  ax11el  2146  ax11inda  2152  ax11v2-o  2153  pm13.183  2921  sbcth  3018  sbcth2  3087  ssun3  3353  ssun4  3354  uneqdifeq  3555  ralf0  3573  uniintsn  3915  rext  4238  exss  4252  uniopel  4286  wefrc  4403  ordun  4510  limsssuc  4657  tfisi  4665  finds1  4701  relop  4850  dmrnssfld  4954  iss  5014  sofld  5137  relcoi1  5217  nfunv  5301  funimass2  5342  fvbr0  5565  fvmptg  5616  fovcl  5965  ov3  6000  elovmpt2  6080  frxp  6241  oaordi  6560  oaword2  6567  omeulem1  6596  oeworde  6607  oelim2  6609  nnaordi  6632  oaabs2  6659  sbthlem1  6987  0domg  7004  limenpsi  7052  enp1i  7109  findcard2  7114  ordunifi  7123  fidomdm  7154  dffi3  7200  oismo  7271  wdom2d  7310  wdomima2g  7316  suc11reg  7336  elom3  7365  cantnfval2  7386  rankunb  7538  rankval4  7555  karden  7581  cardsn  7618  cardlim  7621  cardprclem  7628  fseqdom  7669  dfac12lem3  7787  kmlem2  7793  kmlem10  7801  cflim2  7905  cfslb2n  7910  fin23lem27  7970  axcc3  8080  axcc4  8081  acncc  8082  domtriomlem  8084  axdclem2  8163  imadomg  8175  alephval2  8210  alephreg  8220  axextnd  8229  fpwwe2lem10  8277  pwfseq  8302  gch2  8317  axgroth3  8469  inaprc  8474  nlt1pi  8546  indpi  8547  1re  8853  mul02lem2  9005  addid1  9008  fimaxre  9717  supmul1  9735  inelr  9752  rimul  9753  nnge1  9788  zneo  10110  uzindOLD  10122  ltweuz  11040  hashf1lem2  11410  climuni  12042  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  efne0  12393  ruclem13  12536  dvdslelem  12589  divalglem0  12608  prmreclem2  12980  prmreclem3  12981  mreexexd  13566  coaval  13916  xpcco  13973  pltirr  14113  frgpnabllem1  15177  ablfac1eulem  15323  mretopd  16845  fiuncmp  17147  ptcmpfi  17520  filtop  17566  supnfcls  17731  flimfnfcls  17739  alexsubALTlem2  17758  alexsubALTlem4  17760  rectbntr0  18353  fsumcn  18390  bcthlem2  18763  ovoliunlem3  18879  ovolicc2lem4  18895  dyadmax  18969  vitali  18984  itgfsum  19197  dvmptfsum  19338  fta1g  19569  fta1  19704  aannenlem1  19724  aalioulem3  19730  logltb  19969  logdmn0  20003  ang180lem2  20124  angpined  20143  mumullem2  20434  dchrisum0re  20678  chpdifbnd  20720  pntrlog2bnd  20749  pntibndlem3  20757  pnt3  20777  dvrunz  21116  hiidge0  21693  chsupval  21930  chsupcl  21935  chsupss  21937  ococin  22003  chsupval2  22005  ssjo  22042  h1de2i  22148  pjss2i  22275  pjssmii  22276  sto2i  22833  stge1i  22834  stle0i  22835  stlei  22836  stlesi  22837  stm1i  22839  staddi  22842  stadd3i  22844  golem1  22867  stcltrlem1  22872  mdexchi  22931  chirred  22991  atabsi  22997  abrexdomjm  23181  ctex  23351  probdif  23638  kur14lem9  23760  relexp1  24042  wfrlem5  24331  wfrlem16  24342  tfrALTlem  24347  frrlem5  24356  nofv  24382  noprc  24406  dffun10  24524  limsucncmpi  24956  wl-adnestantALT  24979  supaddc  24995  intopcoaconlem3  25642  lemindclsbu  26098  abrexdom  26508  heiborlem10  26647  pellexlem3  27019  pell1234qrne0  27041  hbtlem6  27436  funressnfv  28096  faovcl  28168  nbgraop  28274  isuvtx  28301  sb5ALT  28587  eexinst01  28588  a9e2eq  28622  bnj849  29273  ax10NEW7  29450  equveliNEW7  29503  ax11v2NEW7  29505  a12stdy1-x12  29733  a12stdy1  29748  ax9lem1  29762  ax9vax9  29780  cvrnrefN  30094  pmod1i  30659  pmodN  30661  osumcllem11N  30777  pexmidlem8N  30788  pl42lem3N  30792  cdleme18b  31103  dochexmidlem8  32279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator