Theorem anidms

Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)

Hypothesis
anidms.1
\( \vdash \varphi \wedge \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
anidms.1
ex _
pm2.43i _