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  4232  swopo  4284  reusv3  4438  ralxfrd  4440  rexxfrd  4441  nlimsucg  4543  poirr2  4996  elpreima  5604  fmptco  5651  tposfo2  6235  nnm00  6497  th3qlem1  6603  fiintim  6894  supmoti  6958  infglbti  6990  infnlbti  6991  updjud  7047  recexprlemss1l  7576  recexprlemss1u  7577  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemladdrl  7619  uzind  9302  ledivge1le  9662  xltnegi  9771  ixxssixx  9838  expnegzap  10489  shftlem  10758  cau3lem  11056  caubnd2  11059  climuni  11234  2clim  11242  summodclem2  11323  summodc  11324  zsumdc  11325  fsumf1o  11331  fisumss  11333  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  prodmodclem2  11518  prodmodc  11519  zproddc  11520  fprodf1o  11529  fprodssdc  11531  fprodmul  11532  dfgcd2  11947  cncongrprm  12089  prmpwdvds  12285  infpnlem1  12289  1arith  12297  eltg3  12697  tgidm  12714  tgrest  12809  tgcn  12848  lmtopcnp  12890  txbasval  12907  txcnp  12911  bldisj  13041  xblm  13057  blssps  13067  blss  13068  blssexps  13069  blssex  13070  metcnp3  13151  2sqlem6  13596  2sqlem7  13597  bj-findis  13861