Theorem mpid 42

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 41	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:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  428  ceqsalt  2826  rspcimdv  2908  fvimacnv  5749  riotass2  5982  pr2ne  7361  0mnnnnn0  9397  caucvgre  11487  climcn1  11814  climcn2  11815  gcdaddm  12500  dvdsgcd  12528  coprmgcdb  12605  nprm  12640  pcqmul  12821  grpid  13567  uniopn  14669  metcnp3  15179  cncfco  15259