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  1573  falanfal  1576  nic-axALT  1674  inidm  4178  2reu4lem  4473  opcom  5444  poirr  5539  asymref2  6066  xp11  6124  fununi  6557  brprcneu  6812  brprcneuALT  6813  f13dfv  7211  erinxp  8718  dom2lem  8917  pssnn  9082  djuinf  10083  dmaddpi  10784  dmmulpi  10785  gcddvds  16414  iscatd2  17587  dfiso2  17679  isnsg2  19035  eqger  19057  gaorber  19187  efgcpbllemb  19634  xmeter  24319  caucfil  25181  tgcgr4  28476  axcontlem5  28913  cplgr3v  29380  erclwwlkref  29964  clwwlkn2  29988  erclwwlknref  30013  frgr3v  30219  numclwlk1lem1  30313  disjunsn  32538  bnj594  34885  subfaclefac  35159  isbasisrelowllem1  37339  isbasisrelowllem2  37340  inixp  37718  opideq  38321  cdlemg33b  40696  eelT11  44690  uunT11  44779  uunT11p1  44780  uunT11p2  44781  uun111  44788