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  4179  2reu4lem  4486  opcom  5486  poirr  5583  asymref2  6119  xp11  6175  fununi  6615  brprcneu  6875  brprcneuALT  6876  f13dfv  7281  erinxp  8795  dom2lem  8995  pssnn  9160  djuinf  10188  dmaddpi  10894  dmmulpi  10895  gcddvds  16587  iscatd2  17763  dfiso2  17855  isnsg2  19270  eqger  19294  gaorber  19426  efgcpbllemb  19873  xmeter  24645  caucfil  25497  tgcgr4  28855  axcontlem5  29377  cplgr3v  29847  erclwwlkref  30442  clwwlkn2  30466  erclwwlknref  30491  frgr3v  30701  numclwlk1lem1  30795  disjunsn  33014  bnj594  35369  subfaclefac  35709  isbasisrelowllem1  38062  isbasisrelowllem2  38063  inixp  38441  opideq  39054  cdlemg33b  41543  eelT11  45492  uunT11  45581  uunT11p1  45582  uunT11p2  45583  uun111  45590