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  6607  recexprlemss1u  6608  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  uzind  8125  xltnegi  8518  ixxssixx  8541  expnegzap  8943  bj-findis  9439