Theorem mp3an

An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses
mp3an.1
\( \vdash \varphi \)
mp3an.2
\( \vdash \psi \)
mp3an.3
\( \vdash \chi \)
mp3an.4
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \theta \)
Proof
l0
mp3an.2
\( \vdash \psi \)
l1
mp3an.3
\( \vdash \chi \)
l2
mp3an.1
\( \vdash \varphi \)
mp3an.4
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mp3an1 l2 _
\( \vdash \psi \wedge \chi \rightarrow \theta \)
mp2an l0 l1 _