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  2657  reu6  2995  fun11iun  5604  poxp  6396  smoel  6465  iinerm  6775  suplub2ti  7199  infglbti  7223  infnlbti  7224  prarloclemlo  7713  peano5uzti  9587  lbzbi  9849  ssfzo12bi  10469  cau3lem  11674  summodc  11943  mertenslem2  12096  prodmodclem2  12137  alzdvds  12414  nno  12466  nn0seqcvgd  12612  lcmdvds  12650  divgcdodd  12714  prmpwdvds  12927  cnptoprest  14962  lmss  14969  txlm  15002  incistruhgr  15940