Metamath Proof Explorer

Theorem 3anidm

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

Ref Expression
Assertion 3anidm ⊢ φ ∧ φ ∧ φ ↔ φ

Proof

Step Hyp Ref Expression
1 df-3an ⊢ φ ∧ φ ∧ φ ↔ φ ∧ φ ∧ φ
2 anabs1 ⊢ φ ∧ φ ∧ φ ↔ φ ∧ φ
3 anidm ⊢ φ ∧ φ ↔ φ
4 1 2 3 3bitri ⊢ φ ∧ φ ∧ φ ↔ φ