Theorem mp3anl2

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

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