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

Theorem expimpd 587
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 421 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  disjiun  4170  euotd  4425  swopo  4481  wereu2  4547  oneqmini  4600  reusv3  4698  ralxfrd  4704  onmindif2  4759  poirr2  5225  sossfld  5284  elpreima  5817  suppss  5830  fmptco  5868  isofrlem  6027  frxp  6423  fnse  6430  tposfo2  6469  tz7.48-2  6666  omeulem1  6792  omeu  6795  nnaordex  6848  th3qlem1  6977  pssnn  7294  fodomfib  7353  dffi3  7402  supmo  7421  supnub  7431  cantnfle  7590  cantnflem1  7609  epfrs  7631  alephord2i  7922  cardinfima  7942  aceq3lem  7965  dfac2  7975  dfac12lem2  7988  axdc2lem  8292  ttukeylem6  8358  alephval2  8411  fpwwe2lem12  8480  fpwwe2lem13  8481  prlem934  8874  reclem4pr  8891  suplem1pr  8893  letr  9131  sup2  9928  uzind  10325  xrletr  10712  xltnegi  10766  xlemul1a  10831  ixxssixx  10894  difreicc  10992  flval3  11185  fsequb  11277  seqf1olem1  11325  expnegz  11377  shftlem  11846  rexuzre  12119  cau3lem  12121  caubnd2  12124  caubnd  12125  climrlim2  12304  climuni  12309  2clim  12329  o1co  12343  rlimno1  12410  climbdd  12428  caurcvg  12433  summolem2  12473  summo  12474  zsum  12475  fsumf1o  12480  fsumss  12482  fsumcl2lem  12488  fsumadd  12495  fsummulc2  12530  fsumconst  12536  fsumrelem  12549  prmpwdvds  13235  infpnlem1  13241  1arith  13258  vdwapun  13305  vdwlem11  13322  vdwnnlem2  13327  ramz  13356  ramcl  13360  prmlem0  13391  firest  13623  catpropd  13898  pltnle  14386  pltletr  14391  pospo  14393  psss  14609  isgrpid2  14804  pgpfi  15202  frgpnabllem1  15447  gsumval3eu  15476  gsumzres  15480  gsumzcl  15481  gsumzf1o  15482  gsumzaddlem  15489  gsumconst  15495  gsumzmhm  15496  gsumzoppg  15502  ablfaclem3  15608  dvdsrtr  15720  dvdsrmul1  15721  unitgrp  15735  lspsolvlem  16177  domnmuln0  16321  gsumfsum  16729  obslbs  16920  eltg3  16990  tgidm  17008  neindisj  17144  tgrest  17185  restcld  17198  tgcn  17278  lmcnp  17330  iunconlem  17451  2ndcredom  17474  2ndc1stc  17475  1stcrest  17477  2ndcrest  17478  2ndcdisj  17480  nllyrest  17510  nllyidm  17513  ptpjpre1  17564  ptuni2  17569  ptbasin  17570  ptbasfi  17574  txbasval  17599  ptpjopn  17605  ptclsg  17608  dfac14lem  17610  xkoccn  17612  txcnp  17613  ptcnplem  17614  ptcnp  17615  txtube  17633  txcmplem1  17634  txcmplem2  17635  tx2ndc  17644  txkgen  17645  xkoco1cn  17650  xkoco2cn  17651  xkococnlem  17652  xkococn  17653  xkoinjcn  17680  qtoprest  17710  kqsat  17724  kqcldsat  17726  isfild  17851  fbunfip  17862  fgabs  17872  filcon  17876  fbasrn  17877  filufint  17913  elfm2  17941  elfm3  17943  fmfnfm  17951  hausflimi  17973  cnpflfi  17992  ptcmplem2  18045  tmdgsum2  18087  cldsubg  18101  divstgpopn  18110  ustfilxp  18203  bldisj  18389  xbln0  18405  blssps  18415  blss  18416  blssexps  18417  blssex  18418  blcls  18497  metcnp3  18531  icccmplem2  18815  cnheibor  18941  iscau4  19193  ovolshftlem2  19367  ovolicc2lem5  19378  dyadmax  19451  mbfi1fseqlem4  19571  mbfi1flimlem  19575  lhop1lem  19858  dvfsumrlim  19876  pf1ind  19936  aalioulem3  20212  ulmcn  20276  radcnvlt1  20295  pilem2  20329  efopn  20510  cxpeq0  20530  cxpmul2z  20543  cxpcn3lem  20592  xrlimcnp  20768  vmappw  20860  fsumvma  20958  dchrptlem1  21009  lgsqr  21091  lgsdchrval  21092  2sqlem6  21114  2sqlem7  21115  pntlem3  21264  pntleml  21266  cusgrafilem2  21450  redwlk  21567  4cycl4dv  21615  cusconngra  21624  pjhthmo  22765  spansncvi  23115  nmcexi  23490  cnlnssadj  23544  leopmuli  23597  elpjrn  23654  mdsl0  23774  sumdmdii  23879  fmptcof2  24037  lmxrge0  24298  erdszelem7  24844  sconpi1  24887  cvmsval  24914  cvmopnlem  24926  cvmfolem  24927  cvmliftmolem2  24930  cvmlift2lem10  24960  cvmlift2lem12  24962  cvmlift3lem5  24971  cvmlift3lem8  24974  prodmolem2  25222  prodmo  25223  zprod  25224  fprodf1o  25233  fprodss  25235  fprodcl2lem  25237  fprodmul  25245  fproddiv  25246  fprodconst  25263  fprodn0  25264  trpredrec  25463  wfr3g  25477  frr3g  25502  sltval2  25532  brbtwn  25750  brcgr  25751  axcontlem8  25822  linethru  25999  voliunnfl  26157  volsupnfl  26158  itg2addnclem  26163  opnrebl2  26222  lfinpfin  26281  locfincmp  26282  neibastop2lem  26287  neibastop2  26288  unirep  26312  sdclem2  26344  istotbnd3  26378  ssbnd  26395  incssnn0  26663  eldioph4b  26770  diophren  26772  fphpdo  26776  rencldnfilem  26779  pellexlem5  26794  pell1234qrne0  26814  pell1234qrmulcl  26816  pell14qrgt0  26820  pell1234qrdich  26822  pell14qrdich  26830  pell1qrge1  26831  pell1qrgap  26835  pellfundre  26842  pellfundlb  26845  dvdsacongtr  26947  jm2.19lem4  26961  aomclem4  27030  hbtlem2  27204  hbtlem4  27206  hbtlem6  27209  f1omvdco2  27267  ordpss  27529  swrd0swrd  28017  usg2spthonot  28093  usg2spthonot0  28094  frg2woteq  28171  bnj594  29001  bnj849  29014  lshpdisj  29482  lsatn0  29494  lsat0cv  29528  cvrletrN  29768  cvrval4N  29908  lncvrelatN  30275  paddasslem14  30327  paddasslem15  30328  paddasslem16  30329  pmapjoin  30346  dihglblem2N  31789  dochvalr  31852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator