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:  disjiun  4391  reusv3  4609  ralxfrd  4615  euotd  4701  swopo  4760  wereu2  4826  oneqmini  4879  poirr2  5331  sossfld  5394  elpreima  5933  suppssOLD  5946  fmptco  5986  isofrlem  6141  onmindif2  6534  frxp  6793  fnse  6800  suppss  6830  tposfo2  6879  tz7.48-2  7008  omeulem1  7132  omeu  7135  nnaordex  7188  th3qlem1  7317  pssnn  7643  fodomfib  7703  dffi3  7793  supmo  7814  supnub  7824  cantnfle  7991  cantnflem1  8009  cantnfleOLD  8021  cantnflem1OLD  8032  epfrs  8063  alephord2i  8359  cardinfima  8379  aceq3lem  8402  dfac2  8412  dfac12lem2  8425  axdc2lem  8729  ttukeylem6  8795  alephval2  8848  fpwwe2lem12  8920  fpwwe2lem13  8921  prlem934  9314  reclem4pr  9331  suplem1pr  9333  letr  9580  sup2  10398  uzind  10845  xrletr  11244  xltnegi  11298  xlemul1a  11363  ixxssixx  11426  difreicc  11535  flval3  11781  fsequb  11915  seqf1olem1  11963  expnegz  12016  swrdsymbeq  12460  shftlem  12676  rexuzre  12959  cau3lem  12961  caubnd2  12964  caubnd  12965  climrlim2  13144  climuni  13149  2clim  13169  o1co  13183  rlimno1  13250  climbdd  13268  caurcvg  13273  summolem2  13312  summo  13313  zsum  13314  fsumf1o  13319  fsumss  13321  fsumcl2lem  13327  fsumadd  13334  fsummulc2  13370  fsumconst  13376  fsumrelem  13389  prmpwdvds  14084  infpnlem1  14090  1arith  14107  vdwapun  14154  vdwlem11  14171  vdwnnlem2  14176  ramz  14205  ramcl  14209  prmlem0  14252  firest  14491  catpropd  14768  pltnle  15256  pltletr  15261  pospo  15263  psss  15504  isgrpid2  15694  f1omvdco2  16074  pgpfi  16226  frgpnabllem1  16473  gsumval3eu  16503  gsumzres  16510  gsumzcl2  16511  gsumzf1o  16513  gsumzresOLD  16514  gsumzclOLD  16515  gsumzf1oOLD  16516  gsumzaddlem  16530  gsumzaddlemOLD  16532  gsumconst  16550  gsumzmhm  16553  gsumzmhmOLD  16554  gsumzoppg  16563  gsumzoppgOLD  16564  ablfaclem3  16711  dvdsrtr  16868  dvdsrmul1  16869  unitgrp  16883  lspsolvlem  17347  domnmuln0  17494  pf1ind  17915  gsumfsum  18005  obslbs  18281  mdetdiaglem  18537  eltg3  18700  tgidm  18718  neindisj  18854  tgrest  18896  restcld  18909  tgcn  18989  lmcnp  19041  iunconlem  19164  2ndcredom  19187  2ndc1stc  19188  1stcrest  19190  2ndcrest  19191  2ndcdisj  19193  nllyrest  19223  nllyidm  19226  ptpjpre1  19277  ptuni2  19282  ptbasin  19283  ptbasfi  19287  txbasval  19312  ptpjopn  19318  ptclsg  19321  dfac14lem  19323  xkoccn  19325  txcnp  19326  ptcnplem  19327  ptcnp  19328  txtube  19346  txcmplem1  19347  txcmplem2  19348  tx2ndc  19357  txkgen  19358  xkoco1cn  19363  xkoco2cn  19364  xkococnlem  19365  xkococn  19366  xkoinjcn  19393  qtoprest  19423  kqsat  19437  kqcldsat  19439  isfild  19564  fbunfip  19575  fgabs  19585  filcon  19589  fbasrn  19590  filufint  19626  elfm2  19654  elfm3  19656  fmfnfm  19664  hausflimi  19686  cnpflfi  19705  ptcmplem2  19758  tmdgsum2  19800  cldsubg  19814  divstgpopn  19823  ustfilxp  19920  bldisj  20106  xbln0  20122  blssps  20132  blss  20133  blssexps  20134  blssex  20135  blcls  20214  metcnp3  20248  icccmplem2  20533  cnheibor  20660  iscau4  20923  ovolshftlem2  21126  ovolicc2lem5  21137  dyadmax  21212  mbfi1fseqlem4  21330  mbfi1flimlem  21334  lhop1lem  21619  dvfsumrlim  21637  aalioulem3  21934  ulmcn  21998  radcnvlt1  22017  pilem2  22051  efopn  22237  cxpeq0  22257  cxpmul2z  22270  cxpcn3lem  22319  xrlimcnp  22496  vmappw  22588  fsumvma  22686  dchrptlem1  22737  lgsqr  22819  lgsdchrval  22820  2sqlem6  22842  2sqlem7  22843  pntlem3  22992  pntleml  22994  brbtwn  23298  brcgr  23299  axcontlem8  23370  cusgrafilem2  23541  redwlk  23658  4cycl4dv  23706  cusconngra  23715  pjhthmo  24858  spansncvi  25208  nmcexi  25583  cnlnssadj  25637  leopmuli  25690  elpjrn  25747  mdsl0  25867  sumdmdii  25972  fmptcof2  26131  suppss3  26179  fpwrelmap  26185  lmxrge0  26528  erdszelem7  27230  sconpi1  27273  cvmsval  27300  cvmopnlem  27312  cvmfolem  27313  cvmliftmolem2  27316  cvmlift2lem10  27346  cvmlift2lem12  27348  cvmlift3lem5  27357  cvmlift3lem8  27360  prodmolem2  27593  prodmo  27594  zprod  27595  fprodf1o  27604  fprodss  27606  fprodcl2lem  27608  fprodmul  27616  fproddiv  27617  fprodconst  27634  fprodn0  27635  trpredrec  27847  wfr3g  27868  frr3g  27912  sltval2  27942  linethru  28329  finixpnum  28563  heicant  28575  voliunnfl  28584  volsupnfl  28585  itg2addnclem  28592  opnrebl2  28665  lfinpfin  28724  locfincmp  28725  neibastop2lem  28730  neibastop2  28731  unirep  28755  sdclem2  28787  istotbnd3  28819  ssbnd  28836  incssnn0  29196  eldioph4b  29299  diophren  29301  fphpdo  29305  rencldnfilem  29308  pellexlem5  29323  pell1234qrne0  29343  pell1234qrmulcl  29345  pell14qrgt0  29349  pell1234qrdich  29351  pell14qrdich  29359  pell1qrge1  29360  pell1qrgap  29364  pellfundre  29371  pellfundlb  29374  dvdsacongtr  29476  jm2.19lem4  29490  aomclem4  29559  hbtlem2  29629  hbtlem4  29631  hbtlem6  29634  ordpss  29856  usg2wlkeq  30438  usg2spthonot  30556  usg2spthonot0  30557  frg2woteq  30802  gsummoncoe1  30997  scmatscmid  31024  ellcoellss  31102  cpmatinvcl  31207  mp2pm2mplem4  31297  cpmadugsumlemF  31363  bnj594  32238  bnj849  32251  bj-cbv3ta  32539  lshpdisj  32971  lsatn0  32983  lsat0cv  33017  cvrletrN  33257  cvrval4N  33397  lncvrelatN  33764  paddasslem14  33816  paddasslem15  33817  paddasslem16  33818  pmapjoin  33835  dihglblem2N  35278  dochvalr  35341
  Copyright terms: Public domain W3C validator