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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  432  ceqsalt  2848  rspcimdv  2930  fvimacnv  5827  riotass2  6070  pr2ne  7544  0mnnnnn0  9606  caucvgre  11769  climcn1  12099  climcn2  12100  gcdaddm  12786  dvdsgcd  12814  coprmgcdb  12891  nprm  12926  pcqmul  13111  grpid  13903  uniopn  15227  metcnp3  15737  cncfco  15817  eupth2fi  16925