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

Theorem expimpd 598
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 ) ) )
32imp3a 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:  disjiun  4270  reusv3  4488  ralxfrd  4494  euotd  4580  swopo  4638  wereu2  4704  oneqmini  4757  poirr2  5210  sossfld  5273  elpreima  5811  suppssOLD  5824  fmptco  5863  isofrlem  6018  onmindif2  6412  frxp  6671  fnse  6678  suppss  6708  tposfo2  6757  tz7.48-2  6883  omeulem1  7009  omeu  7012  nnaordex  7065  th3qlem1  7194  pssnn  7519  fodomfib  7579  dffi3  7669  supmo  7690  supnub  7700  cantnfle  7867  cantnflem1  7885  cantnfleOLD  7897  cantnflem1OLD  7908  epfrs  7939  alephord2i  8235  cardinfima  8255  aceq3lem  8278  dfac2  8288  dfac12lem2  8301  axdc2lem  8605  ttukeylem6  8671  alephval2  8724  fpwwe2lem12  8796  fpwwe2lem13  8797  prlem934  9190  reclem4pr  9207  suplem1pr  9209  letr  9456  sup2  10274  uzind  10721  xrletr  11120  xltnegi  11174  xlemul1a  11239  ixxssixx  11302  difreicc  11404  flval3  11647  fsequb  11781  seqf1olem1  11829  expnegz  11882  swrdsymbeq  12325  shftlem  12541  rexuzre  12824  cau3lem  12826  caubnd2  12829  caubnd  12830  climrlim2  13009  climuni  13014  2clim  13034  o1co  13048  rlimno1  13115  climbdd  13133  caurcvg  13138  summolem2  13177  summo  13178  zsum  13179  fsumf1o  13184  fsumss  13186  fsumcl2lem  13192  fsumadd  13199  fsummulc2  13234  fsumconst  13240  fsumrelem  13253  prmpwdvds  13948  infpnlem1  13954  1arith  13971  vdwapun  14018  vdwlem11  14035  vdwnnlem2  14040  ramz  14069  ramcl  14073  prmlem0  14116  firest  14354  catpropd  14631  pltnle  15119  pltletr  15124  pospo  15126  psss  15367  isgrpid2  15554  f1omvdco2  15934  pgpfi  16084  frgpnabllem1  16331  gsumval3eu  16361  gsumzres  16368  gsumzcl2  16369  gsumzf1o  16371  gsumzresOLD  16372  gsumzclOLD  16373  gsumzf1oOLD  16374  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsumzoppg  16416  gsumzoppgOLD  16417  ablfaclem3  16562  dvdsrtr  16678  dvdsrmul1  16679  unitgrp  16693  lspsolvlem  17145  domnmuln0  17292  gsumfsum  17723  obslbs  17997  eltg3  18409  tgidm  18427  neindisj  18563  tgrest  18605  restcld  18618  tgcn  18698  lmcnp  18750  iunconlem  18873  2ndcredom  18896  2ndc1stc  18897  1stcrest  18899  2ndcrest  18900  2ndcdisj  18902  nllyrest  18932  nllyidm  18935  ptpjpre1  18986  ptuni2  18991  ptbasin  18992  ptbasfi  18996  txbasval  19021  ptpjopn  19027  ptclsg  19030  dfac14lem  19032  xkoccn  19034  txcnp  19035  ptcnplem  19036  ptcnp  19037  txtube  19055  txcmplem1  19056  txcmplem2  19057  tx2ndc  19066  txkgen  19067  xkoco1cn  19072  xkoco2cn  19073  xkococnlem  19074  xkococn  19075  xkoinjcn  19102  qtoprest  19132  kqsat  19146  kqcldsat  19148  isfild  19273  fbunfip  19284  fgabs  19294  filcon  19298  fbasrn  19299  filufint  19335  elfm2  19363  elfm3  19365  fmfnfm  19373  hausflimi  19395  cnpflfi  19414  ptcmplem2  19467  tmdgsum2  19509  cldsubg  19523  divstgpopn  19532  ustfilxp  19629  bldisj  19815  xbln0  19831  blssps  19841  blss  19842  blssexps  19843  blssex  19844  blcls  19923  metcnp3  19957  icccmplem2  20242  cnheibor  20369  iscau4  20632  ovolshftlem2  20835  ovolicc2lem5  20846  dyadmax  20920  mbfi1fseqlem4  21038  mbfi1flimlem  21042  lhop1lem  21327  dvfsumrlim  21345  pf1ind  21406  aalioulem3  21685  ulmcn  21749  radcnvlt1  21768  pilem2  21802  efopn  21988  cxpeq0  22008  cxpmul2z  22021  cxpcn3lem  22070  xrlimcnp  22247  vmappw  22339  fsumvma  22437  dchrptlem1  22488  lgsqr  22570  lgsdchrval  22571  2sqlem6  22593  2sqlem7  22594  pntlem3  22743  pntleml  22745  brbtwn  22968  brcgr  22969  axcontlem8  23040  cusgrafilem2  23211  redwlk  23328  4cycl4dv  23376  cusconngra  23385  pjhthmo  24528  spansncvi  24878  nmcexi  25253  cnlnssadj  25307  leopmuli  25360  elpjrn  25417  mdsl0  25537  sumdmdii  25642  fmptcof2  25803  suppss3  25851  fpwrelmap  25858  lmxrge0  26236  erdszelem7  26933  sconpi1  26976  cvmsval  27003  cvmopnlem  27015  cvmfolem  27016  cvmliftmolem2  27019  cvmlift2lem10  27049  cvmlift2lem12  27051  cvmlift3lem5  27060  cvmlift3lem8  27063  prodmolem2  27295  prodmo  27296  zprod  27297  fprodf1o  27306  fprodss  27308  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodconst  27336  fprodn0  27337  trpredrec  27549  wfr3g  27570  frr3g  27614  sltval2  27644  linethru  28031  finixpnum  28258  heicant  28270  voliunnfl  28279  volsupnfl  28280  itg2addnclem  28287  opnrebl2  28360  lfinpfin  28419  locfincmp  28420  neibastop2lem  28425  neibastop2  28426  unirep  28450  sdclem2  28482  istotbnd3  28514  ssbnd  28531  incssnn0  28892  eldioph4b  28995  diophren  28997  fphpdo  29001  rencldnfilem  29004  pellexlem5  29019  pell1234qrne0  29039  pell1234qrmulcl  29041  pell14qrgt0  29045  pell1234qrdich  29047  pell14qrdich  29055  pell1qrge1  29056  pell1qrgap  29060  pellfundre  29067  pellfundlb  29070  dvdsacongtr  29172  jm2.19lem4  29186  aomclem4  29255  hbtlem2  29325  hbtlem4  29327  hbtlem6  29330  ordpss  29552  usg2wlkeq  30135  usg2spthonot  30253  usg2spthonot0  30254  frg2woteq  30499  ellcoellss  30678  bnj594  31607  bnj849  31620  bj-cbv3ta  31837  lshpdisj  32205  lsatn0  32217  lsat0cv  32251  cvrletrN  32491  cvrval4N  32631  lncvrelatN  32998  paddasslem14  33050  paddasslem15  33051  paddasslem16  33052  pmapjoin  33069  dihglblem2N  34512  dochvalr  34575
  Copyright terms: Public domain W3C validator