Theorem anidm 564

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidmdbi  565  anandi  676  anandir  677  3anidm  1103  truantru  1574  falanfal  1577  nic-axALT  1675  inidm  4179  2reu4lem  4476  opcom  5449  poirr  5544  asymref2  6074  xp11  6133  fununi  6567  brprcneu  6824  brprcneuALT  6825  f13dfv  7220  erinxp  8730  dom2lem  8931  pssnn  9095  djuinf  10101  dmaddpi  10803  dmmulpi  10804  gcddvds  16432  iscatd2  17606  dfiso2  17698  isnsg2  19087  eqger  19109  gaorber  19239  efgcpbllemb  19686  xmeter  24379  caucfil  25241  tgcgr4  28605  axcontlem5  29043  cplgr3v  29510  erclwwlkref  30097  clwwlkn2  30121  erclwwlknref  30146  frgr3v  30352  numclwlk1lem1  30446  disjunsn  32671  bnj594  35070  subfaclefac  35372  isbasisrelowllem1  37562  isbasisrelowllem2  37563  inixp  37931  opideq  38541  cdlemg33b  40989  eelT11  44968  uunT11  45057  uunT11p1  45058  uunT11p2  45059  uun111  45066