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

Theorem expimpd 606
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 432 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ornld  906  ralrimdva  2850  disjiun  4417  reusv3  4633  ralxfrd  4636  euotd  4722  swopo  4785  wereu2  4851  poirr2  5244  sossfld  5303  oneqmini  5493  elpreima  6017  fmptco  6071  isofrlem  6246  onmindif2  6653  frxp  6917  fnse  6924  suppss  6956  tposfo2  7004  wfr3g  7042  tz7.48-2  7167  omeulem1  7291  omeu  7294  nnaordex  7347  pssnn  7796  fodomfib  7857  dffi3  7951  supmo  7972  supnub  7982  infglb  8012  infnlb  8014  cantnfle  8175  cantnflem1  8193  epfrs  8214  alephord2i  8506  cardinfima  8526  aceq3lem  8549  dfac2  8559  dfac12lem2  8572  axdc2lem  8876  ttukeylem6  8942  alephval2  8995  fpwwe2lem12  9065  fpwwe2lem13  9066  prlem934  9457  reclem4pr  9474  suplem1pr  9476  letr  9726  sup2  10565  uzind  11027  xrletr  11455  xltnegi  11509  xlemul1a  11574  ixxssixx  11649  difreicc  11762  flval3  12047  fsequb  12185  seqf1olem1  12249  expnegz  12303  relexprelg  13080  shftlem  13110  rexuzre  13394  cau3lem  13396  caubnd2  13399  caubnd  13400  climrlim2  13589  climuni  13594  2clim  13614  o1co  13628  rlimno1  13695  climbdd  13713  caurcvg  13720  caurcvgOLD  13721  summolem2  13760  summo  13761  zsum  13762  fsumf1o  13767  fsumss  13769  fsumcl2lem  13775  fsumadd  13783  fsummulc2  13823  fsumconst  13829  fsumrelem  13845  prodmolem2  13967  prodmo  13968  zprod  13969  fprodf1o  13978  fprodss  13980  fprodcl2lem  13982  fprodmul  13992  fproddiv  13993  fprodconst  14010  fprodn0  14011  coprmproddvdslem  14641  prmpwdvds  14802  infpnlem1  14808  1arith  14825  vdwapun  14878  vdwlem11  14895  vdwnnlem2  14900  ramz  14937  ramcl  14941  prmlem0  15031  firest  15281  catpropd  15556  initoid  15842  termoid  15843  initoeu2lem1  15851  pltnle  16154  pltletr  16159  pospo  16161  psss  16402  isgrpid2  16644  f1omvdco2  17031  pgpfi  17183  frgpnabllem1  17435  gsumval3eu  17464  gsumzres  17469  gsumzcl2  17470  gsumzf1o  17472  gsumzaddlem  17480  gsumconst  17493  gsumzmhm  17496  gsumzoppg  17503  ablfaclem3  17646  dvdsrtr  17806  dvdsrmul1  17807  unitgrp  17821  lspsolvlem  18291  domnmuln0  18448  gsummoncoe1  18824  pf1ind  18869  gsumfsum  18960  obslbs  19215  dmatscmcl  19450  scmatmulcl  19465  smatvscl  19471  mdetdiaglem  19545  cpmatinvcl  19663  mp2pm2mplem4  19755  cpmadugsumlemF  19822  eltg3  19899  tgidm  19918  neindisj  20055  tgrest  20097  restcld  20110  tgcn  20190  lmcnp  20242  iunconlem  20364  2ndcredom  20387  2ndc1stc  20388  1stcrest  20390  2ndcrest  20391  2ndcdisj  20393  nllyrest  20423  nllyidm  20426  lfinpfin  20461  locfincmp  20463  ptpjpre1  20508  ptuni2  20513  ptbasin  20514  ptbasfi  20518  txbasval  20543  ptpjopn  20549  ptclsg  20552  dfac14lem  20554  xkoccn  20556  txcnp  20557  ptcnplem  20558  ptcnp  20559  txtube  20577  txcmplem1  20578  txcmplem2  20579  tx2ndc  20588  txkgen  20589  xkoco1cn  20594  xkoco2cn  20595  xkococnlem  20596  xkococn  20597  xkoinjcn  20624  qtoprest  20654  kqsat  20668  kqcldsat  20670  isfild  20795  fbunfip  20806  fgabs  20816  filcon  20820  fbasrn  20821  filufint  20857  elfm2  20885  elfm3  20887  fmfnfm  20895  hausflimi  20917  cnpflfi  20936  ptcmplem2  20990  tmdgsum2  21033  cldsubg  21047  qustgpopn  21056  ustfilxp  21149  bldisj  21335  xbln0  21351  blssps  21361  blss  21362  blssexps  21363  blssex  21364  blcls  21443  metcnp3  21477  icccmplem2  21743  cnheibor  21870  iscau4  22133  ovolshftlem2  22332  ovolicc2lem5  22343  dyadmax  22424  mbfi1fseqlem4  22544  mbfi1flimlem  22548  lhop1lem  22833  dvfsumrlim  22851  aalioulem3  23146  ulmcn  23210  radcnvlt1  23229  pilem2  23263  pilem2OLD  23264  efopn  23459  cxpeq0  23479  cxpmul2z  23492  cxpcn3lem  23543  xrlimcnp  23750  vmappw  23897  fsumvma  23995  dchrptlem1  24046  lgsqr  24128  lgsdchrval  24129  2sqlem6  24151  2sqlem7  24152  pntlem3  24301  pntleml  24303  brbtwn  24766  brcgr  24767  axcontlem8  24838  cusgrafilem2  25044  redwlk  25172  4cycl4dv  25231  cusconngra  25240  usg2wlkeq  25272  usg2spthonot  25452  usg2spthonot0  25453  frg2woteq  25624  pjhthmo  26781  spansncvi  27131  nmcexi  27505  cnlnssadj  27559  leopmuli  27612  elpjrn  27669  mdsl0  27789  sumdmdii  27894  fmptcof2  28090  suppss3  28146  lmxrge0  28588  bnj594  29502  bnj849  29515  erdszelem7  29699  sconpi1  29741  cvmsval  29768  cvmopnlem  29780  cvmfolem  29781  cvmliftmolem2  29784  cvmlift2lem10  29814  cvmlift2lem12  29816  cvmlift3lem5  29825  cvmlift3lem8  29828  trpredrec  30257  frr3g  30291  sltval2  30321  linethru  30696  opnrebl2  30753  neibastop2lem  30792  neibastop2  30793  bj-cbv3ta  31041  phpreu  31623  finixpnum  31624  ptrecube  31634  poimirlem26  31660  poimirlem27  31661  poimirlem31  31665  poimir  31667  heicant  31669  voliunnfl  31678  volsupnfl  31679  itg2addnclem  31687  unirep  31733  sdclem2  31765  istotbnd3  31797  ssbnd  31814  lshpdisj  32252  lsatn0  32264  lsat0cv  32298  cvrletrN  32538  cvrval4N  32678  lncvrelatN  33045  paddasslem14  33097  paddasslem15  33098  paddasslem16  33099  pmapjoin  33116  dihglblem2N  34561  dochvalr  34624  incssnn0  35252  eldioph4b  35353  diophren  35355  fphpdo  35359  rencldnfilem  35362  pellexlem5  35377  pell1234qrne0  35397  pell1234qrmulcl  35399  pell14qrgt0  35403  pell1234qrdich  35405  pell14qrdich  35413  pell1qrge1  35414  pell1qrgap  35418  pellfundre  35425  pellfundlb  35428  dvdsacongtr  35530  jm2.19lem4  35543  aomclem4  35611  hbtlem2  35679  hbtlem4  35681  hbtlem6  35684  ordpss  36431  opoeALTV  38192  opeoALTV  38193  gboage9  38245  nzerooringczr  38822  ellcoellss  38978  nn0sumshdiglem1  39183
  Copyright terms: Public domain W3C validator