Theorem mp2d

A double modus ponens deduction. Deduction associated with mp2. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses
mp2d.1
\( \vdash \varphi \rightarrow \psi \)
mp2d.2
\( \vdash \varphi \rightarrow \chi \)
mp2d.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
mp2d.1
\( \vdash \varphi \rightarrow \psi \)
l1
mp2d.2
\( \vdash \varphi \rightarrow \chi \)
mp2d.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
mpid l1 _
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
mpd l0 _