Theorem mpdi 42

Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)

Hypotheses

Ref	Expression
mpdi.1	|- ( ps -> ch )
mpdi.2	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
mpdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpdi

Step	Hyp	Ref	Expression
1		mpdi.1	. . 3 |- ( ps -> ch )
2	1	a1i 11	. 2 |- ( ph -> ( ps -> ch ) )
3		mpdi.2	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpdd 40	1 |- ( ph -> ( 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:  mpii  43  pm2.43d  49  impt  159  predpo  5387  suctr  5495  wfrlem12  7034  tfrlem9  7090  axcc2lem  8850  axdc3lem4  8867  fpwwe2lem8  9047  tskcard  9191  nqereu  9339  lbzbi  11217  fleqceilz  12021  ndvdsadd  14277  gcdneg  14375  ulmcaulem  23083  wlkiswwlk1  25119  frgrawopreglem4  25476  frrlem11  30112  relowlpssretop  31294  heicant  31434  brabg2  31501  neificl  31541  el1fzopredsuc  37686