Theorem expdimp 255

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  rexlimdvv  2484  reu6  2782  fun11iun  5178  poxp  5884  smoel  5949  iinerm  6244  suplub2ti  6473  infglbti  6497  infnlbti  6498  prarloclemlo  6746  peano5uzti  8536  lbzbi  8782  ssfzo12bi  9311  cau3lem  10138  alzdvds  10399  nno  10450  nn0seqcvgd  10567  lcmdvds  10605  divgcdodd  10666