MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anidms Unicode version

Theorem anidms 645
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1
Assertion
Ref Expression
anidms

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3
21ex 434 . 2
32pm2.43i 47 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sylancb  665  sylancbr  666  dedth2v  3997  dedth3v  3998  dedth4v  3999  intsng  4322  pwnss  4617  snex  4693  isso2i  4837  posn  5073  xpid11  5229  f1oprswap  5860  f1o2sn  6074  residpr  6075  f1mpt  6169  f1eqcocnv  6204  isopolem  6241  3xpexg  6603  sqxpexg  6605  poxp  6912  oe0  7191  oecl  7206  nnmsucr  7293  ecopover  7434  enrefg  7567  php  7721  3xpfi  7812  dffi3  7911  infxpenlem  8412  xp2cda  8581  isfin5-2  8792  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  pwfseqlem5  9062  pwfseq  9063  nqereu  9328  halfnq  9375  ltsopr  9431  1idsr  9496  00sr  9497  sqgt0sr  9504  leid  9701  msqgt0  10098  msqge0  10099  recextlem1  10204  recextlem2  10205  recex  10206  div1  10261  cju  10557  2halves  10792  msqznn  10969  uzindOLD  10982  xrltnr  11359  xrleid  11385  iccid  11603  expubnd  12226  sqneg  12228  sqcl  12230  nnsqcl  12237  qsqcl  12239  subsq2  12276  bernneq  12292  faclbnd  12368  faclbnd3  12370  hashfac  12507  leiso  12508  cjmulval  12978  sin2t  13912  cos2t  13913  divalglem0  14051  divalglem2  14053  gcd0id  14161  isprm5  14253  prslem  15560  pslem  15836  dirref  15865  sgrp2nmndlem4  16046  grpsubid  16122  cntzi  16367  symgval  16404  symgbas  16405  symgbasfi  16411  symg1bas  16421  pgrpsubgsymg  16433  symgextfve  16444  pmtrfinv  16486  psgnsn  16545  lsmidm  16682  ipeq0  18673  matsca2  18922  matbas2  18923  matplusgcell  18935  matsubgcell  18936  mamulid  18943  mamurid  18944  mattposcl  18955  mat1dimelbas  18973  mat1dimscm  18977  m1detdiag  19099  mdetdiagid  19102  mdetunilem9  19122  pmatcoe1fsupp  19202  d1mat2pmat  19240  idcn  19758  hausdiag  20146  symgtgp  20600  ustref  20721  ustelimasn  20725  iducn  20786  ismet  20826  isxmet  20827  idnghm  21250  resubmet  21307  xrsxmet  21314  cphnm  21640  tchnmval  21672  ipcau2  21677  tchcphlem1  21678  tchcphlem2  21679  tchcph  21680  chordthmlem  23163  ismot  23922  is2wlkonot  24863  is2spthonot  24864  resgrprn  25282  ismgmOLD  25322  opidon2OLD  25326  rngo2  25390  vcoprnelem  25471  hmoval  25725  htth  25835  hvsubid  25943  hvnegid  25944  hv2times  25978  hiidrcl  26012  normval  26041  issh2  26126  chjidm  26438  normcan  26494  ho2times  26738  kbpj  26875  lnop0  26885  riesz3i  26981  leoprf  27047  leopsq  27048  cvnref  27210  gtiso  27519  prsss  27898  deranglem  28610  m1expevenALT  28663  fallrisefac  29147  dfpo2  29184  predpoirr  29277  predfrirr  29278  elfix2  29554  linedegen  29793  ftc1anclem3  30092  filnetlem2  30197  prdsbnd2  30291  reheibor  30335  exidreslem  30339  mzpf  30668  acongrep  30918  ttac  30978  mendval  31132  mendplusgfval  31134  mendmulrfval  31136  iocinico  31179  iocmbl  31180  seff  31189  sblpnf  31190  lcmid  31215  lcmgcdeq  31216  sigarid  32075  cnambpcma  32315  2leaddle2  32320  clintopval  32528  bj-ru0  34500
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 185  df-an 371
  Copyright terms: Public domain W3C validator