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  6066  fisseneq  7246  exmidapne  7632  prloc  7864  axcaucvglemres  8272  seqf1oglem1  10977  seqf1oglem2  10978  wrdind  11516  wrd2ind  11517  bezoutlemmain  12800  coprm  12948  sqrt2irr  12966  oddprmdvds  13162  lmodfopnelem1  14770  xblss2ps  15630  xblss2  15631  perfectlem2  16300  lgsprme0  16366  dichmul0orlem7  16964  pw1nct  17238  apdiff  17304