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  1570  falanfal  1573  nic-axALT  1671  inidm  4235  2reu4lem  4528  opcom  5511  poirr  5609  asymref2  6140  xp11  6197  fununi  6643  brprcneu  6897  brprcneuALT  6898  f13dfv  7294  erinxp  8830  dom2lem  9031  pssnn  9207  djuinf  10227  dmaddpi  10928  dmmulpi  10929  gcddvds  16537  iscatd2  17726  dfiso2  17820  isnsg2  19187  eqger  19209  gaorber  19339  efgcpbllemb  19788  xmeter  24459  caucfil  25331  tgcgr4  28554  axcontlem5  28998  cplgr3v  29467  erclwwlkref  30049  clwwlkn2  30073  erclwwlknref  30098  frgr3v  30304  numclwlk1lem1  30398  disjunsn  32614  bnj594  34905  subfaclefac  35161  isbasisrelowllem1  37338  isbasisrelowllem2  37339  inixp  37715  opideq  38325  cdlemg33b  40690  eelT11  44705  uunT11  44794  uunT11p1  44795  uunT11p2  44796  uun111  44803