MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expimpd Structured version   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  4202  euotd  4457  swopo  4513  wereu2  4579  oneqmini  4632  reusv3  4731  ralxfrd  4737  onmindif2  4792  poirr2  5258  sossfld  5317  elpreima  5850  suppss  5863  fmptco  5901  isofrlem  6060  frxp  6456  fnse  6463  tposfo2  6502  tz7.48-2  6699  omeulem1  6825  omeu  6828  nnaordex  6881  th3qlem1  7010  pssnn  7327  fodomfib  7386  dffi3  7436  supmo  7457  supnub  7467  cantnfle  7626  cantnflem1  7645  epfrs  7667  alephord2i  7958  cardinfima  7978  aceq3lem  8001  dfac2  8011  dfac12lem2  8024  axdc2lem  8328  ttukeylem6  8394  alephval2  8447  fpwwe2lem12  8516  fpwwe2lem13  8517  prlem934  8910  reclem4pr  8927  suplem1pr  8929  letr  9167  sup2  9964  uzind  10361  xrletr  10748  xltnegi  10802  xlemul1a  10867  ixxssixx  10930  difreicc  11028  flval3  11222  fsequb  11314  seqf1olem1  11362  expnegz  11414  shftlem  11883  rexuzre  12156  cau3lem  12158  caubnd2  12161  caubnd  12162  climrlim2  12341  climuni  12346  2clim  12366  o1co  12380  rlimno1  12447  climbdd  12465  caurcvg  12470  summolem2  12510  summo  12511  zsum  12512  fsumf1o  12517  fsumss  12519  fsumcl2lem  12525  fsumadd  12532  fsummulc2  12567  fsumconst  12573  fsumrelem  12586  prmpwdvds  13272  infpnlem1  13278  1arith  13295  vdwapun  13342  vdwlem11  13359  vdwnnlem2  13364  ramz  13393  ramcl  13397  prmlem0  13428  firest  13660  catpropd  13935  pltnle  14423  pltletr  14428  pospo  14430  psss  14646  isgrpid2  14841  pgpfi  15239  frgpnabllem1  15484  gsumval3eu  15513  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  gsumzoppg  15539  ablfaclem3  15645  dvdsrtr  15757  dvdsrmul1  15758  unitgrp  15772  lspsolvlem  16214  domnmuln0  16358  gsumfsum  16766  obslbs  16957  eltg3  17027  tgidm  17045  neindisj  17181  tgrest  17223  restcld  17236  tgcn  17316  lmcnp  17368  iunconlem  17490  2ndcredom  17513  2ndc1stc  17514  1stcrest  17516  2ndcrest  17517  2ndcdisj  17519  nllyrest  17549  nllyidm  17552  ptpjpre1  17603  ptuni2  17608  ptbasin  17609  ptbasfi  17613  txbasval  17638  ptpjopn  17644  ptclsg  17647  dfac14lem  17649  xkoccn  17651  txcnp  17652  ptcnplem  17653  ptcnp  17654  txtube  17672  txcmplem1  17673  txcmplem2  17674  tx2ndc  17683  txkgen  17684  xkoco1cn  17689  xkoco2cn  17690  xkococnlem  17691  xkococn  17692  xkoinjcn  17719  qtoprest  17749  kqsat  17763  kqcldsat  17765  isfild  17890  fbunfip  17901  fgabs  17911  filcon  17915  fbasrn  17916  filufint  17952  elfm2  17980  elfm3  17982  fmfnfm  17990  hausflimi  18012  cnpflfi  18031  ptcmplem2  18084  tmdgsum2  18126  cldsubg  18140  divstgpopn  18149  ustfilxp  18242  bldisj  18428  xbln0  18444  blssps  18454  blss  18455  blssexps  18456  blssex  18457  blcls  18536  metcnp3  18570  icccmplem2  18854  cnheibor  18980  iscau4  19232  ovolshftlem2  19406  ovolicc2lem5  19417  dyadmax  19490  mbfi1fseqlem4  19610  mbfi1flimlem  19614  lhop1lem  19897  dvfsumrlim  19915  pf1ind  19975  aalioulem3  20251  ulmcn  20315  radcnvlt1  20334  pilem2  20368  efopn  20549  cxpeq0  20569  cxpmul2z  20582  cxpcn3lem  20631  xrlimcnp  20807  vmappw  20899  fsumvma  20997  dchrptlem1  21048  lgsqr  21130  lgsdchrval  21131  2sqlem6  21153  2sqlem7  21154  pntlem3  21303  pntleml  21305  cusgrafilem2  21489  redwlk  21606  4cycl4dv  21654  cusconngra  21663  pjhthmo  22804  spansncvi  23154  nmcexi  23529  cnlnssadj  23583  leopmuli  23636  elpjrn  23693  mdsl0  23813  sumdmdii  23918  fmptcof2  24076  lmxrge0  24337  erdszelem7  24883  sconpi1  24926  cvmsval  24953  cvmopnlem  24965  cvmfolem  24966  cvmliftmolem2  24969  cvmlift2lem10  24999  cvmlift2lem12  25001  cvmlift3lem5  25010  cvmlift3lem8  25013  prodmolem2  25261  prodmo  25262  zprod  25263  fprodf1o  25272  fprodss  25274  fprodcl2lem  25276  fprodmul  25284  fproddiv  25285  fprodconst  25302  fprodn0  25303  trpredrec  25516  wfr3g  25537  frr3g  25581  sltval2  25611  brbtwn  25838  brcgr  25839  axcontlem8  25910  linethru  26087  voliunnfl  26250  volsupnfl  26251  itg2addnclem  26256  opnrebl2  26324  lfinpfin  26383  locfincmp  26384  neibastop2lem  26389  neibastop2  26390  unirep  26414  sdclem2  26446  istotbnd3  26480  ssbnd  26497  incssnn0  26765  eldioph4b  26872  diophren  26874  fphpdo  26878  rencldnfilem  26881  pellexlem5  26896  pell1234qrne0  26916  pell1234qrmulcl  26918  pell14qrgt0  26922  pell1234qrdich  26924  pell14qrdich  26932  pell1qrge1  26933  pell1qrgap  26937  pellfundre  26944  pellfundlb  26947  dvdsacongtr  27049  jm2.19lem4  27063  aomclem4  27132  hbtlem2  27305  hbtlem4  27307  hbtlem6  27310  f1omvdco2  27368  ordpss  27630  swdeq  28196  swrd0swrd  28197  usg2wlkeq  28304  usg2spthonot  28355  usg2spthonot0  28356  frg2woteq  28449  bnj594  29283  bnj849  29296  lshpdisj  29785  lsatn0  29797  lsat0cv  29831  cvrletrN  30071  cvrval4N  30211  lncvrelatN  30578  paddasslem14  30630  paddasslem15  30631  paddasslem16  30632  pmapjoin  30649  dihglblem2N  32092  dochvalr  32155
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