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  5592  poxp  6376  smoel  6444  iinerm  6752  suplub2ti  7164  infglbti  7188  infnlbti  7189  prarloclemlo  7677  peano5uzti  9551  lbzbi  9807  ssfzo12bi  10426  cau3lem  11620  summodc  11889  mertenslem2  12042  prodmodclem2  12083  alzdvds  12360  nno  12412  nn0seqcvgd  12558  lcmdvds  12596  divgcdodd  12660  prmpwdvds  12873  cnptoprest  14907  lmss  14914  txlm  14947  incistruhgr  15884