Theorem mp3anr3

An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)

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