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  6793  nnmord  6794  brecop  6903  findcard2  7197  findcard2s  7198  ordiso2  7381  zindd  9775  ccatopth2  11511  cau3lem  11903  climcau  12138  dvdsabseq  12639  znrrg  15104  metrest  15732  bj-charfunr  17041