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	⊢ (𝜑 → 𝜓)
mp2d.2	⊢ (𝜑 → 𝜒)
mp2d.3	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
mp2d	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2d

Step	Hyp	Ref	Expression
1		mp2d.1	. 2 ⊢ (𝜑 → 𝜓)
2		mp2d.2	. . 3 ⊢ (𝜑 → 𝜒)
3		mp2d.3	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpid 42	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜃)

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  5996  fisseneq  7127  exmidapne  7479  prloc  7711  axcaucvglemres  8119  seqf1oglem1  10782  seqf1oglem2  10783  wrdind  11304  wrd2ind  11305  bezoutlemmain  12571  coprm  12718  sqrt2irr  12736  oddprmdvds  12929  lmodfopnelem1  14341  xblss2ps  15131  xblss2  15132  perfectlem2  15727  lgsprme0  15774  pw1nct  16625  apdiff  16673