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  2658  reu6  2996  fun11iun  5613  poxp  6406  suppssrst  6439  suppssrgst  6440  smoel  6509  iinerm  6819  suplub2ti  7243  infglbti  7267  infnlbti  7268  prarloclemlo  7757  peano5uzti  9632  lbzbi  9894  ssfzo12bi  10516  cau3lem  11737  summodc  12007  mertenslem2  12160  prodmodclem2  12201  alzdvds  12478  nno  12530  nn0seqcvgd  12676  lcmdvds  12714  divgcdodd  12778  prmpwdvds  12991  cnptoprest  15033  lmss  15040  txlm  15073  incistruhgr  16014