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  4277  reusv3  4495  ralxfrd  4501  euotd  4587  swopo  4646  wereu2  4712  oneqmini  4765  poirr2  5217  sossfld  5280  elpreima  5818  suppssOLD  5831  fmptco  5871  isofrlem  6026  onmindif2  6418  frxp  6677  fnse  6684  suppss  6714  tposfo2  6763  tz7.48-2  6889  omeulem1  7013  omeu  7016  nnaordex  7069  th3qlem1  7198  pssnn  7523  fodomfib  7583  dffi3  7673  supmo  7694  supnub  7704  cantnfle  7871  cantnflem1  7889  cantnfleOLD  7901  cantnflem1OLD  7912  epfrs  7943  alephord2i  8239  cardinfima  8259  aceq3lem  8282  dfac2  8292  dfac12lem2  8305  axdc2lem  8609  ttukeylem6  8675  alephval2  8728  fpwwe2lem12  8800  fpwwe2lem13  8801  prlem934  9194  reclem4pr  9211  suplem1pr  9213  letr  9460  sup2  10278  uzind  10725  xrletr  11124  xltnegi  11178  xlemul1a  11243  ixxssixx  11306  difreicc  11409  flval3  11655  fsequb  11789  seqf1olem1  11837  expnegz  11890  swrdsymbeq  12333  shftlem  12549  rexuzre  12832  cau3lem  12834  caubnd2  12837  caubnd  12838  climrlim2  13017  climuni  13022  2clim  13042  o1co  13056  rlimno1  13123  climbdd  13141  caurcvg  13146  summolem2  13185  summo  13186  zsum  13187  fsumf1o  13192  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  fsummulc2  13243  fsumconst  13249  fsumrelem  13262  prmpwdvds  13957  infpnlem1  13963  1arith  13980  vdwapun  14027  vdwlem11  14044  vdwnnlem2  14049  ramz  14078  ramcl  14082  prmlem0  14125  firest  14363  catpropd  14640  pltnle  15128  pltletr  15133  pospo  15135  psss  15376  isgrpid2  15565  f1omvdco2  15945  pgpfi  16095  frgpnabllem1  16342  gsumval3eu  16372  gsumzres  16379  gsumzcl2  16380  gsumzf1o  16382  gsumzresOLD  16383  gsumzclOLD  16384  gsumzf1oOLD  16385  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  ablfaclem3  16576  dvdsrtr  16732  dvdsrmul1  16733  unitgrp  16747  lspsolvlem  17200  domnmuln0  17347  pf1ind  17764  gsumfsum  17854  obslbs  18130  eltg3  18542  tgidm  18560  neindisj  18696  tgrest  18738  restcld  18751  tgcn  18831  lmcnp  18883  iunconlem  19006  2ndcredom  19029  2ndc1stc  19030  1stcrest  19032  2ndcrest  19033  2ndcdisj  19035  nllyrest  19065  nllyidm  19068  ptpjpre1  19119  ptuni2  19124  ptbasin  19125  ptbasfi  19129  txbasval  19154  ptpjopn  19160  ptclsg  19163  dfac14lem  19165  xkoccn  19167  txcnp  19168  ptcnplem  19169  ptcnp  19170  txtube  19188  txcmplem1  19189  txcmplem2  19190  tx2ndc  19199  txkgen  19200  xkoco1cn  19205  xkoco2cn  19206  xkococnlem  19207  xkococn  19208  xkoinjcn  19235  qtoprest  19265  kqsat  19279  kqcldsat  19281  isfild  19406  fbunfip  19417  fgabs  19427  filcon  19431  fbasrn  19432  filufint  19468  elfm2  19496  elfm3  19498  fmfnfm  19506  hausflimi  19528  cnpflfi  19547  ptcmplem2  19600  tmdgsum2  19642  cldsubg  19656  divstgpopn  19665  ustfilxp  19762  bldisj  19948  xbln0  19964  blssps  19974  blss  19975  blssexps  19976  blssex  19977  blcls  20056  metcnp3  20090  icccmplem2  20375  cnheibor  20502  iscau4  20765  ovolshftlem2  20968  ovolicc2lem5  20979  dyadmax  21053  mbfi1fseqlem4  21171  mbfi1flimlem  21175  lhop1lem  21460  dvfsumrlim  21478  aalioulem3  21775  ulmcn  21839  radcnvlt1  21858  pilem2  21892  efopn  22078  cxpeq0  22098  cxpmul2z  22111  cxpcn3lem  22160  xrlimcnp  22337  vmappw  22429  fsumvma  22527  dchrptlem1  22578  lgsqr  22660  lgsdchrval  22661  2sqlem6  22683  2sqlem7  22684  pntlem3  22833  pntleml  22835  brbtwn  23096  brcgr  23097  axcontlem8  23168  cusgrafilem2  23339  redwlk  23456  4cycl4dv  23504  cusconngra  23513  pjhthmo  24656  spansncvi  25006  nmcexi  25381  cnlnssadj  25435  leopmuli  25488  elpjrn  25545  mdsl0  25665  sumdmdii  25770  fmptcof2  25930  suppss3  25978  fpwrelmap  25984  lmxrge0  26334  erdszelem7  27037  sconpi1  27080  cvmsval  27107  cvmopnlem  27119  cvmfolem  27120  cvmliftmolem2  27123  cvmlift2lem10  27153  cvmlift2lem12  27155  cvmlift3lem5  27164  cvmlift3lem8  27167  prodmolem2  27399  prodmo  27400  zprod  27401  fprodf1o  27410  fprodss  27412  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodconst  27440  fprodn0  27441  trpredrec  27653  wfr3g  27674  frr3g  27718  sltval2  27748  linethru  28135  finixpnum  28367  heicant  28379  voliunnfl  28388  volsupnfl  28389  itg2addnclem  28396  opnrebl2  28469  lfinpfin  28528  locfincmp  28529  neibastop2lem  28534  neibastop2  28535  unirep  28559  sdclem2  28591  istotbnd3  28623  ssbnd  28640  incssnn0  29000  eldioph4b  29103  diophren  29105  fphpdo  29109  rencldnfilem  29112  pellexlem5  29127  pell1234qrne0  29147  pell1234qrmulcl  29149  pell14qrgt0  29153  pell1234qrdich  29155  pell14qrdich  29163  pell1qrge1  29164  pell1qrgap  29168  pellfundre  29175  pellfundlb  29178  dvdsacongtr  29280  jm2.19lem4  29294  aomclem4  29363  hbtlem2  29433  hbtlem4  29435  hbtlem6  29438  ordpss  29660  usg2wlkeq  30242  usg2spthonot  30360  usg2spthonot0  30361  frg2woteq  30606  mdetdiaglem  30824  ellcoellss  30858  bnj594  31792  bnj849  31805  bj-cbv3ta  32063  lshpdisj  32472  lsatn0  32484  lsat0cv  32518  cvrletrN  32758  cvrval4N  32898  lncvrelatN  33265  paddasslem14  33317  paddasslem15  33318  paddasslem16  33319  pmapjoin  33336  dihglblem2N  34779  dochvalr  34842
  Copyright terms: Public domain W3C validator