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  4193  2reu4lem  4488  opcom  5464  poirr  5561  asymref2  6093  xp11  6151  fununi  6594  brprcneu  6851  brprcneuALT  6852  f13dfv  7252  erinxp  8767  dom2lem  8966  pssnn  9138  djuinf  10149  dmaddpi  10850  dmmulpi  10851  gcddvds  16480  iscatd2  17649  dfiso2  17741  isnsg2  19095  eqger  19117  gaorber  19247  efgcpbllemb  19692  xmeter  24328  caucfil  25190  tgcgr4  28465  axcontlem5  28902  cplgr3v  29369  erclwwlkref  29956  clwwlkn2  29980  erclwwlknref  30005  frgr3v  30211  numclwlk1lem1  30305  disjunsn  32530  bnj594  34909  subfaclefac  35170  isbasisrelowllem1  37350  isbasisrelowllem2  37351  inixp  37729  opideq  38332  cdlemg33b  40708  eelT11  44703  uunT11  44792  uunT11p1  44793  uunT11p2  44794  uun111  44801