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  5991  fisseneq  7119  exmidapne  7469  prloc  7701  axcaucvglemres  8109  seqf1oglem1  10771  seqf1oglem2  10772  wrdind  11293  wrd2ind  11294  bezoutlemmain  12559  coprm  12706  sqrt2irr  12724  oddprmdvds  12917  lmodfopnelem1  14328  xblss2ps  15118  xblss2  15119  perfectlem2  15714  lgsprme0  15761  pw1nct  16540  apdiff  16588