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  677  anandir  678  3anidm  1104  truantru  1575  falanfal  1578  nic-axALT  1676  inidm  4168  2reu4lem  4464  opcom  5450  poirr  5545  asymref2  6075  xp11  6134  fununi  6568  brprcneu  6825  brprcneuALT  6826  f13dfv  7223  erinxp  8732  dom2lem  8933  pssnn  9097  djuinf  10105  dmaddpi  10807  dmmulpi  10808  gcddvds  16466  iscatd2  17641  dfiso2  17733  isnsg2  19125  eqger  19147  gaorber  19277  efgcpbllemb  19724  xmeter  24411  caucfil  25263  tgcgr4  28616  axcontlem5  29054  cplgr3v  29521  erclwwlkref  30108  clwwlkn2  30132  erclwwlknref  30157  frgr3v  30363  numclwlk1lem1  30457  disjunsn  32682  bnj594  35073  subfaclefac  35377  isbasisrelowllem1  37688  isbasisrelowllem2  37689  inixp  38066  opideq  38681  cdlemg33b  41170  eelT11  45154  uunT11  45243  uunT11p1  45244  uunT11p2  45245  uun111  45252