Theorem mp3anl3

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

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