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

Theorem expimpd 603
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 ) ) )
32impd 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:  ornld  896  ralrimdva  2882  disjiun  4437  reusv3  4655  ralxfrd  4661  euotd  4748  swopo  4810  wereu2  4876  oneqmini  4929  poirr2  5389  sossfld  5452  elpreima  5999  suppssOLD  6012  fmptco  6052  isofrlem  6222  onmindif2  6625  frxp  6890  fnse  6897  suppss  6927  tposfo2  6975  tz7.48-2  7104  omeulem1  7228  omeu  7231  nnaordex  7284  pssnn  7735  fodomfib  7796  dffi3  7887  supmo  7908  supnub  7918  cantnfle  8086  cantnflem1  8104  cantnfleOLD  8116  cantnflem1OLD  8127  epfrs  8158  alephord2i  8454  cardinfima  8474  aceq3lem  8497  dfac2  8507  dfac12lem2  8520  axdc2lem  8824  ttukeylem6  8890  alephval2  8943  fpwwe2lem12  9015  fpwwe2lem13  9016  prlem934  9407  reclem4pr  9424  suplem1pr  9426  letr  9674  sup2  10495  uzind  10948  xrletr  11357  xltnegi  11411  xlemul1a  11476  ixxssixx  11539  difreicc  11648  flval3  11914  fsequb  12048  seqf1olem1  12109  expnegz  12162  swrdsymbeq  12629  shftlem  12858  rexuzre  13141  cau3lem  13143  caubnd2  13146  caubnd  13147  climrlim2  13326  climuni  13331  2clim  13351  o1co  13365  rlimno1  13432  climbdd  13450  caurcvg  13455  summolem2  13494  summo  13495  zsum  13496  fsumf1o  13501  fsumss  13503  fsumcl2lem  13509  fsumadd  13517  fsummulc2  13555  fsumconst  13561  fsumrelem  13577  prmpwdvds  14274  infpnlem1  14280  1arith  14297  vdwapun  14344  vdwlem11  14361  vdwnnlem2  14366  ramz  14395  ramcl  14399  prmlem0  14442  firest  14681  catpropd  14958  pltnle  15446  pltletr  15451  pospo  15453  psss  15694  isgrpid2  15884  f1omvdco2  16266  pgpfi  16418  frgpnabllem1  16665  gsumval3eu  16695  gsumzres  16702  gsumzcl2  16703  gsumzf1o  16705  gsumzresOLD  16706  gsumzclOLD  16707  gsumzf1oOLD  16708  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  gsumzmhm  16745  gsumzmhmOLD  16746  gsumzoppg  16755  gsumzoppgOLD  16756  ablfaclem3  16925  dvdsrtr  17082  dvdsrmul1  17083  unitgrp  17097  lspsolvlem  17568  domnmuln0  17715  gsummoncoe1  18114  pf1ind  18159  gsumfsum  18249  obslbs  18525  dmatscmcl  18769  scmatmulcl  18784  smatvscl  18790  mdetdiaglem  18864  cpmatinvcl  18982  mp2pm2mplem4  19074  cpmadugsumlemF  19141  eltg3  19227  tgidm  19245  neindisj  19381  tgrest  19423  restcld  19436  tgcn  19516  lmcnp  19568  iunconlem  19691  2ndcredom  19714  2ndc1stc  19715  1stcrest  19717  2ndcrest  19718  2ndcdisj  19720  nllyrest  19750  nllyidm  19753  ptpjpre1  19804  ptuni2  19809  ptbasin  19810  ptbasfi  19814  txbasval  19839  ptpjopn  19845  ptclsg  19848  dfac14lem  19850  xkoccn  19852  txcnp  19853  ptcnplem  19854  ptcnp  19855  txtube  19873  txcmplem1  19874  txcmplem2  19875  tx2ndc  19884  txkgen  19885  xkoco1cn  19890  xkoco2cn  19891  xkococnlem  19892  xkococn  19893  xkoinjcn  19920  qtoprest  19950  kqsat  19964  kqcldsat  19966  isfild  20091  fbunfip  20102  fgabs  20112  filcon  20116  fbasrn  20117  filufint  20153  elfm2  20181  elfm3  20183  fmfnfm  20191  hausflimi  20213  cnpflfi  20232  ptcmplem2  20285  tmdgsum2  20327  cldsubg  20341  divstgpopn  20350  ustfilxp  20447  bldisj  20633  xbln0  20649  blssps  20659  blss  20660  blssexps  20661  blssex  20662  blcls  20741  metcnp3  20775  icccmplem2  21060  cnheibor  21187  iscau4  21450  ovolshftlem2  21653  ovolicc2lem5  21664  dyadmax  21739  mbfi1fseqlem4  21857  mbfi1flimlem  21861  lhop1lem  22146  dvfsumrlim  22164  aalioulem3  22461  ulmcn  22525  radcnvlt1  22544  pilem2  22578  efopn  22764  cxpeq0  22784  cxpmul2z  22797  cxpcn3lem  22846  xrlimcnp  23023  vmappw  23115  fsumvma  23213  dchrptlem1  23264  lgsqr  23346  lgsdchrval  23347  2sqlem6  23369  2sqlem7  23370  pntlem3  23519  pntleml  23521  brbtwn  23875  brcgr  23876  axcontlem8  23947  cusgrafilem2  24153  redwlk  24281  4cycl4dv  24340  cusconngra  24349  usg2wlkeq  24381  usg2spthonot  24561  usg2spthonot0  24562  frg2woteq  24734  pjhthmo  25893  spansncvi  26243  nmcexi  26618  cnlnssadj  26672  leopmuli  26725  elpjrn  26782  mdsl0  26902  sumdmdii  27007  fmptcof2  27171  suppss3  27219  fpwrelmap  27225  lmxrge0  27567  erdszelem7  28278  sconpi1  28321  cvmsval  28348  cvmopnlem  28360  cvmfolem  28361  cvmliftmolem2  28364  cvmlift2lem10  28394  cvmlift2lem12  28396  cvmlift3lem5  28405  cvmlift3lem8  28408  prodmolem2  28641  prodmo  28642  zprod  28643  fprodf1o  28652  fprodss  28654  fprodcl2lem  28656  fprodmul  28664  fproddiv  28665  fprodconst  28682  fprodn0  28683  trpredrec  28895  wfr3g  28916  frr3g  28960  sltval2  28990  linethru  29377  finixpnum  29612  heicant  29624  voliunnfl  29633  volsupnfl  29634  itg2addnclem  29641  opnrebl2  29714  lfinpfin  29773  locfincmp  29774  neibastop2lem  29779  neibastop2  29780  unirep  29804  sdclem2  29836  istotbnd3  29868  ssbnd  29885  incssnn0  30245  eldioph4b  30347  diophren  30349  fphpdo  30353  rencldnfilem  30356  pellexlem5  30371  pell1234qrne0  30391  pell1234qrmulcl  30393  pell14qrgt0  30397  pell1234qrdich  30399  pell14qrdich  30407  pell1qrge1  30408  pell1qrgap  30412  pellfundre  30419  pellfundlb  30422  dvdsacongtr  30524  jm2.19lem4  30538  aomclem4  30607  hbtlem2  30677  hbtlem4  30679  hbtlem6  30682  ordpss  30938  ellcoellss  32109  bnj594  33049  bnj849  33062  bj-cbv3ta  33352  lshpdisj  33784  lsatn0  33796  lsat0cv  33830  cvrletrN  34070  cvrval4N  34210  lncvrelatN  34577  paddasslem14  34629  paddasslem15  34630  paddasslem16  34631  pmapjoin  34648  dihglblem2N  36091  dochvalr  36154
  Copyright terms: Public domain W3C validator