Theorem anabsi7

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

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