Theorem anidm 567

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anidmdbi  568  anandi  674  anandir  675  3anidm  1099  truantru  1564  falanfal  1567  nic-axALT  1669  inidm  4193  2reu4lem  4463  opcom  5382  poirr  5478  asymref2  5970  xp11  6025  fununi  6422  brprcneu  6655  f13dfv  7023  erinxp  8363  dom2lem  8541  pssnn  8728  djuinf  9606  dmaddpi  10304  dmmulpi  10305  gcddvds  15844  iscatd2  16944  dfiso2  17034  isnsg2  18300  eqger  18322  gaorber  18430  efgcpbllemb  18873  xmeter  23035  caucfil  23878  tgcgr4  26309  axcontlem5  26746  cplgr3v  27209  erclwwlkref  27790  clwwlkn2  27814  erclwwlknref  27840  frgr3v  28046  numclwlk1lem1  28140  disjunsn  30336  bnj594  32177  subfaclefac  32416  isbasisrelowllem1  34628  isbasisrelowllem2  34629  inixp  34995  opideq  35592  cdlemg33b  37835  eelT11  41031  uunT11  41120  uunT11p1  41121  uunT11p2  41122  uun111  41129