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  5978  fisseneq  7092  exmidapne  7442  prloc  7674  axcaucvglemres  8082  seqf1oglem1  10736  seqf1oglem2  10737  wrdind  11249  wrd2ind  11250  bezoutlemmain  12514  coprm  12661  sqrt2irr  12679  oddprmdvds  12872  lmodfopnelem1  14282  xblss2ps  15072  xblss2  15073  perfectlem2  15668  lgsprme0  15715  pw1nct  16328  apdiff  16375