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  2618  reu6  2950  fun11iun  5522  poxp  6287  smoel  6355  iinerm  6663  suplub2ti  7062  infglbti  7086  infnlbti  7087  prarloclemlo  7556  peano5uzti  9428  lbzbi  9684  ssfzo12bi  10295  cau3lem  11261  summodc  11529  mertenslem2  11682  prodmodclem2  11723  alzdvds  11999  nno  12050  nn0seqcvgd  12182  lcmdvds  12220  divgcdodd  12284  prmpwdvds  12496  cnptoprest  14418  lmss  14425  txlm  14458