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  2581  reu6  2901  fun11iun  5432  poxp  6173  smoel  6241  iinerm  6545  suplub2ti  6937  infglbti  6961  infnlbti  6962  prarloclemlo  7397  peano5uzti  9255  lbzbi  9507  ssfzo12bi  10106  cau3lem  10996  summodc  11262  mertenslem2  11415  prodmodclem2  11456  alzdvds  11727  nno  11778  nn0seqcvgd  11898  lcmdvds  11936  divgcdodd  11997  cnptoprest  12599  lmss  12606  txlm  12639