Theorem mp3an12

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

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