Theorem mpdd 36

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 23	. 2 |- (ph -> ((ps -> ch) -> (ps -> th)))
4	1, 3	mpd 14	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  37  mpdi  38  syld  40  syl6c  60  ax12b  1689  oprabid  5551  enprmaplem3  6079