Theorem mp3anr1

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

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