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  5952  fisseneq  7064  exmidapne  7414  prloc  7646  axcaucvglemres  8054  seqf1oglem1  10708  seqf1oglem2  10709  wrdind  11220  wrd2ind  11221  bezoutlemmain  12485  coprm  12632  sqrt2irr  12650  oddprmdvds  12843  lmodfopnelem1  14253  xblss2ps  15043  xblss2  15044  perfectlem2  15639  lgsprme0  15686  pw1nct  16280  apdiff  16327