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  675  anandir  676  3anidm  1104  truantru  1570  falanfal  1573  nic-axALT  1672  inidm  4248  2reu4lem  4545  opcom  5520  poirr  5620  asymref2  6149  xp11  6206  fununi  6653  brprcneu  6910  brprcneuALT  6911  f13dfv  7310  erinxp  8849  dom2lem  9052  pssnn  9234  djuinf  10258  dmaddpi  10959  dmmulpi  10960  gcddvds  16549  iscatd2  17739  dfiso2  17833  isnsg2  19196  eqger  19218  gaorber  19348  efgcpbllemb  19797  xmeter  24464  caucfil  25336  tgcgr4  28557  axcontlem5  29001  cplgr3v  29470  erclwwlkref  30052  clwwlkn2  30076  erclwwlknref  30101  frgr3v  30307  numclwlk1lem1  30401  disjunsn  32616  bnj594  34888  subfaclefac  35144  isbasisrelowllem1  37321  isbasisrelowllem2  37322  inixp  37688  opideq  38299  cdlemg33b  40664  eelT11  44678  uunT11  44767  uunT11p1  44768  uunT11p2  44769  uun111  44776