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

Theorem expimpd 587
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 421 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  disjiun  4162  euotd  4417  swopo  4473  wereu2  4539  oneqmini  4592  reusv3  4690  ralxfrd  4696  onmindif2  4751  poirr2  5217  sossfld  5276  elpreima  5809  suppss  5822  fmptco  5860  isofrlem  6019  frxp  6415  fnse  6422  tposfo2  6461  tz7.48-2  6658  omeulem1  6784  omeu  6787  nnaordex  6840  th3qlem1  6969  pssnn  7286  fodomfib  7345  dffi3  7394  supmo  7413  supnub  7423  cantnfle  7582  cantnflem1  7601  epfrs  7623  alephord2i  7914  cardinfima  7934  aceq3lem  7957  dfac2  7967  dfac12lem2  7980  axdc2lem  8284  ttukeylem6  8350  alephval2  8403  fpwwe2lem12  8472  fpwwe2lem13  8473  prlem934  8866  reclem4pr  8883  suplem1pr  8885  letr  9123  sup2  9920  uzind  10317  xrletr  10704  xltnegi  10758  xlemul1a  10823  ixxssixx  10886  difreicc  10984  flval3  11177  fsequb  11269  seqf1olem1  11317  expnegz  11369  shftlem  11838  rexuzre  12111  cau3lem  12113  caubnd2  12116  caubnd  12117  climrlim2  12296  climuni  12301  2clim  12321  o1co  12335  rlimno1  12402  climbdd  12420  caurcvg  12425  summolem2  12465  summo  12466  zsum  12467  fsumf1o  12472  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumconst  12528  fsumrelem  12541  prmpwdvds  13227  infpnlem1  13233  1arith  13250  vdwapun  13297  vdwlem11  13314  vdwnnlem2  13319  ramz  13348  ramcl  13352  prmlem0  13383  firest  13615  catpropd  13890  pltnle  14378  pltletr  14383  pospo  14385  psss  14601  isgrpid2  14796  pgpfi  15194  frgpnabllem1  15439  gsumval3eu  15468  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  ablfaclem3  15600  dvdsrtr  15712  dvdsrmul1  15713  unitgrp  15727  lspsolvlem  16169  domnmuln0  16313  gsumfsum  16721  obslbs  16912  eltg3  16982  tgidm  17000  neindisj  17136  tgrest  17177  restcld  17190  tgcn  17270  lmcnp  17322  iunconlem  17443  2ndcredom  17466  2ndc1stc  17467  1stcrest  17469  2ndcrest  17470  2ndcdisj  17472  nllyrest  17502  nllyidm  17505  ptpjpre1  17556  ptuni2  17561  ptbasin  17562  ptbasfi  17566  txbasval  17591  ptpjopn  17597  ptclsg  17600  dfac14lem  17602  xkoccn  17604  txcnp  17605  ptcnplem  17606  ptcnp  17607  txtube  17625  txcmplem1  17626  txcmplem2  17627  tx2ndc  17636  txkgen  17637  xkoco1cn  17642  xkoco2cn  17643  xkococnlem  17644  xkococn  17645  xkoinjcn  17672  qtoprest  17702  kqsat  17716  kqcldsat  17718  isfild  17843  fbunfip  17854  fgabs  17864  filcon  17868  fbasrn  17869  filufint  17905  elfm2  17933  elfm3  17935  fmfnfm  17943  hausflimi  17965  cnpflfi  17984  ptcmplem2  18037  tmdgsum2  18079  cldsubg  18093  divstgpopn  18102  ustfilxp  18195  bldisj  18381  xbln0  18397  blssps  18407  blss  18408  blssexps  18409  blssex  18410  blcls  18489  metcnp3  18523  icccmplem2  18807  cnheibor  18933  iscau4  19185  ovolshftlem2  19359  ovolicc2lem5  19370  dyadmax  19443  mbfi1fseqlem4  19563  mbfi1flimlem  19567  lhop1lem  19850  dvfsumrlim  19868  pf1ind  19928  aalioulem3  20204  ulmcn  20268  radcnvlt1  20287  pilem2  20321  efopn  20502  cxpeq0  20522  cxpmul2z  20535  cxpcn3lem  20584  xrlimcnp  20760  vmappw  20852  fsumvma  20950  dchrptlem1  21001  lgsqr  21083  lgsdchrval  21084  2sqlem6  21106  2sqlem7  21107  pntlem3  21256  pntleml  21258  cusgrafilem2  21442  redwlk  21559  4cycl4dv  21607  cusconngra  21616  pjhthmo  22757  spansncvi  23107  nmcexi  23482  cnlnssadj  23536  leopmuli  23589  elpjrn  23646  mdsl0  23766  sumdmdii  23871  fmptcof2  24029  lmxrge0  24290  erdszelem7  24836  sconpi1  24879  cvmsval  24906  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem2  24922  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift3lem5  24963  cvmlift3lem8  24966  prodmolem2  25214  prodmo  25215  zprod  25216  fprodf1o  25225  fprodss  25227  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodconst  25255  fprodn0  25256  trpredrec  25455  wfr3g  25469  frr3g  25494  sltval2  25524  brbtwn  25742  brcgr  25743  axcontlem8  25814  linethru  25991  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  opnrebl2  26214  lfinpfin  26273  locfincmp  26274  neibastop2lem  26279  neibastop2  26280  unirep  26304  sdclem2  26336  istotbnd3  26370  ssbnd  26387  incssnn0  26655  eldioph4b  26762  diophren  26764  fphpdo  26768  rencldnfilem  26771  pellexlem5  26786  pell1234qrne0  26806  pell1234qrmulcl  26808  pell14qrgt0  26812  pell1234qrdich  26814  pell14qrdich  26822  pell1qrge1  26823  pell1qrgap  26827  pellfundre  26834  pellfundlb  26837  dvdsacongtr  26939  jm2.19lem4  26953  aomclem4  27022  hbtlem2  27196  hbtlem4  27198  hbtlem6  27201  f1omvdco2  27259  ordpss  27521  swrd0swrd  28009  usg2spthonot  28085  usg2spthonot0  28086  frg2woteq  28163  bnj594  28989  bnj849  29002  lshpdisj  29470  lsatn0  29482  lsat0cv  29516  cvrletrN  29756  cvrval4N  29896  lncvrelatN  30263  paddasslem14  30315  paddasslem15  30316  paddasslem16  30317  pmapjoin  30334  dihglblem2N  31777  dochvalr  31840
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 178  df-an 361
  Copyright terms: Public domain W3C validator