Theorem anidm 572

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anidmdbi  573  anandi  686  anandir  687  3anidm  1117  truantru  1594  falanfal  1597  nic-axALT  1695  inidm  4179  2reu4lem  4478  opcom  5471  poirr  5568  asymref2  6105  xp11  6162  fununi  6597  brprcneu  6858  brprcneuALT  6859  f13dfv  7259  erinxp  8774  dom2lem  8974  pssnn  9138  djuinf  10146  dmaddpi  10849  dmmulpi  10850  gcddvds  16538  iscatd2  17714  dfiso2  17806  isnsg2  19198  eqger  19220  gaorber  19349  efgcpbllemb  19796  xmeter  24494  caucfil  25346  tgcgr4  28701  axcontlem5  29170  cplgr3v  29637  erclwwlkref  30223  clwwlkn2  30247  erclwwlknref  30272  frgr3v  30478  numclwlk1lem1  30572  disjunsn  32795  bnj594  35208  subfaclefac  35527  isbasisrelowllem1  37850  isbasisrelowllem2  37851  inixp  38228  opideq  38843  cdlemg33b  41332  eelT11  45283  uunT11  45372  uunT11p1  45373  uunT11p2  45374  uun111  45381