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 
|- ( ( ph /\ ph ) <-> ph )

Proof

Step Hyp Ref Expression
1 pm4.24 
 |-  ( ph <-> ( ph /\ ph ) )
2 1 bicomi 
 |-  ( ( ph /\ ph ) <-> ph )