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  6036  fisseneq  7208  exmidapne  7590  prloc  7822  axcaucvglemres  8230  seqf1oglem1  10908  seqf1oglem2  10909  wrdind  11442  wrd2ind  11443  bezoutlemmain  12722  coprm  12869  sqrt2irr  12887  oddprmdvds  13080  lmodfopnelem1  14601  xblss2ps  15398  xblss2  15399  perfectlem2  15997  lgsprme0  16044  dichmul0orlem7  16642  pw1nct  16916  apdiff  16971