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

Theorem expimpd 603
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expimpd.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
expimpd  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 431 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ornld  898  ralrimdva  2861  disjiun  4427  reusv3  4645  ralxfrd  4651  euotd  4738  swopo  4800  wereu2  4866  oneqmini  4919  poirr2  5381  sossfld  5444  elpreima  5992  suppssOLD  6005  fmptco  6049  isofrlem  6221  onmindif2  6632  frxp  6895  fnse  6902  suppss  6932  tposfo2  6980  tz7.48-2  7109  omeulem1  7233  omeu  7236  nnaordex  7289  pssnn  7740  fodomfib  7802  dffi3  7893  supmo  7914  supnub  7924  cantnfle  8093  cantnflem1  8111  cantnfleOLD  8123  cantnflem1OLD  8134  epfrs  8165  alephord2i  8461  cardinfima  8481  aceq3lem  8504  dfac2  8514  dfac12lem2  8527  axdc2lem  8831  ttukeylem6  8897  alephval2  8950  fpwwe2lem12  9022  fpwwe2lem13  9023  prlem934  9414  reclem4pr  9431  suplem1pr  9433  letr  9681  sup2  10506  uzind  10961  xrletr  11372  xltnegi  11426  xlemul1a  11491  ixxssixx  11554  difreicc  11663  flval3  11933  fsequb  12067  seqf1olem1  12128  expnegz  12182  swrdsymbeq  12654  shftlem  12883  rexuzre  13167  cau3lem  13169  caubnd2  13172  caubnd  13173  climrlim2  13352  climuni  13357  2clim  13377  o1co  13391  rlimno1  13458  climbdd  13476  caurcvg  13481  summolem2  13520  summo  13521  zsum  13522  fsumf1o  13527  fsumss  13529  fsumcl2lem  13535  fsumadd  13543  fsummulc2  13581  fsumconst  13587  fsumrelem  13603  prodmolem2  13724  prodmo  13725  zprod  13726  fprodf1o  13735  fprodss  13737  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodconst  13764  fprodn0  13765  prmpwdvds  14404  infpnlem1  14410  1arith  14427  vdwapun  14474  vdwlem11  14491  vdwnnlem2  14496  ramz  14525  ramcl  14529  prmlem0  14573  firest  14812  catpropd  15086  pltnle  15575  pltletr  15580  pospo  15582  psss  15823  isgrpid2  16065  f1omvdco2  16452  pgpfi  16604  frgpnabllem1  16856  gsumval3eu  16886  gsumzres  16893  gsumzcl2  16894  gsumzf1o  16896  gsumzresOLD  16897  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  gsumzoppgOLD  16947  ablfaclem3  17117  dvdsrtr  17280  dvdsrmul1  17281  unitgrp  17295  lspsolvlem  17767  domnmuln0  17926  gsummoncoe1  18325  pf1ind  18370  gsumfsum  18463  obslbs  18739  dmatscmcl  18983  scmatmulcl  18998  smatvscl  19004  mdetdiaglem  19078  cpmatinvcl  19196  mp2pm2mplem4  19288  cpmadugsumlemF  19355  eltg3  19441  tgidm  19460  neindisj  19596  tgrest  19638  restcld  19651  tgcn  19731  lmcnp  19783  iunconlem  19906  2ndcredom  19929  2ndc1stc  19930  1stcrest  19932  2ndcrest  19933  2ndcdisj  19935  nllyrest  19965  nllyidm  19968  lfinpfin  20003  locfincmp  20005  ptpjpre1  20050  ptuni2  20055  ptbasin  20056  ptbasfi  20060  txbasval  20085  ptpjopn  20091  ptclsg  20094  dfac14lem  20096  xkoccn  20098  txcnp  20099  ptcnplem  20100  ptcnp  20101  txtube  20119  txcmplem1  20120  txcmplem2  20121  tx2ndc  20130  txkgen  20131  xkoco1cn  20136  xkoco2cn  20137  xkococnlem  20138  xkococn  20139  xkoinjcn  20166  qtoprest  20196  kqsat  20210  kqcldsat  20212  isfild  20337  fbunfip  20348  fgabs  20358  filcon  20362  fbasrn  20363  filufint  20399  elfm2  20427  elfm3  20429  fmfnfm  20437  hausflimi  20459  cnpflfi  20478  ptcmplem2  20531  tmdgsum2  20573  cldsubg  20587  qustgpopn  20596  ustfilxp  20693  bldisj  20879  xbln0  20895  blssps  20905  blss  20906  blssexps  20907  blssex  20908  blcls  20987  metcnp3  21021  icccmplem2  21306  cnheibor  21433  iscau4  21696  ovolshftlem2  21899  ovolicc2lem5  21910  dyadmax  21985  mbfi1fseqlem4  22103  mbfi1flimlem  22107  lhop1lem  22392  dvfsumrlim  22410  aalioulem3  22708  ulmcn  22772  radcnvlt1  22791  pilem2  22825  efopn  23017  cxpeq0  23037  cxpmul2z  23050  cxpcn3lem  23099  xrlimcnp  23276  vmappw  23368  fsumvma  23466  dchrptlem1  23517  lgsqr  23599  lgsdchrval  23600  2sqlem6  23622  2sqlem7  23623  pntlem3  23772  pntleml  23774  brbtwn  24180  brcgr  24181  axcontlem8  24252  cusgrafilem2  24458  redwlk  24586  4cycl4dv  24645  cusconngra  24654  usg2wlkeq  24686  usg2spthonot  24866  usg2spthonot0  24867  frg2woteq  25038  pjhthmo  26198  spansncvi  26548  nmcexi  26923  cnlnssadj  26977  leopmuli  27030  elpjrn  27087  mdsl0  27207  sumdmdii  27312  fmptcof2  27480  suppss3  27528  lmxrge0  27912  erdszelem7  28619  sconpi1  28662  cvmsval  28689  cvmopnlem  28701  cvmfolem  28702  cvmliftmolem2  28705  cvmlift2lem10  28735  cvmlift2lem12  28737  cvmlift3lem5  28746  cvmlift3lem8  28749  trpredrec  29297  wfr3g  29318  frr3g  29362  sltval2  29392  linethru  29779  finixpnum  30014  heicant  30025  voliunnfl  30034  volsupnfl  30035  itg2addnclem  30042  opnrebl2  30115  neibastop2lem  30154  neibastop2  30155  unirep  30179  sdclem2  30211  istotbnd3  30243  ssbnd  30260  incssnn0  30619  eldioph4b  30721  diophren  30723  fphpdo  30727  rencldnfilem  30730  pellexlem5  30745  pell1234qrne0  30765  pell1234qrmulcl  30767  pell14qrgt0  30771  pell1234qrdich  30773  pell14qrdich  30781  pell1qrge1  30782  pell1qrgap  30786  pellfundre  30793  pellfundlb  30796  dvdsacongtr  30898  jm2.19lem4  30910  aomclem4  30979  hbtlem2  31049  hbtlem4  31051  hbtlem6  31054  ordpss  31314  ellcoellss  32906  bnj594  33838  bnj849  33851  bj-cbv3ta  34153  lshpdisj  34587  lsatn0  34599  lsat0cv  34633  cvrletrN  34873  cvrval4N  35013  lncvrelatN  35380  paddasslem14  35432  paddasslem15  35433  paddasslem16  35434  pmapjoin  35451  dihglblem2N  36896  dochvalr  36959
  Copyright terms: Public domain W3C validator