Theorem anidm 564

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

Assertion

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

Proof of Theorem anidm

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidmdbi  565  anandi  676  anandir  677  3anidm  1103  truantru  1573  falanfal  1576  nic-axALT  1674  inidm  4186  2reu4lem  4481  opcom  5456  poirr  5551  asymref2  6078  xp11  6136  fununi  6575  brprcneu  6830  brprcneuALT  6831  f13dfv  7231  erinxp  8741  dom2lem  8940  pssnn  9109  djuinf  10118  dmaddpi  10819  dmmulpi  10820  gcddvds  16449  iscatd2  17622  dfiso2  17714  isnsg2  19070  eqger  19092  gaorber  19222  efgcpbllemb  19669  xmeter  24354  caucfil  25216  tgcgr4  28511  axcontlem5  28948  cplgr3v  29415  erclwwlkref  29999  clwwlkn2  30023  erclwwlknref  30048  frgr3v  30254  numclwlk1lem1  30348  disjunsn  32573  bnj594  34895  subfaclefac  35156  isbasisrelowllem1  37336  isbasisrelowllem2  37337  inixp  37715  opideq  38318  cdlemg33b  40694  eelT11  44689  uunT11  44778  uunT11p1  44779  uunT11p2  44780  uun111  44787