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  230  expt  646  hbimd  1552  moim  2063  moimv  2065  sstr2  3104  ssralv  3161  soss  4236  nneneq  6751  prarloclem3  7305  fzind  9166  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  seq3id2  10282  seq3coll  10585  rexico  10993  cnntr  12394  setindft  13163