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  4174  2reu4lem  4469  opcom  5439  poirr  5534  asymref2  6063  xp11  6122  fununi  6556  brprcneu  6812  brprcneuALT  6813  f13dfv  7208  erinxp  8715  dom2lem  8914  pssnn  9078  djuinf  10080  dmaddpi  10781  dmmulpi  10782  gcddvds  16414  iscatd2  17587  dfiso2  17679  isnsg2  19068  eqger  19090  gaorber  19220  efgcpbllemb  19667  xmeter  24348  caucfil  25210  tgcgr4  28509  axcontlem5  28946  cplgr3v  29413  erclwwlkref  30000  clwwlkn2  30024  erclwwlknref  30049  frgr3v  30255  numclwlk1lem1  30349  disjunsn  32574  bnj594  34924  subfaclefac  35220  isbasisrelowllem1  37399  isbasisrelowllem2  37400  inixp  37778  opideq  38385  cdlemg33b  40816  eelT11  44809  uunT11  44898  uunT11p1  44899  uunT11p2  44900  uun111  44907