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  28480  axcontlem5  28917  cplgr3v  29384  erclwwlkref  29968  clwwlkn2  29992  erclwwlknref  30017  frgr3v  30223  numclwlk1lem1  30317  disjunsn  32543  bnj594  34895  subfaclefac  35169  isbasisrelowllem1  37349  isbasisrelowllem2  37350  inixp  37728  opideq  38331  cdlemg33b  40706  eelT11  44700  uunT11  44789  uunT11p1  44790  uunT11p2  44791  uun111  44798