Theorem mp3an13

An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses
mp3an13.1
\( \vdash \varphi \)
mp3an13.2
\( \vdash \chi \)
mp3an13.3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \rightarrow \theta \)
Proof
l0
mp3an13.1
\( \vdash \varphi \)
l1
mp3an13.2
\( \vdash \chi \)
mp3an13.3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mp3an3 l1 _
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
mpan l0 _