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  48  impt  157  suctr  4903  tfrlem9  6947  axcc2lem  8709  axdc3lem4  8726  fpwwe2lem8  8908  tskcard  9052  nqereu  9202  mulcmpblnr  9345  lbzbi  11047  fleqceilz  11803  ndvdsadd  13723  gcdneg  13821  ulmcaulem  21985  predpo  27782  wfrlem12  27872  frrlem11  27917  heicant  28567  brabg2  28750  neificl  28790  wlkiswwlk1  30465  frgrawopreglem4  30781