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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  riotaeqimp  6066  fisseneq  7248  exmidapne  7632  prloc  7864  axcaucvglemres  8272  seqf1oglem1  10976  seqf1oglem2  10977  wrdind  11515  wrd2ind  11516  bezoutlemmain  12799  coprm  12947  sqrt2irr  12965  oddprmdvds  13161  lmodfopnelem1  14769  xblss2ps  15647  xblss2  15648  perfectlem2  16317  lgsprme0  16383  dichmul0orlem7  16981  pw1nct  17255  apdiff  17321