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  6063  fisseneq  7242  exmidapne  7626  prloc  7858  axcaucvglemres  8266  seqf1oglem1  10969  seqf1oglem2  10970  wrdind  11508  wrd2ind  11509  bezoutlemmain  12791  coprm  12939  sqrt2irr  12957  oddprmdvds  13153  lmodfopnelem1  14710  xblss2ps  15554  xblss2  15555  perfectlem2  16198  lgsprme0  16259  dichmul0orlem7  16857  pw1nct  17131  apdiff  17195