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  6028  fisseneq  7195  exmidapne  7574  prloc  7806  axcaucvglemres  8214  seqf1oglem1  10881  seqf1oglem2  10882  wrdind  11414  wrd2ind  11415  bezoutlemmain  12694  coprm  12841  sqrt2irr  12859  oddprmdvds  13052  lmodfopnelem1  14472  xblss2ps  15269  xblss2  15270  perfectlem2  15868  lgsprme0  15915  pw1nct  16777  apdiff  16832