Theorem anidm 554

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

Syntax hints:   ↔ wb 196   ∧ wa 382

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 383

This theorem is referenced by:  anidmdbi  555  anandi  655  anandir  656  nannot  1601  truantru  1654  falanfal  1657  nic-axALT  1747  inidm  3971  opcom  5092  opeqsnOLD  5096  poirr  5181  asymref2  5654  xp11  5710  fununi  6104  brprcneu  6325  f13dfv  6673  erinxp  7973  dom2lem  8149  pssnn  8334  dmaddpi  9914  dmmulpi  9915  gcddvds  15433  iscatd2  16549  dfiso2  16639  isnsg2  17832  eqger  17852  gaorber  17948  efgcpbllemb  18375  xmeter  22458  caucfil  23300  tgcgr4  25647  axcontlem5  26069  cplgr3v  26566  erclwwlkref  27170  clwwlkn2  27200  erclwwlknref  27227  frgr3v  27457  numclwlk1lem1  27560  disjunsn  29745  bnj594  31320  subfaclefac  31496  isbasisrelowllem1  33540  isbasisrelowllem2  33541  inixp  33855  opideq  34452  cdlemg33b  36516  eelT11  39457  uunT11  39548  uunT11p1  39549  uunT11p2  39550  uun111  39557  2reu4a  41709