Theorem anabsan2

Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)

Hypothesis
anabsan2.1
\( \vdash \varphi \wedge (\psi \wedge \psi) \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
anabsan2.1
an12s _
anabss7 _