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  1574  falanfal  1577  nic-axALT  1675  inidm  4177  2reu4lem  4474  opcom  5447  poirr  5542  asymref2  6072  xp11  6131  fununi  6565  brprcneu  6822  brprcneuALT  6823  f13dfv  7218  erinxp  8726  dom2lem  8927  pssnn  9091  djuinf  10097  dmaddpi  10799  dmmulpi  10800  gcddvds  16428  iscatd2  17602  dfiso2  17694  isnsg2  19083  eqger  19105  gaorber  19235  efgcpbllemb  19682  xmeter  24375  caucfil  25237  tgcgr4  28552  axcontlem5  28990  cplgr3v  29457  erclwwlkref  30044  clwwlkn2  30068  erclwwlknref  30093  frgr3v  30299  numclwlk1lem1  30393  disjunsn  32618  bnj594  35017  subfaclefac  35319  isbasisrelowllem1  37499  isbasisrelowllem2  37500  inixp  37868  opideq  38475  cdlemg33b  40906  eelT11  44889  uunT11  44978  uunT11p1  44979  uunT11p2  44980  uun111  44987