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

Theorem anidm 560
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 559 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 215 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  anidmdbi  561  anandi  666  anandir  667  nannotOLD  1619  truantru  1686  falanfal  1689  nic-axALT  1769  inidm  3984  opcom  5122  opeqsnOLD  5126  poirr  5211  asymref2  5698  xp11  5754  fununi  6144  brprcneu  6371  f13dfv  6726  erinxp  8028  dom2lem  8204  pssnn  8389  dmaddpi  9969  dmmulpi  9970  gcddvds  15520  iscatd2  16621  dfiso2  16711  isnsg2  17902  eqger  17922  gaorber  18018  efgcpbllemb  18448  xmeter  22531  caucfil  23374  tgcgr4  25731  axcontlem5  26153  cplgr3v  26636  erclwwlkref  27274  clwwlkn2  27305  erclwwlknref  27339  frgr3v  27576  numclwlk1lem1  27694  disjunsn  29876  bnj594  31451  subfaclefac  31627  isbasisrelowllem1  33657  isbasisrelowllem2  33658  inixp  33967  opideq  34561  cdlemg33b  36684  eelT11  39618  uunT11  39708  uunT11p1  39709  uunT11p2  39710  uun111  39717  2reu4a  41884
  Copyright terms: Public domain W3C validator