Theorem expimpd 363

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 115	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 254	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  euotd  4371  swopo  4427  reusv3  4581  ralxfrd  4583  rexxfrd  4584  nlimsucg  4688  poirr2  5155  elpreima  5797  fmptco  5843  suppssdc  6460  tposfo2  6498  nnm00  6763  th3qlem1  6871  fiintim  7191  supmoti  7284  infglbti  7316  infnlbti  7317  updjud  7373  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  uzind  9689  ledivge1le  10059  xltnegi  10168  ixxssixx  10235  seqf1oglem1  10881  expnegzap  10935  ccatrcl1  11302  shftlem  11501  cau3lem  11799  caubnd2  11802  climuni  11978  2clim  11986  summodclem2  12068  summodc  12069  zsumdc  12070  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  dfgcd2  12710  cncongrprm  12854  prmpwdvds  13053  infpnlem1  13057  1arith  13065  isgrpid2  13753  dvdsrd  14239  dvdsrtr  14246  dvdsrmul1  14247  unitgrp  14261  domnmuln0  14419  eltg3  14922  tgidm  14939  tgrest  15034  tgcn  15073  lmtopcnp  15115  txbasval  15132  txcnp  15136  bldisj  15266  xblm  15282  blssps  15292  blss  15293  blssexps  15294  blssex  15295  metcnp3  15376  mpomulcn  15431  2lgslem3  15974  2sqlem6  15993  2sqlem7  15994  uspgr2wlkeq  16360  wlklenvclwlk  16368  clwwlkccatlem  16395  clwwlknonel  16427  bj-findis  16749