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  1572  falanfal  1575  nic-axALT  1673  inidm  4226  2reu4lem  4521  opcom  5505  poirr  5603  asymref2  6136  xp11  6194  fununi  6640  brprcneu  6895  brprcneuALT  6896  f13dfv  7295  erinxp  8832  dom2lem  9033  pssnn  9209  djuinf  10230  dmaddpi  10931  dmmulpi  10932  gcddvds  16541  iscatd2  17725  dfiso2  17817  isnsg2  19175  eqger  19197  gaorber  19327  efgcpbllemb  19774  xmeter  24444  caucfil  25318  tgcgr4  28540  axcontlem5  28984  cplgr3v  29453  erclwwlkref  30040  clwwlkn2  30064  erclwwlknref  30089  frgr3v  30295  numclwlk1lem1  30389  disjunsn  32608  bnj594  34927  subfaclefac  35182  isbasisrelowllem1  37357  isbasisrelowllem2  37358  inixp  37736  opideq  38345  cdlemg33b  40710  eelT11  44732  uunT11  44821  uunT11p1  44822  uunT11p2  44823  uun111  44830