Theorem anidm 565

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 564	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 223	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anidmdbi  566  anandi  673  anandir  674  3anidm  1103  truantru  1573  falanfal  1576  nic-axALT  1675  inidm  4163  2reu4lem  4468  opcom  5434  poirr  5533  asymref2  6044  xp11  6100  fununi  6545  brprcneu  6801  brprcneuALT  6802  f13dfv  7185  erinxp  8628  dom2lem  8830  pssnn  9010  pssnnOLD  9107  djuinf  10017  dmaddpi  10719  dmmulpi  10720  gcddvds  16282  iscatd2  17460  dfiso2  17554  isnsg2  18853  eqger  18875  gaorber  18983  efgcpbllemb  19429  xmeter  23658  caucfil  24519  tgcgr4  27001  axcontlem5  27445  cplgr3v  27911  erclwwlkref  28493  clwwlkn2  28517  erclwwlknref  28542  frgr3v  28748  numclwlk1lem1  28842  disjunsn  31041  bnj594  32997  subfaclefac  33243  isbasisrelowllem1  35582  isbasisrelowllem2  35583  inixp  35942  opideq  36560  cdlemg33b  38926  eelT11  42548  uunT11  42637  uunT11p1  42638  uunT11p2  42639  uun111  42646