Theorem expimpd 358

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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  euotd  4114  swopo  4166  reusv3  4319  ralxfrd  4321  rexxfrd  4322  nlimsucg  4419  poirr2  4867  elpreima  5471  fmptco  5518  tposfo2  6094  nnm00  6355  th3qlem1  6461  fiintim  6746  supmoti  6795  infglbti  6827  infnlbti  6828  updjud  6882  recexprlemss1l  7344  recexprlemss1u  7345  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemladdrl  7387  uzind  9014  ledivge1le  9360  xltnegi  9459  ixxssixx  9526  expnegzap  10168  shftlem  10429  cau3lem  10726  caubnd2  10729  climuni  10901  2clim  10909  summodclem2  10990  summodc  10991  zsumdc  10992  fsumf1o  10998  fisumss  11000  fsumcl2lem  11006  fsumadd  11014  fsummulc2  11056  dfgcd2  11495  cncongrprm  11628  eltg3  12008  tgidm  12025  tgrest  12120  tgcn  12158  lmtopcnp  12200  txbasval  12217  txcnp  12221  bldisj  12329  xblm  12345  blssps  12355  blss  12356  blssexps  12357  blssex  12358  metcnp3  12435  bj-findis  12762