MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anidm Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm4.24 553 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 214 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator