Theorem anabsi8

Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)

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