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

Theorem expimpd 601
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 432 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 429 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ornld  896  ralrimdva  2800  disjiun  4358  reusv3  4573  ralxfrd  4576  euotd  4662  swopo  4724  wereu2  4790  oneqmini  4843  poirr2  5304  sossfld  5363  elpreima  5909  suppssOLD  5922  fmptco  5966  isofrlem  6137  onmindif2  6546  frxp  6809  fnse  6816  suppss  6848  tposfo2  6896  tz7.48-2  7025  omeulem1  7149  omeu  7152  nnaordex  7205  pssnn  7654  fodomfib  7715  dffi3  7806  supmo  7826  supnub  7836  cantnfle  8003  cantnflem1  8021  cantnfleOLD  8033  cantnflem1OLD  8044  epfrs  8075  alephord2i  8371  cardinfima  8391  aceq3lem  8414  dfac2  8424  dfac12lem2  8437  axdc2lem  8741  ttukeylem6  8807  alephval2  8860  fpwwe2lem12  8930  fpwwe2lem13  8931  prlem934  9322  reclem4pr  9339  suplem1pr  9341  letr  9589  sup2  10415  uzind  10871  xrletr  11282  xltnegi  11336  xlemul1a  11401  ixxssixx  11464  difreicc  11573  flval3  11850  fsequb  11988  seqf1olem1  12049  expnegz  12103  relexprelg  12873  shftlem  12903  rexuzre  13187  cau3lem  13189  caubnd2  13192  caubnd  13193  climrlim2  13372  climuni  13377  2clim  13397  o1co  13411  rlimno1  13478  climbdd  13496  caurcvg  13501  summolem2  13540  summo  13541  zsum  13542  fsumf1o  13547  fsumss  13549  fsumcl2lem  13555  fsumadd  13563  fsummulc2  13601  fsumconst  13607  fsumrelem  13623  prodmolem2  13744  prodmo  13745  zprod  13746  fprodf1o  13755  fprodss  13757  fprodcl2lem  13759  fprodmul  13767  fproddiv  13768  fprodconst  13784  fprodn0  13785  prmpwdvds  14424  infpnlem1  14430  1arith  14447  vdwapun  14494  vdwlem11  14511  vdwnnlem2  14516  ramz  14545  ramcl  14549  prmlem0  14593  firest  14840  catpropd  15115  initoid  15401  termoid  15402  initoeu2lem1  15410  pltnle  15713  pltletr  15718  pospo  15720  psss  15961  isgrpid2  16203  f1omvdco2  16590  pgpfi  16742  frgpnabllem1  16994  gsumval3eu  17024  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzresOLD  17035  gsumzclOLD  17036  gsumzf1oOLD  17037  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumconst  17070  gsumzmhm  17073  gsumzmhmOLD  17074  gsumzoppg  17083  gsumzoppgOLD  17084  ablfaclem3  17251  dvdsrtr  17414  dvdsrmul1  17415  unitgrp  17429  lspsolvlem  17901  domnmuln0  18060  gsummoncoe1  18459  pf1ind  18504  gsumfsum  18597  obslbs  18852  dmatscmcl  19090  scmatmulcl  19105  smatvscl  19111  mdetdiaglem  19185  cpmatinvcl  19303  mp2pm2mplem4  19395  cpmadugsumlemF  19462  eltg3  19548  tgidm  19567  neindisj  19704  tgrest  19746  restcld  19759  tgcn  19839  lmcnp  19891  iunconlem  20013  2ndcredom  20036  2ndc1stc  20037  1stcrest  20039  2ndcrest  20040  2ndcdisj  20042  nllyrest  20072  nllyidm  20075  lfinpfin  20110  locfincmp  20112  ptpjpre1  20157  ptuni2  20162  ptbasin  20163  ptbasfi  20167  txbasval  20192  ptpjopn  20198  ptclsg  20201  dfac14lem  20203  xkoccn  20205  txcnp  20206  ptcnplem  20207  ptcnp  20208  txtube  20226  txcmplem1  20227  txcmplem2  20228  tx2ndc  20237  txkgen  20238  xkoco1cn  20243  xkoco2cn  20244  xkococnlem  20245  xkococn  20246  xkoinjcn  20273  qtoprest  20303  kqsat  20317  kqcldsat  20319  isfild  20444  fbunfip  20455  fgabs  20465  filcon  20469  fbasrn  20470  filufint  20506  elfm2  20534  elfm3  20536  fmfnfm  20544  hausflimi  20566  cnpflfi  20585  ptcmplem2  20638  tmdgsum2  20680  cldsubg  20694  qustgpopn  20703  ustfilxp  20800  bldisj  20986  xbln0  21002  blssps  21012  blss  21013  blssexps  21014  blssex  21015  blcls  21094  metcnp3  21128  icccmplem2  21413  cnheibor  21540  iscau4  21803  ovolshftlem2  22006  ovolicc2lem5  22017  dyadmax  22092  mbfi1fseqlem4  22210  mbfi1flimlem  22214  lhop1lem  22499  dvfsumrlim  22517  aalioulem3  22815  ulmcn  22879  radcnvlt1  22898  pilem2  22932  efopn  23126  cxpeq0  23146  cxpmul2z  23159  cxpcn3lem  23208  xrlimcnp  23415  vmappw  23507  fsumvma  23605  dchrptlem1  23656  lgsqr  23738  lgsdchrval  23739  2sqlem6  23761  2sqlem7  23762  pntlem3  23911  pntleml  23913  brbtwn  24323  brcgr  24324  axcontlem8  24395  cusgrafilem2  24601  redwlk  24729  4cycl4dv  24788  cusconngra  24797  usg2wlkeq  24829  usg2spthonot  25009  usg2spthonot0  25010  frg2woteq  25181  pjhthmo  26337  spansncvi  26687  nmcexi  27061  cnlnssadj  27115  leopmuli  27168  elpjrn  27225  mdsl0  27345  sumdmdii  27450  fmptcof2  27643  suppss3  27700  lmxrge0  28088  erdszelem7  28830  sconpi1  28873  cvmsval  28900  cvmopnlem  28912  cvmfolem  28913  cvmliftmolem2  28916  cvmlift2lem10  28946  cvmlift2lem12  28948  cvmlift3lem5  28957  cvmlift3lem8  28960  trpredrec  29486  wfr3g  29507  frr3g  29551  sltval2  29581  linethru  29956  finixpnum  30203  heicant  30214  voliunnfl  30223  volsupnfl  30224  itg2addnclem  30232  opnrebl2  30305  neibastop2lem  30344  neibastop2  30345  unirep  30369  sdclem2  30401  istotbnd3  30433  ssbnd  30450  incssnn0  30809  eldioph4b  30910  diophren  30912  fphpdo  30916  rencldnfilem  30919  pellexlem5  30934  pell1234qrne0  30954  pell1234qrmulcl  30956  pell14qrgt0  30960  pell1234qrdich  30962  pell14qrdich  30970  pell1qrge1  30971  pell1qrgap  30975  pellfundre  30982  pellfundlb  30985  dvdsacongtr  31087  jm2.19lem4  31100  aomclem4  31169  hbtlem2  31241  hbtlem4  31243  hbtlem6  31246  ordpss  31528  opoeALTV  32525  opeoALTV  32526  nzerooringczr  33080  ellcoellss  33236  nn0sumshdiglem1  33442  bnj594  34317  bnj849  34330  bj-cbv3ta  34617  lshpdisj  35125  lsatn0  35137  lsat0cv  35171  cvrletrN  35411  cvrval4N  35551  lncvrelatN  35918  paddasslem14  35970  paddasslem15  35971  paddasslem16  35972  pmapjoin  35989  dihglblem2N  37434  dochvalr  37497
  Copyright terms: Public domain W3C validator