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  2829  rspcimdv  2911  fvimacnv  5762  riotass2  5999  pr2ne  7396  0mnnnnn0  9433  caucvgre  11541  climcn1  11868  climcn2  11869  gcdaddm  12554  dvdsgcd  12582  coprmgcdb  12659  nprm  12694  pcqmul  12875  grpid  13621  uniopn  14724  metcnp3  15234  cncfco  15314