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  674  anandir  675  3anidm  1104  truantru  1574  falanfal  1577  nic-axALT  1676  inidm  4217  2reu4lem  4524  opcom  5500  poirr  5599  asymref2  6115  xp11  6171  fununi  6620  brprcneu  6878  brprcneuALT  6879  f13dfv  7268  erinxp  8781  dom2lem  8984  pssnn  9164  pssnnOLD  9261  djuinf  10179  dmaddpi  10881  dmmulpi  10882  gcddvds  16440  iscatd2  17621  dfiso2  17715  isnsg2  19030  eqger  19052  gaorber  19166  efgcpbllemb  19617  xmeter  23930  caucfil  24791  tgcgr4  27771  axcontlem5  28215  cplgr3v  28681  erclwwlkref  29262  clwwlkn2  29286  erclwwlknref  29311  frgr3v  29517  numclwlk1lem1  29611  disjunsn  31812  bnj594  33911  subfaclefac  34155  isbasisrelowllem1  36224  isbasisrelowllem2  36225  inixp  36584  opideq  37200  cdlemg33b  39566  eelT11  43453  uunT11  43542  uunT11p1  43543  uunT11p2  43544  uun111  43551