Theorem 3anidm13

Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)

Hypothesis
3anidm13.1
\( \vdash \varphi \wedge \psi \wedge \varphi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
3anidm13.1
3com23 _
3anidm12 _