Theorem anabss4

Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)

Hypothesis
anabss4.1
\( \vdash \psi \wedge \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
anabss4.1
anabss1 _
ancoms _