Theorem mp3anl1

An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)

Hypotheses
mp3anl1.1
\( \vdash \varphi \)
mp3anl1.2
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
l0
mp3anl1.1
\( \vdash \varphi \)
mp3anl1.2
ex _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \rightarrow \tau \)
mp3an1 l0 _
imp _