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

Theorem expimpd 612
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 440 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 437 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ornld  914  ralrimdva  2818  disjiun  4407  reusv3  4625  ralxfrd  4628  euotd  4716  swopo  4784  wereu2  4850  poirr2  5243  sossfld  5302  oneqmini  5493  elpreima  6025  fmptco  6080  isofrlem  6256  onmindif2  6666  frxp  6933  fnse  6940  suppss  6972  tposfo2  7022  wfr3g  7060  tz7.48-2  7185  omeulem1  7309  omeu  7312  nnaordex  7365  pssnn  7816  fodomfib  7877  dffi3  7971  supmo  7992  supnub  8002  infglb  8032  infnlb  8034  infmo  8037  cantnfle  8202  cantnflem1  8220  epfrs  8241  alephord2i  8534  cardinfima  8554  aceq3lem  8577  dfac2  8587  dfac12lem2  8600  axdc2lem  8904  ttukeylem6  8970  alephval2  9023  fpwwe2lem12  9092  fpwwe2lem13  9093  prlem934  9484  reclem4pr  9501  suplem1pr  9503  letr  9753  sup2  10593  uzind  11056  xrletr  11484  xltnegi  11538  xlemul1a  11603  ixxssixx  11678  difreicc  11793  flval3  12082  fsequb  12220  seqf1olem1  12284  expnegz  12338  hash2prd  12667  relexprelg  13150  shftlem  13180  rexuzre  13464  cau3lem  13466  caubnd2  13469  caubnd  13470  climrlim2  13660  climuni  13665  2clim  13685  o1co  13699  rlimno1  13766  climbdd  13784  caurcvg  13791  caurcvgOLD  13792  summolem2  13831  summo  13832  zsum  13833  fsumf1o  13838  fsumss  13840  fsumcl2lem  13846  fsumadd  13854  fsummulc2  13894  fsumconst  13900  fsumrelem  13916  prodmolem2  14038  prodmo  14039  zprod  14040  fprodf1o  14049  fprodss  14051  fprodcl2lem  14053  fprodmul  14063  fproddiv  14064  fprodconst  14081  fprodn0  14082  coprmproddvdslem  14728  prmpwdvds  14897  infpnlem1  14903  1arith  14920  vdwapun  14973  vdwlem11  14990  vdwnnlem2  14995  ramz  15032  ramcl  15036  prmlem0  15126  firest  15380  catpropd  15663  initoid  15949  termoid  15950  initoeu2lem1  15958  pltnle  16261  pltletr  16266  pospo  16268  psss  16509  isgrpid2  16751  f1omvdco2  17138  pgpfi  17306  frgpnabllem1  17558  gsumval3eu  17587  gsumzres  17592  gsumzcl2  17593  gsumzf1o  17595  gsumzaddlem  17603  gsumconst  17616  gsumzmhm  17619  gsumzoppg  17626  ablfaclem3  17769  dvdsrtr  17929  dvdsrmul1  17930  unitgrp  17944  lspsolvlem  18414  domnmuln0  18571  gsummoncoe1  18947  pf1ind  18992  gsumfsum  19083  obslbs  19342  dmatscmcl  19577  scmatmulcl  19592  smatvscl  19598  mdetdiaglem  19672  cpmatinvcl  19790  mp2pm2mplem4  19882  cpmadugsumlemF  19949  eltg3  20026  tgidm  20045  neindisj  20182  tgrest  20224  restcld  20237  tgcn  20317  lmcnp  20369  iunconlem  20491  2ndcredom  20514  2ndc1stc  20515  1stcrest  20517  2ndcrest  20518  2ndcdisj  20520  nllyrest  20550  nllyidm  20553  lfinpfin  20588  locfincmp  20590  ptpjpre1  20635  ptuni2  20640  ptbasin  20641  ptbasfi  20645  txbasval  20670  ptpjopn  20676  ptclsg  20679  dfac14lem  20681  xkoccn  20683  txcnp  20684  ptcnplem  20685  ptcnp  20686  txtube  20704  txcmplem1  20705  txcmplem2  20706  tx2ndc  20715  txkgen  20716  xkoco1cn  20721  xkoco2cn  20722  xkococnlem  20723  xkococn  20724  xkoinjcn  20751  qtoprest  20781  kqsat  20795  kqcldsat  20797  isfild  20922  fbunfip  20933  fgabs  20943  filcon  20947  fbasrn  20948  filufint  20984  elfm2  21012  elfm3  21014  fmfnfm  21022  hausflimi  21044  cnpflfi  21063  ptcmplem2  21117  tmdgsum2  21160  cldsubg  21174  qustgpopn  21183  ustfilxp  21276  bldisj  21462  xbln0  21478  blssps  21488  blss  21489  blssexps  21490  blssex  21491  blcls  21570  metcnp3  21604  icccmplem2  21890  cnheibor  22032  iscau4  22298  ovolshftlem2  22512  ovolicc2lem5  22524  dyadmax  22605  mbfi1fseqlem4  22725  mbfi1flimlem  22729  lhop1lem  23014  dvfsumrlim  23032  aalioulem3  23339  ulmcn  23403  radcnvlt1  23422  pilem2  23456  pilem2OLD  23457  efopn  23652  cxpeq0  23672  cxpmul2z  23685  cxpcn3lem  23736  xrlimcnp  23943  vmappw  24092  fsumvma  24190  dchrptlem1  24241  lgsqr  24323  lgsdchrval  24324  2sqlem6  24346  2sqlem7  24347  pntlem3  24496  pntleml  24498  brbtwn  24978  brcgr  24979  axcontlem8  25050  cusgrafilem2  25257  redwlk  25385  4cycl4dv  25444  cusconngra  25453  usg2wlkeq  25485  usg2spthonot  25665  usg2spthonot0  25666  frg2woteq  25837  pjhthmo  27004  spansncvi  27354  nmcexi  27728  cnlnssadj  27782  leopmuli  27835  elpjrn  27892  mdsl0  28012  sumdmdii  28117  fmptcof2  28308  suppss3  28361  lmxrge0  28807  bnj594  29772  bnj849  29785  erdszelem7  29969  sconpi1  30011  cvmsval  30038  cvmopnlem  30050  cvmfolem  30051  cvmliftmolem2  30054  cvmlift2lem10  30084  cvmlift2lem12  30086  cvmlift3lem5  30095  cvmlift3lem8  30098  trpredrec  30528  frr3g  30562  sltval2  30592  linethru  30969  opnrebl2  31026  neibastop2lem  31065  neibastop2  31066  bj-ssbequ1  31302  bj-cbv3ta  31356  phpreu  31974  finixpnum  31975  ptrecube  31985  poimirlem26  32011  poimirlem27  32012  poimirlem31  32016  poimir  32018  heicant  32020  voliunnfl  32029  volsupnfl  32030  itg2addnclem  32038  unirep  32084  sdclem2  32116  istotbnd3  32148  ssbnd  32165  lshpdisj  32598  lsatn0  32610  lsat0cv  32644  cvrletrN  32884  cvrval4N  33024  lncvrelatN  33391  paddasslem14  33443  paddasslem15  33444  paddasslem16  33445  pmapjoin  33462  dihglblem2N  34907  dochvalr  34970  incssnn0  35598  eldioph4b  35699  diophren  35701  fphpdo  35705  rencldnfilem  35708  pellexlem5  35722  pell1234qrne0  35744  pell1234qrmulcl  35746  pell14qrgt0  35750  pell1234qrdich  35752  pell14qrdich  35760  pell1qrge1  35761  pell1qrgap  35765  pellfundre  35774  pellfundlb  35777  dvdsacongtr  35879  jm2.19lem4  35892  aomclem4  35960  hbtlem2  36028  hbtlem4  36030  hbtlem6  36033  clcnvlem  36275  ordpss  36848  opoeALTV  38850  opeoALTV  38851  gboage9  38903  nbumgrvtx  39464  cusgrfilem2  39567  uspgrloopnb0  39606  wlkOnwlk1l  39713  red1wlk  39717  upgrwlkdvdelem  39768  uspgrn2crct  39826  nzerooringczr  40347  ellcoellss  40501  nn0sumshdiglem1  40705
  Copyright terms: Public domain W3C validator