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  4461  nneneq  7162  prarloclem3  7870  fzind  9772  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seq3id2  10984  seqhomog  10988  seq3coll  11316  rexico  12010  cnntr  15451  bcmono  16304  2sqlem6  16444  eupth2lemsfi  16924  setindft  17196