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 ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpid  42  mpdi  43  syld  45  syl6c  66  mpteqb  5519  oprabid  5811  nnmordi  6420  nnmord  6421  brecop  6527  findcard2  6791  findcard2s  6792  ordiso2  6928  zindd  9193  cau3lem  10918  climcau  11148  dvdsabseq  11581  metrest  12714