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  10956  seqf1oglem2  10957  wrdind  11494  wrd2ind  11495  bezoutlemmain  12775  coprm  12922  sqrt2irr  12940  oddprmdvds  13133  lmodfopnelem1  14661  xblss2ps  15505  xblss2  15506  perfectlem2  16114  lgsprme0  16161  dichmul0orlem7  16759  pw1nct  17033  apdiff  17097