Theorem anidm 569

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anidmdbi  570  anandi  682  anandir  683  3anidm  1109  truantru  1580  falanfal  1583  nic-axALT  1681  inidm  4155  2reu4lem  4451  opcom  5442  poirr  5538  asymref2  6067  xp11  6126  fununi  6560  brprcneu  6817  brprcneuALT  6818  f13dfv  7218  erinxp  8728  dom2lem  8929  pssnn  9093  djuinf  10102  dmaddpi  10804  dmmulpi  10805  gcddvds  16463  iscatd2  17638  dfiso2  17730  isnsg2  19122  eqger  19144  gaorber  19274  efgcpbllemb  19721  xmeter  24416  caucfil  25268  tgcgr4  28617  axcontlem5  29055  cplgr3v  29522  erclwwlkref  30108  clwwlkn2  30132  erclwwlknref  30157  frgr3v  30363  numclwlk1lem1  30457  disjunsn  32683  bnj594  35094  subfaclefac  35404  isbasisrelowllem1  37717  isbasisrelowllem2  37718  inixp  38095  opideq  38710  cdlemg33b  41199  eelT11  45150  uunT11  45239  uunT11p1  45240  uunT11p2  45241  uun111  45248