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  5985  fisseneq  7107  exmidapne  7457  prloc  7689  axcaucvglemres  8097  seqf1oglem1  10753  seqf1oglem2  10754  wrdind  11269  wrd2ind  11270  bezoutlemmain  12534  coprm  12681  sqrt2irr  12699  oddprmdvds  12892  lmodfopnelem1  14303  xblss2ps  15093  xblss2  15094  perfectlem2  15689  lgsprme0  15736  pw1nct  16428  apdiff  16476