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  4172  2reu4lem  4479  opcom  5478  poirr  5575  asymref2  6111  xp11  6168  fununi  6609  brprcneu  6869  brprcneuALT  6870  f13dfv  7276  erinxp  8794  dom2lem  9001  pssnn  9166  djuinf  10194  dmaddpi  10902  dmmulpi  10903  gcddvds  16596  iscatd2  17772  dfiso2  17864  isnsg2  19282  eqger  19306  gaorber  19438  efgcpbllemb  19885  xmeter  24662  caucfil  25514  tgcgr4  28876  axcontlem5  29428  cplgr3v  29898  erclwwlkref  30493  clwwlkn2  30517  erclwwlknref  30542  frgr3v  30758  numclwlk1lem1  30852  disjunsn  33070  bnj594  35424  subfaclefac  35758  isbasisrelowllem1  38112  isbasisrelowllem2  38113  inixp  38481  opideq  39094  cdlemg33b  41583  eelT11  45532  uunT11  45621  uunT11p1  45622  uunT11p2  45623  uun111  45630