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  2840  rspcimdv  2922  fvimacnv  5793  riotass2  6032  pr2ne  7489  0mnnnnn0  9528  caucvgre  11666  climcn1  11993  climcn2  11994  gcdaddm  12680  dvdsgcd  12708  coprmgcdb  12785  nprm  12820  pcqmul  13001  grpid  13752  uniopn  14866  metcnp3  15376  cncfco  15456  eupth2fi  16474