Theorem expdimp 257

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 256	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rexlimdvv  2594  reu6  2919  fun11iun  5463  poxp  6211  smoel  6279  iinerm  6585  suplub2ti  6978  infglbti  7002  infnlbti  7003  prarloclemlo  7456  peano5uzti  9320  lbzbi  9575  ssfzo12bi  10181  cau3lem  11078  summodc  11346  mertenslem2  11499  prodmodclem2  11540  alzdvds  11814  nno  11865  nn0seqcvgd  11995  lcmdvds  12033  divgcdodd  12097  prmpwdvds  12307  cnptoprest  13033  lmss  13040  txlm  13073