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  2655  reu6  2993  fun11iun  5601  poxp  6392  smoel  6461  iinerm  6771  suplub2ti  7191  infglbti  7215  infnlbti  7216  prarloclemlo  7704  peano5uzti  9578  lbzbi  9840  ssfzo12bi  10460  cau3lem  11665  summodc  11934  mertenslem2  12087  prodmodclem2  12128  alzdvds  12405  nno  12457  nn0seqcvgd  12603  lcmdvds  12641  divgcdodd  12705  prmpwdvds  12918  cnptoprest  14953  lmss  14960  txlm  14993  incistruhgr  15931