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  4190  2reu4lem  4485  opcom  5461  poirr  5558  asymref2  6090  xp11  6148  fununi  6591  brprcneu  6848  brprcneuALT  6849  f13dfv  7249  erinxp  8764  dom2lem  8963  pssnn  9132  djuinf  10142  dmaddpi  10843  dmmulpi  10844  gcddvds  16473  iscatd2  17642  dfiso2  17734  isnsg2  19088  eqger  19110  gaorber  19240  efgcpbllemb  19685  xmeter  24321  caucfil  25183  tgcgr4  28458  axcontlem5  28895  cplgr3v  29362  erclwwlkref  29949  clwwlkn2  29973  erclwwlknref  29998  frgr3v  30204  numclwlk1lem1  30298  disjunsn  32523  bnj594  34902  subfaclefac  35163  isbasisrelowllem1  37343  isbasisrelowllem2  37344  inixp  37722  opideq  38325  cdlemg33b  40701  eelT11  44696  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uun111  44794