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 ⊢ (𝜑 → 𝜃)

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  7247  exmidapne  7633  prloc  7865  axcaucvglemres  8273  seqf1oglem1  10978  seqf1oglem2  10979  wrdind  11517  wrd2ind  11518  bezoutlemmain  12801  coprm  12949  sqrt2irr  12967  oddprmdvds  13163  lmodfopnelem1  14771  xblss2ps  15642  xblss2  15643  perfectlem2  16312  lgsprme0  16378  dichmul0orlem7  16976  pw1nct  17250  apdiff  17316