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

Theorem expimpd 606
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 432 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ornld  906  ralrimdva  2778  disjiun  4352  reusv3  4570  ralxfrd  4573  euotd  4659  swopo  4722  wereu2  4788  poirr2  5181  sossfld  5240  oneqmini  5431  elpreima  5956  fmptco  6010  isofrlem  6185  onmindif2  6592  frxp  6856  fnse  6863  suppss  6895  tposfo2  6946  wfr3g  6984  tz7.48-2  7109  omeulem1  7233  omeu  7236  nnaordex  7289  pssnn  7738  fodomfib  7799  dffi3  7893  supmo  7914  supnub  7924  infglb  7954  infnlb  7956  infmo  7959  cantnfle  8123  cantnflem1  8141  epfrs  8162  alephord2i  8454  cardinfima  8474  aceq3lem  8497  dfac2  8507  dfac12lem2  8520  axdc2lem  8824  ttukeylem6  8890  alephval2  8943  fpwwe2lem12  9012  fpwwe2lem13  9013  prlem934  9404  reclem4pr  9421  suplem1pr  9423  letr  9673  sup2  10511  uzind  10973  xrletr  11401  xltnegi  11455  xlemul1a  11520  ixxssixx  11595  difreicc  11710  flval3  11995  fsequb  12133  seqf1olem1  12197  expnegz  12251  hash2prd  12577  relexprelg  13040  shftlem  13070  rexuzre  13354  cau3lem  13356  caubnd2  13359  caubnd  13360  climrlim2  13549  climuni  13554  2clim  13574  o1co  13588  rlimno1  13655  climbdd  13673  caurcvg  13680  caurcvgOLD  13681  summolem2  13720  summo  13721  zsum  13722  fsumf1o  13727  fsumss  13729  fsumcl2lem  13735  fsumadd  13743  fsummulc2  13783  fsumconst  13789  fsumrelem  13805  prodmolem2  13927  prodmo  13928  zprod  13929  fprodf1o  13938  fprodss  13940  fprodcl2lem  13942  fprodmul  13952  fproddiv  13953  fprodconst  13970  fprodn0  13971  coprmproddvdslem  14617  prmpwdvds  14786  infpnlem1  14792  1arith  14809  vdwapun  14862  vdwlem11  14879  vdwnnlem2  14884  ramz  14921  ramcl  14925  prmlem0  15015  firest  15269  catpropd  15552  initoid  15838  termoid  15839  initoeu2lem1  15847  pltnle  16150  pltletr  16155  pospo  16157  psss  16398  isgrpid2  16640  f1omvdco2  17027  pgpfi  17195  frgpnabllem1  17447  gsumval3eu  17476  gsumzres  17481  gsumzcl2  17482  gsumzf1o  17484  gsumzaddlem  17492  gsumconst  17505  gsumzmhm  17508  gsumzoppg  17515  ablfaclem3  17658  dvdsrtr  17818  dvdsrmul1  17819  unitgrp  17833  lspsolvlem  18303  domnmuln0  18460  gsummoncoe1  18836  pf1ind  18881  gsumfsum  18972  obslbs  19230  dmatscmcl  19465  scmatmulcl  19480  smatvscl  19486  mdetdiaglem  19560  cpmatinvcl  19678  mp2pm2mplem4  19770  cpmadugsumlemF  19837  eltg3  19914  tgidm  19933  neindisj  20070  tgrest  20112  restcld  20125  tgcn  20205  lmcnp  20257  iunconlem  20379  2ndcredom  20402  2ndc1stc  20403  1stcrest  20405  2ndcrest  20406  2ndcdisj  20408  nllyrest  20438  nllyidm  20441  lfinpfin  20476  locfincmp  20478  ptpjpre1  20523  ptuni2  20528  ptbasin  20529  ptbasfi  20533  txbasval  20558  ptpjopn  20564  ptclsg  20567  dfac14lem  20569  xkoccn  20571  txcnp  20572  ptcnplem  20573  ptcnp  20574  txtube  20592  txcmplem1  20593  txcmplem2  20594  tx2ndc  20603  txkgen  20604  xkoco1cn  20609  xkoco2cn  20610  xkococnlem  20611  xkococn  20612  xkoinjcn  20639  qtoprest  20669  kqsat  20683  kqcldsat  20685  isfild  20810  fbunfip  20821  fgabs  20831  filcon  20835  fbasrn  20836  filufint  20872  elfm2  20900  elfm3  20902  fmfnfm  20910  hausflimi  20932  cnpflfi  20951  ptcmplem2  21005  tmdgsum2  21048  cldsubg  21062  qustgpopn  21071  ustfilxp  21164  bldisj  21350  xbln0  21366  blssps  21376  blss  21377  blssexps  21378  blssex  21379  blcls  21458  metcnp3  21492  icccmplem2  21778  cnheibor  21920  iscau4  22186  ovolshftlem2  22400  ovolicc2lem5  22412  dyadmax  22493  mbfi1fseqlem4  22613  mbfi1flimlem  22617  lhop1lem  22902  dvfsumrlim  22920  aalioulem3  23227  ulmcn  23291  radcnvlt1  23310  pilem2  23344  pilem2OLD  23345  efopn  23540  cxpeq0  23560  cxpmul2z  23573  cxpcn3lem  23624  xrlimcnp  23831  vmappw  23980  fsumvma  24078  dchrptlem1  24129  lgsqr  24211  lgsdchrval  24212  2sqlem6  24234  2sqlem7  24235  pntlem3  24384  pntleml  24386  brbtwn  24866  brcgr  24867  axcontlem8  24938  cusgrafilem2  25145  redwlk  25273  4cycl4dv  25332  cusconngra  25341  usg2wlkeq  25373  usg2spthonot  25553  usg2spthonot0  25554  frg2woteq  25725  pjhthmo  26892  spansncvi  27242  nmcexi  27616  cnlnssadj  27670  leopmuli  27723  elpjrn  27780  mdsl0  27900  sumdmdii  28005  fmptcof2  28200  suppss3  28257  lmxrge0  28705  bnj594  29670  bnj849  29683  erdszelem7  29867  sconpi1  29909  cvmsval  29936  cvmopnlem  29948  cvmfolem  29949  cvmliftmolem2  29952  cvmlift2lem10  29982  cvmlift2lem12  29984  cvmlift3lem5  29993  cvmlift3lem8  29996  trpredrec  30425  frr3g  30459  sltval2  30489  linethru  30864  opnrebl2  30921  neibastop2lem  30960  neibastop2  30961  bj-cbv3ta  31211  phpreu  31836  finixpnum  31837  ptrecube  31847  poimirlem26  31873  poimirlem27  31874  poimirlem31  31878  poimir  31880  heicant  31882  voliunnfl  31891  volsupnfl  31892  itg2addnclem  31900  unirep  31946  sdclem2  31978  istotbnd3  32010  ssbnd  32027  lshpdisj  32465  lsatn0  32477  lsat0cv  32511  cvrletrN  32751  cvrval4N  32891  lncvrelatN  33258  paddasslem14  33310  paddasslem15  33311  paddasslem16  33312  pmapjoin  33329  dihglblem2N  34774  dochvalr  34837  incssnn0  35465  eldioph4b  35566  diophren  35568  fphpdo  35572  rencldnfilem  35575  pellexlem5  35590  pell1234qrne0  35612  pell1234qrmulcl  35614  pell14qrgt0  35618  pell1234qrdich  35620  pell14qrdich  35628  pell1qrge1  35629  pell1qrgap  35633  pellfundre  35642  pellfundlb  35645  dvdsacongtr  35747  jm2.19lem4  35760  aomclem4  35828  hbtlem2  35896  hbtlem4  35898  hbtlem6  35901  clcnvlem  36143  ordpss  36717  opoeALTV  38625  opeoALTV  38626  gboage9  38678  nbumgrvtx  39150  cusgrfilem2  39245  nzerooringczr  39665  ellcoellss  39821  nn0sumshdiglem1  40025
  Copyright terms: Public domain W3C validator