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  418  ceqsalt  2625  rspcimdv  2702  fvimacnv  5303  riotass2  5514  pr2ne  6461  0mnnnnn0  8320  caucvgre  9867  climcn1  10147  climcn2  10148  gcdaddm  10375  dvdsgcd  10401  coprmgcdb  10470  nprm  10505