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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anidmdbi  565  anandi  672  anandir  673  3anidm  1102  truantru  1574  falanfal  1577  nic-axALT  1680  inidm  4157  2reu4lem  4461  opcom  5417  poirr  5514  asymref2  6019  xp11  6075  fununi  6505  brprcneu  6759  fvprc  6760  f13dfv  7140  erinxp  8554  dom2lem  8751  pssnn  8916  pssnnOLD  9001  djuinf  9928  dmaddpi  10630  dmmulpi  10631  gcddvds  16191  iscatd2  17371  dfiso2  17465  isnsg2  18765  eqger  18787  gaorber  18895  efgcpbllemb  19342  xmeter  23567  caucfil  24428  tgcgr4  26873  axcontlem5  27317  cplgr3v  27783  erclwwlkref  28363  clwwlkn2  28387  erclwwlknref  28412  frgr3v  28618  numclwlk1lem1  28712  disjunsn  30912  bnj594  32871  subfaclefac  33117  isbasisrelowllem1  35505  isbasisrelowllem2  35506  inixp  35865  opideq  36457  cdlemg33b  38700  eelT11  42280  uunT11  42369  uunT11p1  42370  uunT11p2  42371  uun111  42378