Theorem 3anidm12

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

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