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  4013  euotd  4267  swopo  4324  wereu2  4390  oneqmini  4443  reusv3  4542  ralxfrd  4548  onmindif2  4603  poirr2  5067  sossfld  5120  elpreima  5645  suppss  5658  fmptco  5691  isofrlem  5837  frxp  6225  fnse  6232  tposfo2  6257  tz7.48-2  6454  omeulem1  6580  omeu  6583  nnaordex  6636  th3qlem1  6764  pssnn  7081  fodomfib  7136  dffi3  7184  supmo  7203  supnub  7213  cantnfle  7372  cantnflem1  7391  epfrs  7413  alephord2i  7704  cardinfima  7724  aceq3lem  7747  dfac2  7757  dfac12lem2  7770  axdc2lem  8074  ttukeylem6  8141  alephval2  8194  fpwwe2lem12  8263  fpwwe2lem13  8264  prlem934  8657  reclem4pr  8674  suplem1pr  8676  letr  8914  sup2  9710  uzind  10103  xrletr  10489  xltnegi  10543  xlemul1a  10608  ixxssixx  10670  difreicc  10767  flval3  10945  fsequb  11037  seqf1olem1  11085  expnegz  11136  shftlem  11563  rexuzre  11836  cau3lem  11838  caubnd2  11841  caubnd  11842  climrlim2  12021  climuni  12026  2clim  12046  o1co  12060  rlimno1  12127  caurcvg  12149  summolem2  12189  summo  12190  zsum  12191  fsumf1o  12196  fsumss  12198  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumconst  12252  fsumrelem  12265  prmpwdvds  12951  infpnlem1  12957  1arith  12974  vdwapun  13021  vdwlem11  13038  vdwnnlem2  13043  ramz  13072  ramcl  13076  prmlem0  13107  firest  13337  catpropd  13612  pltnle  14100  pltletr  14105  pospo  14107  psss  14323  isgrpid2  14518  pgpfi  14916  frgpnabllem1  15161  gsumval3eu  15190  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  ablfaclem3  15322  dvdsrtr  15434  dvdsrmul1  15435  unitgrp  15449  lspsolvlem  15895  domnmuln0  16039  gsumfsum  16439  obslbs  16630  eltg3  16700  tgidm  16718  neindisj  16854  tgrest  16890  restcld  16903  tgcn  16982  lmcnp  17032  iunconlem  17153  2ndcredom  17176  2ndc1stc  17177  1stcrest  17179  2ndcrest  17180  2ndcdisj  17182  nllyrest  17212  nllyidm  17215  ptpjpre1  17266  ptuni2  17271  ptbasin  17272  ptbasfi  17276  txbasval  17301  ptpjopn  17306  ptclsg  17309  dfac14lem  17311  xkoccn  17313  txcnp  17314  ptcnplem  17315  ptcnp  17316  txtube  17334  txcmplem1  17335  txcmplem2  17336  tx2ndc  17345  txkgen  17346  xkoco1cn  17351  xkoco2cn  17352  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  qtoprest  17408  kqsat  17422  kqcldsat  17424  isfild  17553  fbunfip  17564  fgabs  17574  filcon  17578  fbasrn  17579  filufint  17615  elfm2  17643  elfm3  17645  fmfnfm  17653  hausflimi  17675  cnpflfi  17694  ptcmplem2  17747  tmdgsum2  17779  cldsubg  17793  divstgpopn  17802  bldisj  17955  xbln0  17965  blss  17972  blssex  17973  blcls  18052  metcnp3  18086  icccmplem2  18328  cnheibor  18453  iscau4  18705  ovolshftlem2  18869  ovolicc2lem5  18880  dyadmax  18953  mbfi1fseqlem4  19073  mbfi1flimlem  19077  lhop1lem  19360  dvfsumrlim  19378  pf1ind  19438  aalioulem3  19714  ulmcn  19776  radcnvlt1  19794  pilem2  19828  efopn  20005  cxpeq0  20025  cxpmul2z  20038  cxpcn3lem  20087  xrlimcnp  20263  vmappw  20354  fsumvma  20452  dchrptlem1  20503  lgsqr  20585  lgsdchrval  20586  2sqlem6  20608  2sqlem7  20609  pntlem3  20758  pntleml  20760  pjhthmo  21881  spansncvi  22231  nmcexi  22606  cnlnssadj  22660  leopmuli  22713  elpjrn  22770  mdsl0  22890  sumdmdii  22995  fmptcof2  23229  lmxrge0  23375  erdszelem7  23728  sconpi1  23770  cvmsval  23797  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem2  23813  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift3lem5  23854  cvmlift3lem8  23857  trpredrec  24241  wfr3g  24255  frr3g  24280  sltval2  24310  brbtwn  24527  brcgr  24528  axcontlem8  24599  linethru  24776  repcpwti  25161  exopcopn  25572  opnrebl2  26236  lfinpfin  26303  locfincmp  26304  neibastop2lem  26309  neibastop2  26310  unirep  26349  sdclem2  26452  istotbnd3  26495  ssbnd  26512  incssnn0  26786  eldioph4b  26894  diophren  26896  fphpdo  26900  rencldnfilem  26903  pellexlem5  26918  pell1234qrne0  26938  pell1234qrmulcl  26940  pell14qrgt0  26944  pell1234qrdich  26946  pell14qrdich  26954  pell1qrge1  26955  pell1qrgap  26959  pellfundre  26966  pellfundlb  26969  dvdsacongtr  27071  jm2.19lem4  27085  aomclem4  27154  hbtlem2  27328  hbtlem4  27330  hbtlem6  27333  f1omvdco2  27391  ordpss  27654  bnj594  28944  bnj849  28957  lshpdisj  29177  lsatn0  29189  lsat0cv  29223  cvrletrN  29463  cvrval4N  29603  lncvrelatN  29970  paddasslem14  30022  paddasslem15  30023  paddasslem16  30024  pmapjoin  30041  dihglblem2N  31484  dochvalr  31547
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