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  1622  moim  2147  moimv  2149  sstr2  3247  ssralv  3304  soss  4437  nneneq  7113  prarloclem3  7814  fzind  9696  exbtwnzlemshrink  10612  rebtwn2zlemshrink  10617  seq3fveq2  10841  seqfveq2g  10843  seq3shft2  10847  seqshft2g  10848  monoord  10851  seq3split  10854  seqsplitg  10855  seq3id2  10892  seqhomog  10896  seq3coll  11218  rexico  11910  cnntr  15107  2sqlem6  16010  eupth2lemsfi  16490  setindft  16752