Theorem anabss1

Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)

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