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  5796  oprabid  6117  nnmordi  6789  nnmord  6790  brecop  6899  findcard2  7193  findcard2s  7194  ordiso2  7375  zindd  9764  ccatopth2  11489  cau3lem  11880  climcau  12113  dvdsabseq  12614  znrrg  14995  metrest  15607  bj-charfunr  16836