Theorem anandirs

Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Hypothesis
anandirs.1
\( \vdash \varphi \wedge \chi \wedge (\psi \wedge \chi) \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \tau \)
Proof
anandirs.1
an4s _
anabsan2 _