Theorem anidm 566

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 565	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 223	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anidmdbi  567  anandi  675  anandir  676  3anidm  1105  truantru  1575  falanfal  1578  nic-axALT  1677  inidm  4219  2reu4lem  4526  opcom  5502  poirr  5601  asymref2  6119  xp11  6175  fununi  6624  brprcneu  6882  brprcneuALT  6883  f13dfv  7272  erinxp  8785  dom2lem  8988  pssnn  9168  pssnnOLD  9265  djuinf  10183  dmaddpi  10885  dmmulpi  10886  gcddvds  16444  iscatd2  17625  dfiso2  17719  isnsg2  19036  eqger  19058  gaorber  19172  efgcpbllemb  19623  xmeter  23939  caucfil  24800  tgcgr4  27782  axcontlem5  28226  cplgr3v  28692  erclwwlkref  29273  clwwlkn2  29297  erclwwlknref  29322  frgr3v  29528  numclwlk1lem1  29622  disjunsn  31825  bnj594  33923  subfaclefac  34167  isbasisrelowllem1  36236  isbasisrelowllem2  36237  inixp  36596  opideq  37212  cdlemg33b  39578  eelT11  43468  uunT11  43557  uunT11p1  43558  uunT11p2  43559  uun111  43566