Theorem imim1d 69

Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis

Ref	Expression
imim1d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
imim1d	|- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		idd 21	. 2 |- ( ph -> ( th -> th ) )
3	1, 2	imim12d 68	1 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim1  70  imbi1d  220  expt  583  hbimd  1465  moim  1964  moimv  1966  sstr2  2952  ssralv  3004  soss  4051  nneneq  6320  prarloclem3  6595  fzind  8353  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  setindft  10090