Theorem expdimp 259

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
exp3a.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expdimp	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 258	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  rexlimdvv  2611  reu6  2938  fun11iun  5494  poxp  6247  smoel  6315  iinerm  6621  suplub2ti  7014  infglbti  7038  infnlbti  7039  prarloclemlo  7507  peano5uzti  9375  lbzbi  9630  ssfzo12bi  10239  cau3lem  11137  summodc  11405  mertenslem2  11558  prodmodclem2  11599  alzdvds  11874  nno  11925  nn0seqcvgd  12055  lcmdvds  12093  divgcdodd  12157  prmpwdvds  12367  cnptoprest  14035  lmss  14042  txlm  14075