Theorem mpand

A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses
mpand.1
\( \vdash \varphi \rightarrow \psi \)
mpand.2
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Proof
l0
mpand.1
\( \vdash \varphi \rightarrow \psi \)
mpand.2
ancomsd _
\( \vdash \varphi \rightarrow \chi \wedge \psi \rightarrow \theta \)
mpan2d l0 _