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  5652  oprabid  5954  nnmordi  6574  nnmord  6575  brecop  6684  findcard2  6950  findcard2s  6951  ordiso2  7101  zindd  9444  cau3lem  11279  climcau  11512  dvdsabseq  12012  znrrg  14216  metrest  14742  bj-charfunr  15456