Theorem anidm 566

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  anidmdbi  567  anandi  674  anandir  675  3anidm  1104  truantru  1572  falanfal  1575  nic-axALT  1674  inidm  4158  2reu4lem  4462  opcom  5428  poirr  5526  asymref2  6037  xp11  6093  fununi  6538  brprcneu  6794  brprcneuALT  6795  f13dfv  7178  erinxp  8611  dom2lem  8813  pssnn  8989  pssnnOLD  9084  djuinf  9990  dmaddpi  10692  dmmulpi  10693  gcddvds  16255  iscatd2  17435  dfiso2  17529  isnsg2  18829  eqger  18851  gaorber  18959  efgcpbllemb  19406  xmeter  23631  caucfil  24492  tgcgr4  26937  axcontlem5  27381  cplgr3v  27847  erclwwlkref  28429  clwwlkn2  28453  erclwwlknref  28478  frgr3v  28684  numclwlk1lem1  28778  disjunsn  30978  bnj594  32937  subfaclefac  33183  isbasisrelowllem1  35570  isbasisrelowllem2  35571  inixp  35930  opideq  36520  cdlemg33b  38763  eelT11  42365  uunT11  42454  uunT11p1  42455  uunT11p2  42456  uun111  42463