Theorem anidm 574

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anidmdbi  575  anandi  688  anandir  689  3anidm  1121  truantru  1603  falanfal  1606  nic-axALT  1704  inidm  4179  2reu4lem  4484  opcom  5484  poirr  5581  asymref2  6117  xp11  6173  fununi  6611  brprcneu  6871  brprcneuALT  6872  f13dfv  7272  erinxp  8785  dom2lem  8985  pssnn  9149  djuinf  10168  dmaddpi  10870  dmmulpi  10871  gcddvds  16556  iscatd2  17732  dfiso2  17824  isnsg2  19217  eqger  19241  gaorber  19373  efgcpbllemb  19820  xmeter  24590  caucfil  25442  tgcgr4  28800  axcontlem5  29318  cplgr3v  29785  erclwwlkref  30371  clwwlkn2  30395  erclwwlknref  30420  frgr3v  30626  numclwlk1lem1  30720  disjunsn  32939  bnj594  35300  subfaclefac  35668  isbasisrelowllem1  38021  isbasisrelowllem2  38022  inixp  38399  opideq  39012  cdlemg33b  41501  eelT11  45435  uunT11  45524  uunT11p1  45525  uunT11p2  45526  uun111  45533