Theorem anandis

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

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