Theorem mp2d 47

Description: A double modus ponens deduction. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

Ref	Expression
mp2d.1	|- ( ph -> ps )
mp2d.2	|- ( ph -> ch )
mp2d.3	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
mp2d	|- ( ph -> th )

Proof of Theorem mp2d

Step	Hyp	Ref	Expression
1		mp2d.1	. 2 |- ( ph -> ps )
2		mp2d.2	. . 3 |- ( ph -> ch )
3		mp2d.3	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpid 42	. 2 |- ( ph -> ( ps -> th ) )
5	1, 4	mpd 13	1 |- ( ph -> 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:  riotaeqimp  5995  fisseneq  7126  exmidapne  7478  prloc  7710  axcaucvglemres  8118  seqf1oglem1  10780  seqf1oglem2  10781  wrdind  11302  wrd2ind  11303  bezoutlemmain  12568  coprm  12715  sqrt2irr  12733  oddprmdvds  12926  lmodfopnelem1  14337  xblss2ps  15127  xblss2  15128  perfectlem2  15723  lgsprme0  15770  pw1nct  16604  apdiff  16652