Theorem mp3an23

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

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