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  2621  reu6  2953  fun11iun  5525  poxp  6290  smoel  6358  iinerm  6666  suplub2ti  7067  infglbti  7091  infnlbti  7092  prarloclemlo  7561  peano5uzti  9434  lbzbi  9690  ssfzo12bi  10301  cau3lem  11279  summodc  11548  mertenslem2  11701  prodmodclem2  11742  alzdvds  12019  nno  12071  nn0seqcvgd  12209  lcmdvds  12247  divgcdodd  12311  prmpwdvds  12524  cnptoprest  14475  lmss  14482  txlm  14515