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

Theorem breq1d 4371
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breq1d  |-  ( ph  ->  ( A R C  <-> 
B R C ) )

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq1 4364 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 17 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   class class class wbr 4361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4362
This theorem is referenced by:  eqbrtrd  4382  syl6eqbr  4399  sbcbr2g  4417  pofun  4728  dffv2  5893  fmptco  6010  isorel  6171  soisores  6172  soisoi  6173  isocnv  6175  isotr  6181  f1owe  6198  weniso  6199  caovordig  6427  caovordg  6429  caovord  6433  f1oweALT  6730  frxp  6856  xporderlem  6857  fnwelem  6861  reldmtpos  6931  brtpos  6932  tpostpos  6943  tposoprab  6959  ensn1g  7583  fndmeng  7595  xpsneng  7605  xpcomco  7610  pwdom  7672  snnen2o  7709  supgtoreq  7934  ordtypelem6  7986  ordtypelem7  7987  wdompwdom  8041  infdiffi  8110  r1sdom  8192  pm54.43  8381  prdom2  8384  indcardi  8418  alephordi  8451  cdalepw  8572  fin23lem26  8701  fin23lem23  8702  fin23lem22  8703  fin23lem27  8704  uniimadomf  8916  alephval2  8943  inar1  9146  nqereu  9300  ltrnq  9350  prlem934  9404  prlem936  9418  ltasr  9470  addgt0sr  9474  axpre-ltadd  9537  axpre-sup  9539  ltsubadd  10030  lesubadd  10032  ltaddsub2  10035  leaddsub2  10037  ltaddpos  10050  lesub2  10055  ltnegcon2  10062  lenegcon2  10065  addge01  10070  subge0  10073  suble0  10074  lesub0  10077  ltordlem  10085  mulgt1  10410  ltmulgt11  10411  gt0div  10417  ge0div  10418  ltmuldiv  10424  ltmuldiv2  10425  lemuldiv2  10433  ltrec  10434  lerec2  10440  ltdiv23  10443  lediv23  10444  addltmul  10794  avglt1  10796  avgle1  10798  avgle  10800  zlem1lt  10934  zgt0ge1  10936  rpnnen1lem5  11240  reexALT  11242  xrmin2  11419  xltnegi  11455  xmulval  11464  xlesubadd  11495  xmullem2  11497  nn0disj  11853  dfceil2  12013  uzenom  12123  seqf1olem1  12197  leexp2r  12275  sqlecan  12326  expmulnbnd  12349  hashbnd  12466  hashle00  12522  hashgt12el2  12539  hashf1  12563  seqcoll  12570  hashge3el3dif  12585  swrdccatin2  12784  swrd2lsw  12966  2swrd2eqwrdeq  12967  shftfval  13072  shftfib  13074  shftfn  13075  2shfti  13082  shftidt2  13083  sqrlem1  13245  sqrlem2  13246  sqrlem6  13250  sqrlem7  13251  absdiflt  13319  absdifle  13320  lenegsq  13322  cau3lem  13356  limsupgle  13473  limsupgre  13480  limsupgreOLD  13481  clim  13496  rlim  13497  rlim2  13498  clim2  13506  clim0  13508  clim0c  13509  rlim0  13510  rlim0lt  13511  climi0  13514  ello1  13517  ello1mpt  13523  elo1  13528  lo1o1  13534  rlimclim1  13547  rlimclim  13548  climrlim2  13549  rlimuni  13552  climuni  13554  lo1res  13561  rlimresb  13567  rlimeq  13571  2clim  13574  climshftlem  13576  climshft  13578  climabs0  13587  o1co  13588  rlimcn1  13590  rlimcn2  13592  climcn1  13593  climcn2  13594  addcn2  13595  subcn2  13596  mulcn2  13597  o1of2  13614  o1rlimmul  13620  rlimdiv  13647  rlimno1  13655  isershft  13665  isercoll  13669  climsup  13671  climcau  13672  caucvgrlem  13674  caucvgrlemOLD  13675  caucvgrlem2  13678  caurcvg2  13682  caucvg  13683  caucvgb  13684  serf0  13685  iseraltlem2  13687  iseralt  13689  sumeq1  13693  sumeq2w  13696  sumeq2ii  13697  sumrb  13717  summolem2  13720  summo  13721  zsum  13722  o1fsum  13811  cvgcmp  13814  cvgcmpce  13816  isumshft  13835  climcndslem1  13845  geolim  13864  geolim2  13865  geoisum1c  13874  mertenslem1  13878  mertenslem2  13879  mertens  13880  ntrivcvg  13891  ntrivcvgn0  13892  ntrivcvgmullem  13895  prodeq1f  13900  prodeq2w  13904  prodeq2ii  13905  prodrblem2  13923  prodmolem2  13927  prodmo  13928  zprod  13929  fprodntriv  13934  sin01bnd  14177  cos01bnd  14178  rpnnen  14217  ruclem9  14228  ruclem12  14231  sadcaddlem  14369  gcddvds  14415  dvdssq  14466  lcmgcdlem  14509  lcmdvds  14511  lcmfunsnlem  14552  isprm  14562  isprm2lem  14569  prmgt1  14581  prmn2uzge3  14582  isprm5  14589  isprm6  14604  coprmproddvdslem  14617  coprmproddvds  14618  odzdvds  14678  odzdvdsOLD  14684  pclem  14726  pcprecl  14727  pcprendvds  14728  pcpremul  14731  pcval  14732  pceulem  14733  pczndvds  14752  pcelnn  14757  pc2dvds  14766  pcadd  14772  pcadd2  14773  pcmpt  14775  prmpwdvds  14786  prmreclem1  14798  prmreclem5  14802  prmreclem6  14803  4sqlem17OLD  14843  4sqlem17  14849  vdwlem10  14878  ramval  14898  ramvalOLD  14899  0ram  14916  ram0  14918  ramz2  14920  ramub1lem2  14923  imasaddfnlem  15372  imasvscafn  15381  imasleval  15385  mreexexlemd  15488  symggen  17049  oddvdsnn0  17131  oddvds  17134  odf1  17151  odf1o1  17159  odf1o2  17160  gexdvds  17173  sylow1lem3  17190  efginvrel2  17315  efgsfo  17327  efgredlemd  17332  efgredlem  17335  efgred  17336  gexexlem  17428  torsubg  17430  oddvdssubg  17431  lt6abl  17467  ablfacrplem  17636  ablfacrp  17637  ablfaclem3  17658  abvfval  17984  abvpropd  18008  evlslem2  18673  znf1o  19059  znidomb  19069  cygznlem1  19074  frlmup1  19293  islinds  19304  lindsss  19319  chfacfscmul0  19819  chfacfscmulfsupp  19820  chfacfpmmul0  19823  chfacfpmmulfsupp  19824  cayleyhamilton1  19853  cctop  19958  ordthmeolem  20753  csdfil  20846  ufilen  20882  ptcmplem2  21005  ptcmplem3  21006  cnextfvval  21017  prdsxmetlem  21320  blfvalps  21335  elblps  21339  elbl  21340  elbl3ps  21343  elbl3  21344  blres  21383  imasf1obl  21440  blcld  21457  comet  21465  stdbdmetval  21466  stdbdbl  21469  metcnp2  21494  txmetcnp  21499  dscopn  21525  ngptgp  21581  nlmvscn  21627  nrginvrcn  21631  nmoval  21657  nmovalOLD  21676  nghmcn  21703  cnbl0  21731  cnblcld  21732  bl2ioo  21747  recld2  21769  icccmplem2  21778  addcnlem  21833  divcn  21837  elcncf  21858  elcncf2  21859  cncfi  21863  rescncf  21866  mulc1cncf  21874  cncfco  21876  cncfmet  21877  cnheiborlem  21919  cnheibor  21920  cnllycmp  21921  evth  21924  htpycc  21948  phtpycc  21959  pcohtpylem  21987  pcoass  21992  pcorevlem  21994  nmoleub2lem2  22067  nmoleub3  22070  nmhmcn  22071  ipcau2  22145  ipcn  22154  lmmbr2  22166  lmmcvg  22168  lmmbrf  22169  fmcfil  22179  iscau2  22184  iscau4  22186  iscauf  22187  caucfil  22190  iscmet3lem3  22197  iscmet3lem1  22198  iscmet3lem2  22199  cfilresi  22202  cfilres  22203  caussi  22204  causs  22205  lmle  22208  lmclim  22209  bcthlem1  22229  bcthlem4  22232  bcth  22234  minveclem3b  22307  minveclem3  22308  minveclem4  22311  minveclem5  22312  minveclem7  22314  minveclem3bOLD  22319  minveclem3OLD  22320  minveclem4OLD  22323  minveclem5OLD  22324  minveclem7OLD  22326  pmltpclem1  22336  pmltpc  22338  ivthlem1  22339  ivthlem2  22340  ivthlem3  22341  ivth  22342  cniccbdd  22349  ovolunlem1  22387  ovoliunlem1  22392  ovoliunlem2  22393  ovoliunlem3  22394  ovolshftlem1  22399  ovolscalem1  22403  ovolicc1  22406  ovolicc2lem3  22409  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ovolicc2lem5  22412  ioombl1lem4  22451  ioombl1  22452  uniioombllem6  22483  volsup2  22500  volcn  22501  mbfmulc2lem  22540  mbfsup  22557  mbflimsup  22560  mbflimsupOLD  22561  itg1climres  22609  mbfi1fseqlem6  22615  mbfi1fseq  22616  mbfi1flimlem  22617  itg2leub  22629  itg2seq  22637  itg2mulclem  22641  itg2monolem1  22645  itg2mono  22648  itg2i1fseq  22650  itg2addlem  22653  itg2gt0  22655  itg2cnlem1  22656  itg2cnlem2  22657  itg2cn  22658  bddmulibl  22733  itgcn  22737  ellimc3  22771  dveflem  22868  dvferm1lem  22873  dvferm2lem  22875  rolle  22879  dvlip  22882  dvlipcn  22883  dvlip2  22884  c1liplem1  22885  c1lip3  22888  dvge0  22895  dvivthlem1  22897  lhop1lem  22902  lhop1  22903  dvcvx  22909  dvfsumabs  22912  dvfsumlem2  22916  dvfsumrlim  22920  ftc1a  22926  ftc1lem4  22928  ftc1lem6  22930  itgsubstlem  22937  mdegleb  22950  mdegmullem  22964  deg1lt0  22977  ply1divmo  23023  ply1divex  23024  ply1divalg2  23026  q1peqb  23042  fta1g  23055  dgrub  23125  coe1termlem  23149  dgrcolem2  23165  dgrco  23166  quotval  23182  plydivlem3  23185  plydivlem4  23186  plydivex  23187  plydivalg  23189  quotlem  23190  plyrem  23195  fta1  23198  aannenlem1  23221  aannenlem2  23222  aalioulem3  23227  aalioulem4  23228  aalioulem5  23229  aalioulem6  23230  aaliou  23231  aaliou2  23233  aaliou2b  23234  ulmval  23272  ulm2  23277  ulmclm  23279  ulmshftlem  23281  ulmcaulem  23286  ulmcau  23287  ulmss  23289  ulmcn  23291  ulmdvlem1  23292  ulmdvlem3  23294  mtestbdd  23297  iblulm  23299  itgulm  23300  radcnvlem1  23305  pserulm  23314  abelthlem2  23324  abelthlem5  23327  abelthlem7  23330  abelthlem8  23331  abelthlem9  23332  abelth  23333  pilem3  23346  pilem3OLD  23347  sincosq2sgn  23391  sincosq3sgn  23392  sincosq4sgn  23393  logltb  23486  logcnlem5  23528  cxpcn3lem  23624  cxpcn3  23625  cxpaddle  23629  logreclem  23636  rlimcnp  23828  rlimcnp2  23829  xrlimcnp  23831  rlimcxp  23836  cxploglim  23840  jensen  23851  emcllem6  23863  emcllem7  23864  lgamgulmlem2  23892  lgamgulmlem3  23893  lgamgulmlem5  23895  lgamgulmlem6  23896  lgambdd  23899  lgamucov  23900  lgamcvglem  23902  ftalem2  23935  ftalem3  23936  ftalem5  23938  ftalem5OLD  23940  sqfpc  24001  mumullem2  24044  sqff1o  24046  chtublem  24076  chtub  24077  fsumvma2  24079  chpchtsum  24084  logexprlim  24090  bposlem6  24154  lgslem2  24162  lgslem3  24163  lgsval  24165  lgsfcl2  24167  lgsfle1  24170  lgsle1  24176  lgsdirprm  24194  chtppilimlem2  24249  chtppilim  24250  dchrisumlema  24263  dchrisumlem1  24264  dchrisumlem2  24265  dchrisumlem3  24266  dchrisum  24267  dchrmusumlema  24268  dchrvmasumlem2  24273  dchrisum0flblem1  24283  dchrisum0lema  24289  2vmadivsumlem  24315  chpdifbndlem1  24328  selberg3lem1  24332  selberg4lem1  24335  pntrsumbnd  24341  pntrsumbnd2  24342  selbergsb  24350  pntrlog2bndlem3  24354  pntrlog2bndlem5  24356  pntrlog2bndlem6  24358  pntpbnd1  24361  pntpbnd2  24362  pntibndlem2  24366  pntibndlem3  24367  pntibnd  24368  pntlemn  24375  pntlemj  24378  pntlemi  24379  pntlemo  24382  pntlem3  24384  pntlemp  24385  pntleml  24386  pnt3  24387  padicabv  24405  ostth2lem2  24409  ostth3  24413  ostth  24414  mirbtwnhl  24662  foot  24701  footeq  24703  mideulem2  24713  opphllem6  24731  hpgbr  24739  lmieu  24763  inaghl  24818  brbtwn2  24872  colinearalg  24877  axcontlem10  24940  umgrale  24985  umgrafi  24986  umgra1  24990  uslgra1  25036  1pthoncl  25259  2pthoncl  25270  clwlkisclwwlk2  25455  0eusgraiff0rgra  25604  umgrabi  25648  frgrawopreglem2  25710  isnvlem  26166  nvelbl  26262  nvelbl2  26263  nmoofval  26340  nmosetn0  26343  nmoolb  26349  nmoubi  26350  nmounbseqi  26355  nmounbseqiALT  26356  nmobndseqi  26357  nmobndseqiALT  26358  bloval  26359  isblo  26360  nmoo0  26369  nmlno0lem  26371  blocnilem  26382  siilem2  26430  ubthlem1  26449  ubthlem2  26450  ubthlem3  26451  ubth  26452  minvecolem3  26455  minvecolem4  26459  minvecolem5  26460  minvecolem7  26462  minvecolem3OLD  26465  minvecolem4OLD  26469  minvecolem5OLD  26470  minvecolem7OLD  26472  htthlem  26507  htth  26508  h2hcau  26569  h2hlm  26570  normlem7tALT  26709  norm3lemt  26742  hcau  26774  hlimi  26778  hlim2  26782  cmcm3  27205  pjnorm  27314  pjnel  27316  elcnop  27447  elbdop  27450  nmopsetn0  27455  nmfnsetn0  27468  elcnfn  27472  hhcno  27494  hhcnf  27495  nmoplb  27497  nmopub  27498  cnopc  27503  nmfnlb  27514  nmfnleub  27515  cnfnc  27520  idcnop  27571  nmop0  27576  nmfn0  27577  nmlnop0iALT  27585  nmcexi  27616  nmcopexi  27617  lnconi  27623  lnopcon  27625  nmcfnexi  27641  lnfncon  27646  branmfn  27695  leop3  27715  opsqrlem6  27735  cvmd  27926  cvdmd  27927  cvexch  27964  cdj3i  28031  fmptcof2  28200  xraddge02  28281  xdivpnfrp  28348  omndadd  28415  omndmul  28423  archirngz  28452  archiabllem2a  28457  isorng  28509  madjusmdetlem2  28601  locfinreflem  28614  locfinref  28615  sqsscirc2  28662  cnre2csqlem  28663  xrge0iifiso  28688  lmdvg  28706  qqhcn  28742  qqhucn  28743  esum2d  28861  brfae  29018  dya2ub  29039  omssubadd  29075  omssubaddOLD  29079  carsgmon  29093  oddpwdc  29134  eulerpartlemd  29146  ballotlemfc0  29272  ballotlemfcc  29273  ballotlemic  29286  ballotlemsv  29289  ballotlemrc  29310  ballotlemiminOLD  29323  ballotlemicOLD  29324  ballotlemsvOLD  29327  ballotlemfrcn0OLD  29347  ballotlemrcOLD  29348  sgnmul  29360  sgnmulsgn  29367  signsply0  29387  signswch  29397  signsvfn  29418  signsvfnn  29422  signlem0  29423  erdszelem8  29868  kur14  29886  snmlval  30001  snmlflim  30002  sinccvg  30264  abs2sqle  30271  abs2sqlt  30272  faclim2  30330  br1steqg  30362  br2ndeqg  30363  poseq  30437  soseq  30438  sltval  30480  brimg  30648  cgrtriv  30713  cgrdegen  30715  brofs  30716  cgrextend  30719  segconeu  30722  fvtransport  30743  transportprops  30745  brifs  30754  ifscgr  30755  brcgr3  30757  cgrxfr  30766  brfs  30790  btwnconn1lem7  30804  btwnconn1lem11  30808  btwnconn1lem12  30809  btwnconn1lem14  30811  brsegle  30819  segleantisym  30826  outsideofeu  30842  nn0prpwlem  30922  nn0prpw  30923  nndivlub  31062  poimirlem28  31875  poimirlem29  31876  poimirlem31  31878  poimir  31880  heicant  31882  dvtanlemOLD  31898  itg2addnclem  31900  itg2addnclem3  31902  itg2addnc  31903  itg2gt0cn  31904  bddiblnc  31919  ftc1cnnclem  31922  ftc1cnnc  31923  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anc  31932  areacirclem1  31939  areacirclem2  31940  areacirclem4  31942  areacirclem5  31943  areacirc  31944  seqpo  31983  incsequz2  31985  lmclim2  31994  geomcau  31995  caushft  31997  prdsbnd  32032  ismtyima  32042  heiborlem4  32053  heiborlem6  32055  heiborlem7  32056  bfplem1  32061  bfplem2  32062  rrndstprj2  32070  rrncmslem  32071  rrnequiv  32074  oposlem  32660  opltcon2b  32684  pats  32763  ishlat1  32830  cvrexch  32897  atle  32913  athgt  32933  1cvrco  32949  3atlem5  32964  4atlem3  33073  dalawlem15  33362  lhprelat3N  33517  lautle  33561  lautcvr  33569  ltrnatb  33614  ltrneq2  33625  cdlemefr32sn2aw  33883  cdlemefs32sn1aw  33893  cdleme32fvaw  33918  cdleme35sn3a  33938  cdleme46frvlpq  33983  cdleme48gfv  34016  trlord  34048  cdlemg1fvawlemN  34052  cdlemg7fvbwN  34086  cdlemg31d  34179  istendo  34239  dva1dim  34464  dvhb1dimN  34465  diafval  34511  diaelval  34513  cdlemm10N  34598  dihopelvalcpre  34728  dihmeetcN  34782  dihmeetlem6  34789  dihjatc1  34791  irrapxlem3  35581  irrapxlem4  35582  irrapxlem5  35583  irrapxlem6  35584  pellexlem3  35588  monotoddzz  35704  jm2.19  35761  rmydioph  35782  fnwe2lem2  35822  hbtlem1  35895  hbtlem2  35896  hbtlem7  35897  hbtlem4  35898  hbtlem5  35900  hbtlem6  35901  dgrsub2  35907  fiuneneq  35984  rp-isfinite5  36075  frege124d  36266  frege92  36464  leeq1d  36508  extoimad  36520  isprm7  36573  nzss  36579  evth2f  37252  evthf  37264  cncmpmax  37269  rfcnpre4  37271  supxrgere  37453  suplesup  37459  fmul01  37541  climinf  37567  climinfOLD  37568  climsuse  37570  mullimc  37579  ellimcabssub0  37580  climf  37585  mullimcf  37586  idlimc  37589  limcperiod  37591  clim2f  37599  limsupre  37604  limsupreOLD  37605  limcleqr  37608  limclner  37615  clim0cf  37618  cncfshift  37634  cncfperiod  37639  fperdvper  37673  dvbdfbdioolem2  37684  dvbdfbdioo  37685  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweidlem7  37750  stoweidlem9  37752  stoweidlem15  37758  stoweidlem16  37759  stoweidlem18  37761  stoweidlem21  37764  stoweidlem26  37769  stoweidlem31  37775  stoweidlem34  37778  stoweidlem36  37780  stoweidlem37  37781  stoweidlem41  37785  stoweidlem44  37788  stoweidlem45  37789  stoweidlem46  37790  stoweidlem48  37792  stoweidlem51  37795  stoweidlem52  37796  stoweidlem55  37799  stoweidlem59  37803  stoweidlem60  37804  fourierdlem20  37872  fourierdlem25  37877  fourierdlem37  37890  fourierdlem39  37892  fourierdlem41  37894  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem54  37907  fourierdlem64  37917  fourierdlem68  37921  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem79  37932  fourierdlem80  37933  fourierdlem87  37940  fourierdlem96  37949  fourierdlem97  37950  fourierdlem98  37951  fourierdlem99  37952  fourierdlem103  37956  fourierdlem104  37957  fourierdlem105  37958  fourierdlem108  37961  fourierdlem109  37962  fourierdlem111  37964  fourierswlem  37977  fouriersw  37978  etransclem31  38013  etransclem47  38029  etransclem48OLD  38030  etransclem48  38031  etransc  38032  sge0lefimpt  38116  sge0isummpt2  38125  sge0gtfsumgt  38136  omessle  38170  ovnsubaddlem1  38239  ovnsubadd  38241  hsphoif  38245  hsphoival  38248  hsphoidmvle2  38254  sge0hsphoire  38258  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  hoidmvlelem5  38268  hoidmvle  38269  iccpartlt  38551  iccpartltu  38552  iccpartgt  38554  iccpartleu  38555  iccpartrn  38557  iccpartiun  38561  icceuelpartlem  38562  iccpartdisj  38564  iccpartnel  38565  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  bgoldbtbnd  38717  upgrle  38956  upgrfi  38957  upgr1elem  38970  edgupgr  38988  upgredg  38990  usgruspgrb  39024  subupgr  39096  upgrres1  39117  pgrpgt2nabl  39744  ply1mulgsumlem1  39771  ply1mulgsumlem2  39772  divge1b  39901  divgt1b  39902  divlt1lt  39903  logge0b  39935  loggt0b  39936  regt1loggt0  39940  elbigo  39955  elbigolo1  39961  logblt1b  39968  nnlog2ge0lt1  39970  logbpw2m1  39971  blenpw2m1  39983
  Copyright terms: Public domain W3C validator