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  7627  prloc  7859  axcaucvglemres  8267  seqf1oglem1  10971  seqf1oglem2  10972  wrdind  11510  wrd2ind  11511  bezoutlemmain  12794  coprm  12942  sqrt2irr  12960  oddprmdvds  13156  lmodfopnelem1  14745  xblss2ps  15596  xblss2  15597  perfectlem2  16261  lgsprme0  16327  dichmul0orlem7  16925  pw1nct  17199  apdiff  17264