Theorem anabsan

Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.)

Hypothesis
anabsan.1
\( \vdash \varphi \wedge \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
l0
pm4.24
\( \vdash \varphi \leftrightarrow \varphi \wedge \varphi \)
anabsan.1
\( \vdash \varphi \wedge \varphi \wedge \psi \rightarrow \chi \)
sylanb l0 _