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  5528  poxp  6299  smoel  6367  iinerm  6675  suplub2ti  7076  infglbti  7100  infnlbti  7101  prarloclemlo  7578  peano5uzti  9451  lbzbi  9707  ssfzo12bi  10318  cau3lem  11296  summodc  11565  mertenslem2  11718  prodmodclem2  11759  alzdvds  12036  nno  12088  nn0seqcvgd  12234  lcmdvds  12272  divgcdodd  12336  prmpwdvds  12549  cnptoprest  14559  lmss  14566  txlm  14599