Theorem expimpd 345

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  euotd  3991  swopo  4043  reusv3  4192  ralxfrd  4194  rexxfrd  4195  nlimsucg  4290  poirr2  4717  elpreima  5286  fmptco  5330  tposfo2  5882  nnm00  6102  th3qlem1  6208  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  uzind  8349  ledivge1le  8652  xltnegi  8748  ixxssixx  8771  expnegzap  9289  shftlem  9417  cau3lem  9710  caubnd2  9713  climuni  9814  2clim  9822  bj-findis  10104