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  2667  reu6  3006  fun11iun  5635  poxp  6428  suppssrst  6461  suppssrgst  6462  smoel  6531  iinerm  6841  suplub2ti  7292  infglbti  7316  infnlbti  7317  prarloclemlo  7809  peano5uzti  9686  lbzbi  9948  ssfzo12bi  10570  cau3lem  11799  summodc  12069  mertenslem2  12222  prodmodclem2  12263  alzdvds  12540  nno  12592  nn0seqcvgd  12738  lcmdvds  12776  divgcdodd  12840  prmpwdvds  13053  cnptoprest  15104  lmss  15111  txlm  15144  incistruhgr  16085