Theorem mpan9

Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses
mpan9.1
\( \vdash \varphi \rightarrow \psi \)
mpan9.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Proof
l0
mpan9.1
\( \vdash \varphi \rightarrow \psi \)
mpan9.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
syl5 l0 _
impcom _