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  2590  reu6  2915  fun11iun  5453  poxp  6200  smoel  6268  iinerm  6573  suplub2ti  6966  infglbti  6990  infnlbti  6991  prarloclemlo  7435  peano5uzti  9299  lbzbi  9554  ssfzo12bi  10160  cau3lem  11056  summodc  11324  mertenslem2  11477  prodmodclem2  11518  alzdvds  11792  nno  11843  nn0seqcvgd  11973  lcmdvds  12011  divgcdodd  12075  prmpwdvds  12285  cnptoprest  12879  lmss  12886  txlm  12919