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  4340  swopo  4396  reusv3  4550  ralxfrd  4552  rexxfrd  4553  nlimsucg  4657  poirr2  5120  elpreima  5753  fmptco  5800  tposfo2  6411  nnm00  6674  th3qlem1  6782  fiintim  7089  supmoti  7156  infglbti  7188  infnlbti  7189  updjud  7245  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  uzind  9554  ledivge1le  9918  xltnegi  10027  ixxssixx  10094  seqf1oglem1  10736  expnegzap  10790  shftlem  11322  cau3lem  11620  caubnd2  11623  climuni  11799  2clim  11807  summodclem2  11888  summodc  11889  zsumdc  11890  fsumf1o  11896  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  dfgcd2  12530  cncongrprm  12674  prmpwdvds  12873  infpnlem1  12877  1arith  12885  isgrpid2  13568  dvdsrd  14052  dvdsrtr  14059  dvdsrmul1  14060  unitgrp  14074  domnmuln0  14231  eltg3  14725  tgidm  14742  tgrest  14837  tgcn  14876  lmtopcnp  14918  txbasval  14935  txcnp  14939  bldisj  15069  xblm  15085  blssps  15095  blss  15096  blssexps  15097  blssex  15098  metcnp3  15179  mpomulcn  15234  2lgslem3  15774  2sqlem6  15793  2sqlem7  15794  bj-findis  16300