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

Theorem anidm 568
 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 567 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 227 1 ((𝜑𝜑) ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ 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 210  df-an 400 This theorem is referenced by:  anidmdbi  569  anandi  675  anandir  676  3anidm  1101  truantru  1571  falanfal  1574  nic-axALT  1676  inidm  4145  2reu4lem  4423  opcom  5357  poirr  5450  asymref2  5945  xp11  6000  fununi  6402  brprcneu  6641  fvprc  6642  f13dfv  7014  erinxp  8361  dom2lem  8539  pssnn  8727  djuinf  9606  dmaddpi  10308  dmmulpi  10309  gcddvds  15849  iscatd2  16951  dfiso2  17041  isnsg2  18308  eqger  18330  gaorber  18438  efgcpbllemb  18881  xmeter  23054  caucfil  23901  tgcgr4  26339  axcontlem5  26776  cplgr3v  27239  erclwwlkref  27819  clwwlkn2  27843  erclwwlknref  27868  frgr3v  28074  numclwlk1lem1  28168  disjunsn  30371  bnj594  32330  subfaclefac  32572  isbasisrelowllem1  34812  isbasisrelowllem2  34813  inixp  35206  opideq  35800  cdlemg33b  38043  eelT11  41477  uunT11  41566  uunT11p1  41567  uunT11p2  41568  uun111  41575
 Copyright terms: Public domain W3C validator