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  661  hbimd  1619  moim  2142  moimv  2144  sstr2  3232  ssralv  3289  soss  4409  nneneq  7038  prarloclem3  7707  fzind  9585  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seq3id2  10778  seqhomog  10782  seq3coll  11096  rexico  11772  cnntr  14939  2sqlem6  15839  setindft  16496