Theorem anidm 625

Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Assertion

Ref	Expression
anidm	⊢ ((φ ∧ φ) ↔ φ)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm4.24 624	. 2 ⊢ (φ ↔ (φ ∧ φ))
2	1	bicomi 193	1 ⊢ ((φ ∧ φ) ↔ φ)

Syntax hints:   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anidmdbi  627  anandi  801  anandir  802  nannot  1293  truantru  1336  falanfal  1339  nic-axALT  1439  sbnf2  2108  2eu4  2287  elcomplg  3219  inidm  3465  ncfinlower  4484  nnpw1ex  4485  nnpweq  4524  phialllem1  4617  xp11  5057  fununi  5161