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  6053  fisseneq  7232  exmidapne  7616  prloc  7848  axcaucvglemres  8256  seqf1oglem1  10934  seqf1oglem2  10935  wrdind  11472  wrd2ind  11473  bezoutlemmain  12753  coprm  12900  sqrt2irr  12918  oddprmdvds  13111  lmodfopnelem1  14633  xblss2ps  15428  xblss2  15429  perfectlem2  16028  lgsprme0  16075  dichmul0orlem7  16673  pw1nct  16947  apdiff  17002