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  6030  fisseneq  7197  exmidapne  7576  prloc  7808  axcaucvglemres  8216  seqf1oglem1  10885  seqf1oglem2  10886  wrdind  11418  wrd2ind  11419  bezoutlemmain  12698  coprm  12845  sqrt2irr  12863  oddprmdvds  13056  lmodfopnelem1  14489  xblss2ps  15286  xblss2  15287  perfectlem2  15885  lgsprme0  15932  pw1nct  16794  apdiff  16849