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  2761  rspcimdv  2840  fvimacnv  5623  riotass2  5847  pr2ne  7181  0mnnnnn0  9179  caucvgre  10956  climcn1  11282  climcn2  11283  gcdaddm  11950  dvdsgcd  11978  coprmgcdb  12053  nprm  12088  pcqmul  12268  grpid  12772  uniopn  13050  metcnp3  13562  cncfco  13629