Theorem mp3anr2

An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)

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