Theorem 3anidm

Idempotent law for conjunction. (Contributed by Peter Mazsa, 17-Oct-2023.)

Conclusion
\( \vdash \varphi \wedge \varphi \wedge \varphi \leftrightarrow \varphi \)
Proof
l0
df-3an
\( \vdash \varphi \wedge \varphi \wedge \varphi \leftrightarrow \varphi \wedge \varphi \wedge \varphi \)
l1
anabs1
\( \vdash \varphi \wedge \varphi \wedge \varphi \leftrightarrow \varphi \wedge \varphi \)
anidm
\( \vdash \varphi \wedge \varphi \leftrightarrow \varphi \)
3bitri l0 l1 _