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  677  anandir  678  3anidm  1104  truantru  1575  falanfal  1578  nic-axALT  1676  inidm  4167  2reu4lem  4463  opcom  5455  poirr  5551  asymref2  6080  xp11  6139  fununi  6573  brprcneu  6830  brprcneuALT  6831  f13dfv  7229  erinxp  8738  dom2lem  8939  pssnn  9103  djuinf  10111  dmaddpi  10813  dmmulpi  10814  gcddvds  16472  iscatd2  17647  dfiso2  17739  isnsg2  19131  eqger  19153  gaorber  19283  efgcpbllemb  19730  xmeter  24398  caucfil  25250  tgcgr4  28599  axcontlem5  29037  cplgr3v  29504  erclwwlkref  30090  clwwlkn2  30114  erclwwlknref  30139  frgr3v  30345  numclwlk1lem1  30439  disjunsn  32664  bnj594  35054  subfaclefac  35358  isbasisrelowllem1  37671  isbasisrelowllem2  37672  inixp  38049  opideq  38664  cdlemg33b  41153  eelT11  45133  uunT11  45222  uunT11p1  45223  uunT11p2  45224  uun111  45231