Theorem anabss3

Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)

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