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  2798  rspcimdv  2878  fvimacnv  5695  riotass2  5926  pr2ne  7300  0mnnnnn0  9327  caucvgre  11292  climcn1  11619  climcn2  11620  gcdaddm  12305  dvdsgcd  12333  coprmgcdb  12410  nprm  12445  pcqmul  12626  grpid  13371  uniopn  14473  metcnp3  14983  cncfco  15063