Theorem anidm 574

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anidmdbi  575  anandi  688  anandir  689  3anidm  1119  truantru  1600  falanfal  1603  nic-axALT  1701  inidm  4187  2reu4lem  4489  opcom  5485  poirr  5582  asymref2  6118  xp11  6174  fununi  6612  brprcneu  6872  brprcneuALT  6873  f13dfv  7273  erinxp  8789  dom2lem  8989  pssnn  9153  djuinf  10172  dmaddpi  10875  dmmulpi  10876  gcddvds  16561  iscatd2  17737  dfiso2  17829  isnsg2  19222  eqger  19246  gaorber  19378  efgcpbllemb  19825  xmeter  24559  caucfil  25411  tgcgr4  28766  axcontlem5  29259  cplgr3v  29726  erclwwlkref  30312  clwwlkn2  30336  erclwwlknref  30361  frgr3v  30567  numclwlk1lem1  30661  disjunsn  32880  bnj594  35245  subfaclefac  35601  isbasisrelowllem1  37923  isbasisrelowllem2  37924  inixp  38301  opideq  38916  cdlemg33b  41405  eelT11  45341  uunT11  45430  uunT11p1  45431  uunT11p2  45432  uun111  45439