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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  76  imbi1d  231  expt  667  hbimd  1626  moim  2151  moimv  2153  sstr2  3255  ssralv  3312  soss  4459  nneneq  7158  prarloclem3  7865  fzind  9766  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seq3id2  10978  seqhomog  10982  seq3coll  11310  rexico  12004  cnntr  15417  bcmono  16265  2sqlem6  16405  eupth2lemsfi  16885  setindft  17157