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  2675  reu6  3015  ifeqeqxdc  3684  fun11iun  5655  poxp  6458  suppssrst  6491  suppssrgst  6492  smoel  6561  iinerm  6871  suplub2ti  7331  infglbti  7355  infnlbti  7356  prarloclemlo  7851  peano5uzti  9733  lbzbi  9995  ssfzo12bi  10621  cau3lem  11858  summodc  12128  mertenslem2  12281  prodmodclem2  12322  alzdvds  12599  nno  12651  nn0seqcvgd  12797  lcmdvds  12835  divgcdodd  12899  prmpwdvds  13112  cnptoprest  15263  lmss  15270  txlm  15303  incistruhgr  16245