Theorem mpdd 41

Description: A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.)

Hypotheses

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

Assertion

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

Proof of Theorem mpdd

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		mpdd.2	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	a2d 26	. 2 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
4	1, 3	mpd 13	1 |- ( ph -> ( 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:  mpid  42  mpdi  43  syld  45  syl6c  66  mpteqb  5799  oprabid  6120  nnmordi  6794  nnmord  6795  brecop  6904  findcard2  7199  findcard2s  7200  ordiso2  7381  zindd  9774  ccatopth2  11510  cau3lem  11902  climcau  12137  dvdsabseq  12638  znrrg  15103  metrest  15749  bj-charfunr  17058