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  3982  swopo  4034  reusv3  4158  ralxfrd  4160  rexxfrd  4161  nlimsucg  4242  poirr2  4660  elpreima  5229  fmptco  5273  tposfo2  5823  nnm00  6038  th3qlem1  6144  recexprlemss1l  6606  recexprlemss1u  6607  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  uzind  8105  xltnegi  8498  ixxssixx  8521  expnegzap  8923  bj-findis  9409