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  2631  reu6  2966  fun11iun  5554  poxp  6330  smoel  6398  iinerm  6706  suplub2ti  7117  infglbti  7141  infnlbti  7142  prarloclemlo  7622  peano5uzti  9496  lbzbi  9752  ssfzo12bi  10371  cau3lem  11495  summodc  11764  mertenslem2  11917  prodmodclem2  11958  alzdvds  12235  nno  12287  nn0seqcvgd  12433  lcmdvds  12471  divgcdodd  12535  prmpwdvds  12748  cnptoprest  14781  lmss  14788  txlm  14821  incistruhgr  15756