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  663  hbimd  1621  moim  2144  moimv  2146  sstr2  3234  ssralv  3291  soss  4411  nneneq  7046  prarloclem3  7720  fzind  9598  exbtwnzlemshrink  10512  rebtwn2zlemshrink  10517  seq3fveq2  10741  seqfveq2g  10743  seq3shft2  10747  seqshft2g  10748  monoord  10751  seq3split  10754  seqsplitg  10755  seq3id2  10792  seqhomog  10796  seq3coll  11110  rexico  11802  cnntr  14976  2sqlem6  15876  eupth2lemsfi  16356  setindft  16619