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  231  expt  659  hbimd  1596  moim  2118  moimv  2120  sstr2  3200  ssralv  3257  soss  4361  nneneq  6954  prarloclem3  7610  fzind  9488  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  seq3id2  10671  seqhomog  10675  seq3coll  10987  rexico  11532  cnntr  14697  2sqlem6  15597  setindft  15901