Theorem anidm 575

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anidmdbi  576  anandi  689  anandir  690  3anidm  1121  truantru  1603  falanfal  1606  nic-axALT  1707  inidm  4182  2reu4lem  4489  opcom  5489  poirr  5586  asymref2  6122  xp11  6178  fununi  6618  brprcneu  6878  brprcneuALT  6879  f13dfv  7283  erinxp  8798  dom2lem  8998  pssnn  9163  djuinf  10191  dmaddpi  10893  dmmulpi  10894  gcddvds  16586  iscatd2  17762  dfiso2  17854  isnsg2  19247  eqger  19271  gaorber  19403  efgcpbllemb  19850  xmeter  24620  caucfil  25472  tgcgr4  28830  axcontlem5  29348  cplgr3v  29815  erclwwlkref  30401  clwwlkn2  30425  erclwwlknref  30450  frgr3v  30656  numclwlk1lem1  30750  disjunsn  32969  bnj594  35324  subfaclefac  35681  isbasisrelowllem1  38034  isbasisrelowllem2  38035  inixp  38412  opideq  39025  cdlemg33b  41514  eelT11  45448  uunT11  45537  uunT11p1  45538  uunT11p2  45539  uun111  45546