Theorem 3anidm23

Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)

Hypothesis
3anidm23.1
\( \vdash \varphi \wedge \psi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
3anidm23.1
3expa _
anabss3 _