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  6006  fisseneq  7170  exmidapne  7522  prloc  7754  axcaucvglemres  8162  seqf1oglem1  10827  seqf1oglem2  10828  wrdind  11352  wrd2ind  11353  bezoutlemmain  12632  coprm  12779  sqrt2irr  12797  oddprmdvds  12990  lmodfopnelem1  14403  xblss2ps  15198  xblss2  15199  perfectlem2  15797  lgsprme0  15844  pw1nct  16708  apdiff  16763