Theorem expimpd 355

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  euotd  4009  swopo  4061  reusv3  4210  ralxfrd  4212  rexxfrd  4213  nlimsucg  4309  poirr2  4737  elpreima  5307  fmptco  5351  tposfo2  5905  nnm00  6125  th3qlem1  6231  supmoti  6406  infglbti  6438  infnlbti  6439  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  uzind  8458  ledivge1le  8803  xltnegi  8902  ixxssixx  8925  expnegzap  9510  shftlem  9704  cau3lem  10000  caubnd2  10003  climuni  10132  2clim  10140  dfgcd2  10403  cncongrprm  10536  bj-findis  10774