Theorem mp2ani

An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses
mp2ani.1
\( \vdash \psi \)
mp2ani.2
\( \vdash \chi \)
mp2ani.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
mp2ani.2
\( \vdash \chi \)
l1
mp2ani.1
\( \vdash \psi \)
mp2ani.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
mpani l1 _
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
mpi l0 _