Theorem anidm 676

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anidmdbi  678  anandi  871  anandir  872  nannot  1453  truantru  1506  falanfal  1509  nic-axALT  1599  inidm  3822  opcom  4965  opeqsn  4967  poirr  5046  asymref2  5513  xp11  5569  fununi  5964  brprcneu  6184  f13dfv  6530  erinxp  7821  dom2lem  7995  pssnn  8178  dmaddpi  9712  dmmulpi  9713  gcddvds  15225  iscatd2  16342  dfiso2  16432  isnsg2  17624  eqger  17644  gaorber  17741  efgcpbllemb  18168  xmeter  22238  caucfil  23081  tgcgr4  25426  axcontlem5  25848  cplgr3v  26331  clwwlksn2  26910  erclwwlksref  26934  erclwwlksnref  26946  frgr3v  27139  disjunsn  29407  bnj594  30982  subfaclefac  31158  isbasisrelowllem1  33203  isbasisrelowllem2  33204  inixp  33523  cdlemg33b  35995  eelT11  38932  uunT11  39023  uunT11p1  39024  uunT11p2  39025  uun111  39032  2reu4a  41189