Theorem expimpd 361

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  euotd  4239  swopo  4291  reusv3  4445  ralxfrd  4447  rexxfrd  4448  nlimsucg  4550  poirr2  5003  elpreima  5615  fmptco  5662  tposfo2  6246  nnm00  6509  th3qlem1  6615  fiintim  6906  supmoti  6970  infglbti  7002  infnlbti  7003  updjud  7059  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  uzind  9323  ledivge1le  9683  xltnegi  9792  ixxssixx  9859  expnegzap  10510  shftlem  10780  cau3lem  11078  caubnd2  11081  climuni  11256  2clim  11264  summodclem2  11345  summodc  11346  zsumdc  11347  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  dfgcd2  11969  cncongrprm  12111  prmpwdvds  12307  infpnlem1  12311  1arith  12319  isgrpid2  12743  eltg3  12851  tgidm  12868  tgrest  12963  tgcn  13002  lmtopcnp  13044  txbasval  13061  txcnp  13065  bldisj  13195  xblm  13211  blssps  13221  blss  13222  blssexps  13223  blssex  13224  metcnp3  13305  2sqlem6  13750  2sqlem7  13751  bj-findis  14014