Theorem anabsi5

Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)

Hypothesis
anabsi5.1
\( \vdash \varphi \rightarrow \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
l0
simpl
\( \vdash \varphi \wedge \psi \rightarrow \varphi \)
anabsi5.1
\( \vdash \varphi \rightarrow \varphi \wedge \psi \rightarrow \chi \)
mpcom l0 _