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  1100  truantru  1570  falanfal  1573  nic-axALT  1675  inidm  4195  2reu4lem  4465  opcom  5391  poirr  5485  asymref2  5977  xp11  6032  fununi  6429  brprcneu  6662  f13dfv  7031  erinxp  8371  dom2lem  8549  pssnn  8736  djuinf  9614  dmaddpi  10312  dmmulpi  10313  gcddvds  15852  iscatd2  16952  dfiso2  17042  isnsg2  18308  eqger  18330  gaorber  18438  efgcpbllemb  18881  xmeter  23043  caucfil  23886  tgcgr4  26317  axcontlem5  26754  cplgr3v  27217  erclwwlkref  27798  clwwlkn2  27822  erclwwlknref  27848  frgr3v  28054  numclwlk1lem1  28148  disjunsn  30344  bnj594  32184  subfaclefac  32423  isbasisrelowllem1  34639  isbasisrelowllem2  34640  inixp  35018  opideq  35615  cdlemg33b  37858  eelT11  41061  uunT11  41150  uunT11p1  41151  uunT11p2  41152  uun111  41159