Theorem imim1d 75

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 74	1 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim1  76  imbi1d  230  expt  647  hbimd  1553  moim  2070  moimv  2072  sstr2  3135  ssralv  3192  soss  4276  nneneq  6804  prarloclem3  7419  fzind  9284  exbtwnzlemshrink  10157  rebtwn2zlemshrink  10162  seq3fveq2  10377  seq3shft2  10381  monoord  10384  seq3split  10387  seq3id2  10417  seq3coll  10724  rexico  11132  cnntr  12695  setindft  13611