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

Theorem expimpd 586
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 420 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  disjiun  4092  euotd  4346  swopo  4403  wereu2  4469  oneqmini  4522  reusv3  4621  ralxfrd  4627  onmindif2  4682  poirr2  5146  sossfld  5199  elpreima  5725  suppss  5738  fmptco  5771  isofrlem  5921  frxp  6309  fnse  6316  tposfo2  6341  tz7.48-2  6538  omeulem1  6664  omeu  6667  nnaordex  6720  th3qlem1  6849  pssnn  7166  fodomfib  7223  dffi3  7271  supmo  7290  supnub  7300  cantnfle  7459  cantnflem1  7478  epfrs  7500  alephord2i  7791  cardinfima  7811  aceq3lem  7834  dfac2  7844  dfac12lem2  7857  axdc2lem  8161  ttukeylem6  8228  alephval2  8281  fpwwe2lem12  8350  fpwwe2lem13  8351  prlem934  8744  reclem4pr  8761  suplem1pr  8763  letr  9001  sup2  9797  uzind  10192  xrletr  10578  xltnegi  10632  xlemul1a  10697  ixxssixx  10759  difreicc  10856  flval3  11034  fsequb  11126  seqf1olem1  11174  expnegz  11226  shftlem  11653  rexuzre  11926  cau3lem  11928  caubnd2  11931  caubnd  11932  climrlim2  12111  climuni  12116  2clim  12136  o1co  12150  rlimno1  12217  climbdd  12235  caurcvg  12240  summolem2  12280  summo  12281  zsum  12282  fsumf1o  12287  fsumss  12289  fsumcl2lem  12295  fsumadd  12302  fsummulc2  12337  fsumconst  12343  fsumrelem  12356  prmpwdvds  13042  infpnlem1  13048  1arith  13065  vdwapun  13112  vdwlem11  13129  vdwnnlem2  13134  ramz  13163  ramcl  13167  prmlem0  13198  firest  13430  catpropd  13705  pltnle  14193  pltletr  14198  pospo  14200  psss  14416  isgrpid2  14611  pgpfi  15009  frgpnabllem1  15254  gsumval3eu  15283  gsumzres  15287  gsumzcl  15288  gsumzf1o  15289  gsumzaddlem  15296  gsumconst  15302  gsumzmhm  15303  gsumzoppg  15309  ablfaclem3  15415  dvdsrtr  15527  dvdsrmul1  15528  unitgrp  15542  lspsolvlem  15988  domnmuln0  16132  gsumfsum  16539  obslbs  16730  eltg3  16800  tgidm  16818  neindisj  16954  tgrest  16990  restcld  17003  tgcn  17082  lmcnp  17132  iunconlem  17253  2ndcredom  17276  2ndc1stc  17277  1stcrest  17279  2ndcrest  17280  2ndcdisj  17282  nllyrest  17312  nllyidm  17315  ptpjpre1  17366  ptuni2  17371  ptbasin  17372  ptbasfi  17376  txbasval  17401  ptpjopn  17406  ptclsg  17409  dfac14lem  17411  xkoccn  17413  txcnp  17414  ptcnplem  17415  ptcnp  17416  txtube  17434  txcmplem1  17435  txcmplem2  17436  tx2ndc  17445  txkgen  17446  xkoco1cn  17451  xkoco2cn  17452  xkococnlem  17453  xkococn  17454  xkoinjcn  17481  qtoprest  17508  kqsat  17522  kqcldsat  17524  isfild  17649  fbunfip  17660  fgabs  17670  filcon  17674  fbasrn  17675  filufint  17711  elfm2  17739  elfm3  17741  fmfnfm  17749  hausflimi  17771  cnpflfi  17790  ptcmplem2  17843  tmdgsum2  17875  cldsubg  17889  divstgpopn  17898  bldisj  18051  xbln0  18061  blss  18068  blssex  18069  blcls  18148  metcnp3  18182  icccmplem2  18425  cnheibor  18551  iscau4  18803  ovolshftlem2  18967  ovolicc2lem5  18978  dyadmax  19051  mbfi1fseqlem4  19171  mbfi1flimlem  19175  lhop1lem  19458  dvfsumrlim  19476  pf1ind  19536  aalioulem3  19812  ulmcn  19876  radcnvlt1  19895  pilem2  19929  efopn  20110  cxpeq0  20130  cxpmul2z  20143  cxpcn3lem  20192  xrlimcnp  20368  vmappw  20460  fsumvma  20558  dchrptlem1  20609  lgsqr  20691  lgsdchrval  20692  2sqlem6  20714  2sqlem7  20715  pntlem3  20864  pntleml  20866  pjhthmo  21989  spansncvi  22339  nmcexi  22714  cnlnssadj  22768  leopmuli  22821  elpjrn  22878  mdsl0  22998  sumdmdii  23103  fmptcof2  23277  lmxrge0  23493  ustfilxp  23518  erdszelem7  24132  sconpi1  24174  cvmsval  24201  cvmopnlem  24213  cvmfolem  24214  cvmliftmolem2  24217  cvmlift2lem10  24247  cvmlift2lem12  24249  cvmlift3lem5  24258  cvmlift3lem8  24261  zprod  24564  fprodf1o  24573  fprodss  24575  fprodcl2lem  24577  fprodmul  24585  fproddiv  24586  fprodconst  24603  fprodn0  24604  trpredrec  24799  wfr3g  24813  frr3g  24838  sltval2  24868  brbtwn  25086  brcgr  25087  axcontlem8  25158  linethru  25335  voliunnfl  25490  volsupnfl  25491  itg2addnclem  25492  opnrebl2  25560  lfinpfin  25627  locfincmp  25628  neibastop2lem  25633  neibastop2  25634  unirep  25673  sdclem2  25776  istotbnd3  25818  ssbnd  25835  incssnn0  26109  eldioph4b  26217  diophren  26219  fphpdo  26223  rencldnfilem  26226  pellexlem5  26241  pell1234qrne0  26261  pell1234qrmulcl  26263  pell14qrgt0  26267  pell1234qrdich  26269  pell14qrdich  26277  pell1qrge1  26278  pell1qrgap  26282  pellfundre  26289  pellfundlb  26292  dvdsacongtr  26394  jm2.19lem4  26408  aomclem4  26477  hbtlem2  26651  hbtlem4  26653  hbtlem6  26656  f1omvdco2  26714  ordpss  26977  redwlk  27725  4cycl4dv  27774  cusconngra  27783  bnj594  28689  bnj849  28702  lshpdisj  29229  lsatn0  29241  lsat0cv  29275  cvrletrN  29515  cvrval4N  29655  lncvrelatN  30022  paddasslem14  30074  paddasslem15  30075  paddasslem16  30076  pmapjoin  30093  dihglblem2N  31536  dochvalr  31599
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 177  df-an 360
  Copyright terms: Public domain W3C validator