Metamath Proof Explorer

Theorem anidm

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

Ref Expression
Assertion anidm ( ( 𝜑 ∧ 𝜑 ) ↔ 𝜑 )

Proof

Step Hyp Ref Expression
1 pm4.24 ⊢ ( 𝜑 ↔ ( 𝜑 ∧ 𝜑 ) )
2 1 bicomi ⊢ ( ( 𝜑 ∧ 𝜑 ) ↔ 𝜑 )