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  11641  summodc  11910  mertenslem2  12063  prodmodclem2  12104  alzdvds  12381  nno  12433  nn0seqcvgd  12579  lcmdvds  12617  divgcdodd  12681  prmpwdvds  12894  cnptoprest  14929  lmss  14936  txlm  14969  incistruhgr  15906