Theorem anabss7

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

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