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  677  anandir  678  3anidm  1104  truantru  1575  falanfal  1578  nic-axALT  1676  inidm  4181  2reu4lem  4478  opcom  5457  poirr  5552  asymref2  6082  xp11  6141  fununi  6575  brprcneu  6832  brprcneuALT  6833  f13dfv  7230  erinxp  8740  dom2lem  8941  pssnn  9105  djuinf  10111  dmaddpi  10813  dmmulpi  10814  gcddvds  16442  iscatd2  17616  dfiso2  17708  isnsg2  19100  eqger  19122  gaorber  19252  efgcpbllemb  19699  xmeter  24392  caucfil  25254  tgcgr4  28619  axcontlem5  29057  cplgr3v  29524  erclwwlkref  30111  clwwlkn2  30135  erclwwlknref  30160  frgr3v  30366  numclwlk1lem1  30460  disjunsn  32685  bnj594  35092  subfaclefac  35396  isbasisrelowllem1  37614  isbasisrelowllem2  37615  inixp  37983  opideq  38598  cdlemg33b  41087  eelT11  45066  uunT11  45155  uunT11p1  45156  uunT11p2  45157  uun111  45164