Theorem mpid 41

Description: A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
mpid.1	|- ( ph -> ch )
mpid.2	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
mpid	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpid

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 |- ( ph -> ch )
2	1	a1d 22	. 2 |- ( ph -> ( ps -> ch ) )
3		mpid.2	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpdd 40	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  mp2d  46  pm2.43a  50  embantd  55  mpan2d  419  ceqsalt  2626  rspcimdv  2703  fvimacnv  5308  riotass2  5519  pr2ne  6510  0mnnnnn0  8376  caucvgre  9994  climcn1  10274  climcn2  10275  gcdaddm  10508  dvdsgcd  10534  coprmgcdb  10603  nprm  10638