Theorem anabss5

Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)

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