Theorem expimpd 629

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

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 447	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  ornld  940  ralrimdva  2969  disjiun  4640  reusv3  4876  ralxfrdOLD  4880  euotd  4975  swopo  5045  wereu2  5111  poirr2  5520  sossfld  5580  oneqmini  5776  suctr  5808  elpreima  6337  fmptco  6396  isofrlem  6590  onmindif2  7012  frxp  7287  fnse  7294  suppss  7325  tposfo2  7375  wfr3g  7413  tz7.48-2  7537  omeulem1  7662  omeu  7665  nnaordex  7718  pssnn  8178  fodomfib  8240  dffi3  8337  supmo  8358  supnub  8368  infglb  8396  infnlb  8398  infmo  8401  cantnfle  8568  cantnflem1  8586  epfrs  8607  alephord2i  8900  cardinfima  8920  aceq3lem  8943  dfac2  8953  dfac12lem2  8966  axdc2lem  9270  ttukeylem6  9336  alephval2  9394  fpwwe2lem12  9463  fpwwe2lem13  9464  prlem934  9855  reclem4pr  9872  suplem1pr  9874  letr  10131  sup2  10979  uzind  11469  ledivge1le  11901  xrletr  11989  xltnegi  12047  xlemul1a  12118  ixxssixx  12189  difreicc  12304  flval3  12616  fsequb  12774  seqf1olem1  12840  expnegz  12894  hash2prd  13257  ccatrcl1  13376  relexprelg  13778  shftlem  13808  rexuzre  14092  cau3lem  14094  caubnd2  14097  caubnd  14098  climrlim2  14278  climuni  14283  2clim  14303  o1co  14317  rlimno1  14384  climbdd  14402  caurcvg  14407  summolem2  14447  summo  14448  zsum  14449  fsumf1o  14454  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumconst  14522  fsumrelem  14539  prodmolem2  14665  prodmo  14666  zprod  14667  fprodf1o  14676  fprodss  14678  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodconst  14708  fprodn0  14709  dfgcd2  15263  coprmproddvdslem  15376  cncongrprm  15437  prmpwdvds  15608  infpnlem1  15614  1arith  15631  vdwapun  15678  vdwlem11  15695  vdwnnlem2  15700  ramz  15729  ramcl  15733  prmlem0  15812  firest  16093  catpropd  16369  initoid  16655  termoid  16656  initoeu2lem1  16664  pltnle  16966  pltletr  16971  pospo  16973  psss  17214  isgrpid2  17458  f1omvdco2  17868  pgpfi  18020  frgpnabllem1  18276  gsumval3eu  18305  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  ablfaclem3  18486  dvdsrtr  18652  dvdsrmul1  18653  unitgrp  18667  lspsolvlem  19142  domnmuln0  19298  gsummoncoe1  19674  pf1ind  19719  gsumfsum  19813  obslbs  20074  dmatscmcl  20309  scmatmulcl  20324  smatvscl  20330  mdetdiaglem  20404  cpmatinvcl  20522  mp2pm2mplem4  20614  cpmadugsumlemF  20681  eltg3  20766  tgidm  20784  neindisj  20921  tgrest  20963  restcld  20976  tgcn  21056  lmcnp  21108  iunconnlem  21230  2ndcredom  21253  2ndc1stc  21254  1stcrest  21256  2ndcrest  21257  2ndcdisj  21259  nllyrest  21289  nllyidm  21292  lfinpfin  21327  locfincmp  21329  ptpjpre1  21374  ptuni2  21379  ptbasin  21380  ptbasfi  21384  txbasval  21409  ptpjopn  21415  ptclsg  21418  dfac14lem  21420  xkoccn  21422  txcnp  21423  ptcnplem  21424  ptcnp  21425  txtube  21443  txcmplem1  21444  txcmplem2  21445  tx2ndc  21454  txkgen  21455  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  qtoprest  21520  kqsat  21534  kqcldsat  21536  isfild  21662  fbunfip  21673  fgabs  21683  filconn  21687  fbasrn  21688  filufint  21724  elfm2  21752  elfm3  21754  fmfnfm  21762  hausflimi  21784  cnpflfi  21803  ptcmplem2  21857  tmdgsum2  21900  cldsubg  21914  qustgpopn  21923  ustfilxp  22016  bldisj  22203  xbln0  22219  blssps  22229  blss  22230  blssexps  22231  blssex  22232  blcls  22311  metcnp3  22345  icccmplem2  22626  cnheibor  22754  iscau4  23077  ovolshftlem2  23278  ovolicc2lem5  23289  dyadmax  23366  mbfi1fseqlem4  23485  mbfi1flimlem  23489  lhop1lem  23776  dvfsumrlim  23794  aalioulem3  24089  ulmcn  24153  radcnvlt1  24172  pilem2  24206  efopn  24404  cxpeq0  24424  cxpmul2z  24437  cxpcn3lem  24488  xrlimcnp  24695  vmappw  24842  fsumvma  24938  dchrptlem1  24989  lgsqr  25076  lgsdchrval  25079  2lgslem3  25129  2sqlem6  25148  2sqlem7  25149  pntlem3  25298  pntleml  25300  brbtwn  25779  brcgr  25780  axcontlem8  25851  nbumgrvtx  26242  cusgrfilem2  26352  1loopgrnb0  26398  uspgr2wlkeq  26542  upgrwlkdvdelem  26632  uspgrn2crct  26700  0enwwlksnge1  26749  usgr2wspthons3  26857  frgrncvvdeqlem9  27171  frgr2wwlkeqm  27195  frgrreggt1  27251  frgrreg  27252  pjhthmo  28161  spansncvi  28511  nmcexi  28885  cnlnssadj  28939  leopmuli  28992  elpjrn  29049  mdsl0  29169  sumdmdii  29274  fmptcof2  29457  suppss3  29502  lmxrge0  29998  bnj594  30982  bnj849  30995  erdszelem7  31179  sconnpi1  31221  cvmsval  31248  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmlift2lem10  31294  cvmlift2lem12  31296  cvmlift3lem5  31305  cvmlift3lem8  31308  sotr3  31656  trpredrec  31738  frr3g  31779  sltval2  31809  nosupno  31849  nosupbnd1lem5  31858  sletr  31883  linethru  32260  opnrebl2  32316  neibastop2lem  32355  neibastop2  32356  bj-ssbequ1  32644  bj-cbv3ta  32710  bj-ismoored  33062  phpreu  33393  finixpnum  33394  matunitlindflem1  33405  ptrecube  33409  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimir  33442  heicant  33444  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  unirep  33507  sdclem2  33538  istotbnd3  33570  ssbnd  33587  lshpdisj  34274  lsatn0  34286  lsat0cv  34320  cvrletrN  34560  cvrval4N  34700  lncvrelatN  35067  paddasslem14  35119  paddasslem15  35120  paddasslem16  35121  pmapjoin  35138  dihglblem2N  36583  dochvalr  36646  incssnn0  37274  eldioph4b  37375  diophren  37377  fphpdo  37381  rencldnfilem  37384  pellexlem5  37397  pell1234qrne0  37417  pell1234qrmulcl  37419  pell14qrgt0  37423  pell1234qrdich  37425  pell14qrdich  37433  pell1qrge1  37434  pell1qrgap  37438  pellfundre  37445  pellfundlb  37448  dvdsacongtr  37551  jm2.19lem4  37559  aomclem4  37627  hbtlem2  37694  hbtlem4  37696  hbtlem6  37699  clcnvlem  37930  ordpss  38655  fmtnofac2lem  41480  opoeALTV  41594  opeoALTV  41595  gboge9  41652  sprsymrelf1lem  41741  sprsymrelfolem2  41743  nzerooringczr  42072  ellcoellss  42224  nn0sumshdiglem1  42415