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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rexlimdvv  2675  reu6  3015  ifeqeqxdc  3687  fun11iun  5663  poxp  6472  suppssrst  6505  suppssrgst  6506  smoel  6576  iinerm  6886  suplub2ti  7347  infglbti  7371  infnlbti  7372  prarloclemlo  7867  peano5uzti  9764  lbzbi  10031  ssfzo12bi  10659  cau3lem  11902  summodc  12174  mertenslem2  12327  prodmodclem2  12368  alzdvds  12645  nno  12697  nn0seqcvgd  12843  lcmdvds  12881  divgcdodd  12946  prmpwdvds  13162  cnptoprest  15482  lmss  15489  txlm  15522  incistruhgr  16553