Theorem anidm

Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Conclusion

\( \vdash \varphi \wedge \varphi \leftrightarrow \varphi \)

Proof

pm4.24

bicomi _