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  2992  fun11iun  5595  poxp  6384  smoel  6452  iinerm  6762  suplub2ti  7179  infglbti  7203  infnlbti  7204  prarloclemlo  7692  peano5uzti  9566  lbzbi  9823  ssfzo12bi  10443  cau3lem  11640  summodc  11909  mertenslem2  12062  prodmodclem2  12103  alzdvds  12380  nno  12432  nn0seqcvgd  12578  lcmdvds  12616  divgcdodd  12680  prmpwdvds  12893  cnptoprest  14928  lmss  14935  txlm  14968  incistruhgr  15905