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:  fisseneq  7046  exmidapne  7392  prloc  7624  axcaucvglemres  8032  seqf1oglem1  10686  seqf1oglem2  10687  wrdind  11198  wrd2ind  11199  bezoutlemmain  12394  coprm  12541  sqrt2irr  12559  oddprmdvds  12752  lmodfopnelem1  14161  xblss2ps  14951  xblss2  14952  perfectlem2  15547  lgsprme0  15594  pw1nct  16081  apdiff  16128