Theorem breq2d 4665

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
breq2d	|- ( ph -> ( C R A <-> C R B ) )

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq2 4657	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breqtrd  4679  sbcbr1g  4709  pofun  5051  csbfv12  6231  isorel  6576  soisores  6577  soisoi  6578  isocnv  6580  isotr  6586  f1owe  6603  caovordig  6839  caovordg  6841  caovord  6845  f1oweALT  7152  frxp  7287  xporderlem  7288  fnwelem  7292  difsnen  8042  domdifsn  8043  unfilem3  8226  domunfican  8233  marypha1lem  8339  marypha1  8340  inflb  8395  wemapwe  8594  oef1o  8595  r1sdom  8637  sdomsdomcardi  8797  alephordi  8897  pwcdadom  9038  sornom  9099  axdclem  9341  pwcfsdom  9405  elgch  9444  winalim2  9518  rankcf  9599  inatsk  9600  pinq  9749  nqereu  9751  ltaddnq  9796  ltrnq  9801  archnq  9802  addclprlem1  9838  mulclprlem  9841  1idpr  9851  ltaprlem  9866  ltapr  9867  prlem936  9869  ltasr  9921  mulgt0sr  9926  sqgt0sr  9927  map2psrpr  9931  axpre-ltadd  9988  axpre-mulgt0  9989  axpre-sup  9990  ltaddneg  10251  ltsubadd2  10499  lesubadd2  10501  ltaddpos2  10519  posdif  10521  lesub1  10522  ltnegcon1  10529  lenegcon1  10532  addge02  10539  leaddle0  10543  mulge0  10546  msqge0  10549  ltordlem  10553  possumd  10652  sublt0d  10653  prodgt0  10868  prodgt02  10869  prodge02  10871  ltmulgt12  10884  lemulge12  10886  mulge0b  10893  mulle0b  10894  ltdivmul  10898  ledivmul  10899  ltdivmul2  10900  lt2mul2div  10901  ledivmul2  10902  ltrec  10905  ltrec1  10910  ltdiv23  10914  lediv23  10915  nnge1  11046  halfpos  11262  lt2halves  11267  addltmul  11268  avglt2  11271  avgle2  11273  nnrecl  11290  difgtsumgt  11346  zltlem1  11430  nn0le2is012  11441  gtndiv  11454  nn01to3  11781  rebtwnz  11787  nnledivrp  11940  xrmax1  12006  max1ALT  12017  qbtwnre  12030  xralrple  12036  xltnegi  12047  xmulval  12056  xsubge0  12091  xposdif  12092  xlesubadd  12093  divelunit  12314  eluzgtdifelfzo  12529  fllelt  12598  flflp1  12608  flbi  12617  btwnzge0  12629  2tnp1ge0ge0  12630  dfceil2  12640  ceilval2  12641  2submod  12731  addmodlteq  12745  om2uzlti  12749  monoord  12831  sermono  12833  expval  12862  expnbnd  12993  discr1  13000  discr  13001  facwordi  13076  seqcoll  13248  seqcoll2  13249  hashtpg  13267  swrdccat3blem  13495  cnpart  13980  sqrlem6  13988  sqrmo  13992  resqreu  13993  resqrtcl  13994  resqrtthlem  13995  sqrtneg  14008  sqreulem  14099  sqreu  14100  sqrtthlem  14102  eqsqrtd  14107  limsuple  14209  rlimcld2  14309  rlimrege0  14310  o1compt  14318  climserle  14393  caurcvgr  14404  fsum00  14530  fsumabs  14533  climcndslem2  14582  climcnds  14583  supcvg  14588  georeclim  14603  geoisumr  14609  cvgrat  14615  sin01bnd  14915  cos01bnd  14916  ruclem1  14960  ruclem9  14967  ruclem12  14970  summodnegmod  15012  modmulconst  15013  dvdsaddr  15025  dvdssub  15026  dvdssubr  15027  dvdsfac  15048  dvdsmod  15050  fprodfvdvdsd  15058  oddp1even  15068  ltoddhalfle  15085  opoe  15087  omoe  15088  sumeven  15110  sumodd  15111  divalglem0  15116  divalglem2  15118  divalglem4  15119  divalglem5  15120  divalglem9  15124  divalg  15126  divalg2  15128  divalgmod  15129  divalgmodOLD  15130  ndvdssub  15133  ndvdsadd  15134  bitsfval  15145  bitsval  15146  bits0  15150  bitsp1  15153  bitsfzolem  15156  bitsfzo  15157  bitscmp  15160  bitsinv1lem  15163  bitsshft  15197  gcdcllem1  15221  dvdslegcd  15226  bezoutlem4  15259  dvdssqim  15273  dvdsmulgcd  15274  dvdssq  15280  nn0seqcvgd  15283  lcmfunsnlem2lem2  15352  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  rpmul  15373  cncongr1  15381  divgcdodd  15422  isprm6  15426  prmdvdsexp  15427  prmdvdsexpr  15429  prmfac1  15431  hashdvds  15480  phiprmpw  15481  eulerthlem2  15487  prmdiv  15490  prmdiveq  15491  odzval  15496  odzcllem  15497  odzdvds  15500  pythagtriplem11  15530  pythagtriplem13  15532  pythagtrip  15539  pceulem  15550  pczndvds2  15571  pcdvdsb  15573  pc2dvds  15583  pcz  15585  pcprmpw2  15586  dvdsprmpweq  15588  dvdsprmpweqle  15590  difsqpwdvds  15591  pcaddlem  15592  pcmpt  15596  prmpwdvds  15608  pockthlem  15609  prmreclem2  15621  prmreclem4  15623  4sqlem11  15659  vdwlem9  15693  rami  15719  ramlb  15723  0ram  15724  ramz2  15728  ramub1lem1  15730  prmdvdsprmo  15746  prmgaplem7  15761  prmgaplem8  15762  setsstruct  15898  imasleval  16201  subsubc  16513  pospo  16973  mulgval  17543  oddvdsnn0  17963  odmulg  17973  pgpfi1  18010  pgpfi  18020  slwispgp  18026  pgpssslw  18029  subgslw  18031  sylow2alem2  18033  sylow2blem3  18037  fislw  18040  efgi  18132  efgval2  18137  efgsrel  18147  efgredlemb  18159  lt6abl  18296  telgsums  18390  dprdval  18402  dprd2dlem2  18439  dprd2da  18441  dprd2d2  18443  ablfacrplem  18464  ablfac1a  18468  ablfac1b  18469  ablfac1eulem  18471  ablfac1eu  18472  pgpfac1lem3a  18475  ablfaclem3  18486  dvdsrtr  18652  dvdsrmul1  18653  unitpropd  18697  isabvd  18820  mplval  19428  ressmplbas2  19455  mplbaspropd  19607  zndvds0  19899  znunit  19912  cygth  19920  frlmup1  20137  lmisfree  20181  pmatcoe1fsupp  20506  fvmptnn04if  20654  hmphindis  21600  ordthmeolem  21604  psmettri2  22114  ismet2  22138  xmettri2  22145  imasdsf1olem  22178  imasf1oxmet  22180  comet  22318  stdbdxmet  22320  nmogelb  22520  nmolb  22521  metdsge  22652  metdseq0  22657  iihalf2  22732  bndth  22757  evth  22758  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  iscau3  23076  iscmet3  23091  bcthlem1  23121  bcth  23126  minveclem3b  23199  minveclem3  23200  minveclem4  23203  minveclem5  23204  pjthlem1  23208  pjthlem2  23209  pmltpclem1  23217  pmltpc  23219  ivthlem2  23221  ivthlem3  23222  ovolgelb  23248  ovolunlem1  23265  ovoliunlem2  23271  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem3  23287  ioombl1lem4  23329  mbfmulc2lem  23414  mbfposb  23420  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  mbflimsup  23433  i1fposd  23474  itg1ge0a  23478  mbfi1fseqlem4  23485  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfi1flim  23490  itg2const2  23508  itg2seq  23509  itg2monolem1  23517  itg2i1fseq  23522  itg2addlem  23525  ibllem  23531  isibl  23532  isibl2  23533  iblitg  23535  dfitg  23536  cbvitg  23542  itgeq2  23544  itgvallem  23551  iblneg  23569  itgneg  23570  itggt0  23608  dvlip  23756  c1lip1  23760  dvfsumle  23784  dvfsumlem2  23790  dvfsumlem4  23792  dvfsum2  23797  mdeglt  23825  degltp1le  23833  deg1suble  23867  ply1divex  23896  plypf1  23968  dgrlb  23992  coemulc  24011  dgrsub  24028  quotval  24047  plydivlem4  24051  quotcan  24064  vieta1lem2  24066  aalioulem2  24088  aaliou3lem9  24105  ulmcn  24153  dvradcnv  24175  sincosq1sgn  24250  sincosq2sgn  24251  sincosq4sgn  24253  logltb  24346  logle1b  24379  loglt1b  24380  cxpge0  24429  cxple2  24443  logreclem  24500  jensen  24715  emcllem7  24728  lgamgulmlem1  24755  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  lgamcvglem  24766  wilthlem1  24794  ftalem2  24800  ftalem3  24801  ftalem7  24805  fta  24806  sgmval  24868  mumul  24907  dvdsppwf1o  24912  musum  24917  chtublem  24936  chtub  24937  perfect1  24953  bcmono  25002  bclbnd  25005  bposlem1  25009  bposlem5  25013  lgslem1  25022  lgsval  25026  lgsdilem  25049  lgsne0  25060  lgsqrlem2  25072  lgsqrlem4  25074  gausslemma2dlem1a  25090  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem2  25110  m1lgs  25113  2lgslem1a1  25114  2lgslem1a  25116  2lgsoddprmlem2  25134  2lgsoddprmlem3  25139  2sqlem4  25146  2sqlem8a  25150  2sqblem  25156  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  chpdifbndlem2  25243  pntrsumbnd2  25256  pntpbnd1  25275  pntibndlem3  25281  pntlemi  25293  pntleme  25297  pntlem3  25298  pnt3  25301  ostth2lem2  25323  ostth3  25327  ostth  25328  tgcgrxfr  25413  hlpasch  25648  islmib  25679  lmicom  25680  trgcopyeu  25698  iscgra  25701  iscgra1  25702  iscgrad  25703  isleag  25733  iseqlg  25747  brbtwn2  25785  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem3  25846  axcontlem4  25847  axcontlem9  25852  axcontlem10  25853  axcontlem11  25854  axcontlem12  25855  ebtwntg  25862  umgrislfupgrlem  26017  lfgredgge2  26019  lfgrnloop  26020  lfuhgr1v0e  26146  1hevtxdg1  26402  vtxdgoddnumeven  26449  ewlksfval  26497  isewlk  26498  ewlkinedg  26500  lfgrwlkprop  26584  crctcshlem4  26712  umgrwwlks2on  26850  elwwlks2  26861  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  eupth2lem3lem3  27090  eupth2lem3lem4  27091  eupth2lem3lem6  27093  eupth2lem3lem7  27094  eupth2lems  27098  eupth2  27099  eucrct2eupth  27105  konigsberglem4  27117  frgrreggt1  27251  ex-ind-dvds  27318  nmounbseqi  27632  nmounbseqiALT  27633  isblo3i  27656  blo3i  27657  blocnilem  27659  siilem2  27707  normlem6  27972  normgt0  27984  norm3dif  28007  norm3lemt  28009  pjhthlem1  28250  pjige0  28550  nmcexi  28885  lnconi  28892  lnopcnbd  28895  lnfncnbd  28916  riesz1  28924  cnlnadjlem2  28927  cnlnadjlem8  28933  leopg  28981  leop2  28983  leoppos  28985  leopadd  28991  leopmuli  28992  leopmul2i  28994  pjssge0i  29025  pjdifnormi  29026  pjssposi  29031  pjssdif1i  29034  chcv1  29214  cvexch  29233  atcvatlem  29244  atcvat3i  29255  atdmd  29257  cdj3i  29300  addltmulALT  29305  xrofsup  29533  fsumiunle  29575  xrge0addgt0  29691  omndadd  29706  omndmul2  29712  ogrpinvlt  29724  isinftm  29735  isarchi3  29741  archirng  29742  archirngz  29743  archiexdiv  29744  isorng  29799  orngmul  29803  ofldchr  29814  isarchiofld  29817  elrhmunit  29820  rearchi  29842  fzto1st  29853  unitdivcld  29947  esumlub  30122  esumfsup  30132  esumcvg  30148  esum2d  30155  dya2ub  30332  omssubadd  30362  carsgmon  30376  itgeq12dv  30388  oddpwdc  30416  eulerpartlems  30422  prob01  30475  orvcval  30519  ballotlemfc0  30554  ballotlemfcc  30555  ballotleme  30558  ballotlem4  30560  ballotlemimin  30567  ballotlem1c  30569  ballotlemsval  30570  ballotlemieq  30578  ballotlemfrcn0  30591  sgnmulsgp  30612  signsply0  30628  signslema  30639  signsvfpn  30662  erdszelem8  31180  erdsze2lem2  31186  abs2sqle  31574  abs2sqlt  31575  pdivsq  31635  dvdspw  31636  poseq  31750  soseq  31751  sltval  31800  nolt02o  31845  nosupbnd1lem1  31854  nosupbnd1lem2  31855  nosupbnd2  31862  conway  31910  scutcut  31912  scutbday  31913  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  cgrdegen  32111  brofs  32112  segconeu  32118  btwntriv2  32119  transportprops  32141  brifs  32150  ifscgr  32151  brcgr3  32153  cgrxfr  32162  brcolinear2  32165  colineardim1  32168  brfs  32186  idinside  32191  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn1lem14  32207  brsegle  32215  seglerflx  32219  seglemin  32220  segleantisym  32222  btwnsegle  32224  outsideofeu  32238  outsidele  32239  fvray  32248  nn0prpwlem  32317  nn0prpw  32318  unblimceq0lem  32497  unbdqndv2  32502  knoppndvlem13  32515  knoppndvlem19  32521  knoppndvlem21  32523  ltflcei  33397  cos2h  33400  tan2h  33401  matunitlindflem2  33406  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  itggt0cn  33482  ftc1anclem5  33489  dvasin  33496  areacirclem1  33500  areacirclem4  33503  areacirclem5  33504  areacirc  33505  seqpo  33543  incsequz2  33545  mettrifi  33553  heibor1lem  33608  rrncmslem  33631  lsatcv0eq  34334  oposlem  34469  oplecon1b  34488  opltcon1b  34492  atlatmstc  34606  cvlexch1  34615  cvlexch2  34616  cvlexchb2  34618  cvlatexchb2  34622  cvlatexch2  34624  cvlatcvr2  34629  cvlsupr2  34630  ishlat1  34639  hlsuprexch  34667  cvrexch  34706  cvrat  34708  atcvr0eq  34712  atcvrj0  34714  atltcvr  34721  cvrat3  34728  cvrat4  34729  cvrat42  34730  3noncolr2  34735  hlatcon2  34738  4noncolr3  34739  3dimlem1  34744  3dimlem2  34745  3dimlem3a  34746  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  3dim1lem5  34752  3dim2  34754  3dim3  34755  ps-1  34763  ps-2  34764  3atlem5  34773  3atlem6  34774  lplni2  34823  lplnnle2at  34827  lplnnleat  34828  lplnnlelln  34829  lplnribN  34837  lplnexllnN  34850  lvoli2  34867  lvolnle3at  34868  lvolnleat  34869  lvolnlelln  34870  lvolnlelpln  34871  4atlem9  34889  4atlem10a  34890  4atlem11a  34893  4atlem11  34895  4atlem12a  34896  dalempnes  34937  dalemqnet  34938  dalem1  34945  dalemswapyzps  34976  dalemrotps  34977  dalem30  34988  dalem35  34993  lineset  35024  islinei  35026  psubspset  35030  psubspi2N  35034  snatpsubN  35036  2llnma1  35073  elpaddn0  35086  elpaddri  35088  elpaddat  35090  elpadd2at  35092  paddcom  35099  paddasslem12  35117  pmapjat1  35139  llnexchb2  35155  lhp2at0nle  35321  lhprelat3N  35326  4atexlemswapqr  35349  4atexlemcnd  35358  lautle  35370  lautcvr  35378  ltrnel  35425  ltrneq2  35434  trlnle  35473  cdlemc3  35480  cdlemd6  35490  cdleme3  35524  cdleme7aa  35529  cdleme7  35536  cdleme11c  35548  cdleme15c  35563  cdleme20yOLD  35590  cdleme20m  35611  cdleme21b  35614  cdleme21c  35615  cdleme21at  35616  cdleme36a  35748  cdleme43bN  35778  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemb3  35894  cdlemg4d  35901  cdlemg6d  35909  cdlemg10c  35927  cdlemg12  35938  cdlemg27b  35984  djhcvat42  36704  elpell1qr2  37436  monotuz  37506  monotoddzzfi  37507  monotoddzz  37508  oddcomabszz  37509  rmxypos  37514  mzpcong  37539  congrep  37540  acongsym  37543  acongneg2  37544  acongtr  37545  acongeq12d  37546  jm2.18  37555  jm2.19lem2  37557  jm2.19lem3  37558  jm2.19lem4  37559  jm2.19  37560  jm2.25  37566  jm2.15nn0  37570  jm2.16nn0  37571  jm2.27  37575  rmydioph  37581  expdiophlem1  37588  expdiophlem2  37589  fnwe2lem2  37621  relexpmulg  38002  relexpxpmin  38009  frege124d  38053  frege72  38229  frege91  38248  inductionexd  38453  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  dvgrat  38511  hashnzfz  38519  evth2f  39174  evthf  39186  rfcnpre3  39192  brneqtrd  39248  dmrelrnrel  39419  upbdrech2  39522  supxrgelem  39553  supxrge  39554  xrlexaddrp  39568  xralrple2  39570  ltdivgt1  39572  infleinf  39588  xralrple4  39589  xralrple3  39590  ltdiv23neg  39617  leneg3d  39687  fsumlessf  39809  fmul01  39812  fmul01lt1lem1  39816  climinf  39838  climinff  39843  limcrecl  39861  limsupre  39873  limclner  39883  limsuppnfd  39934  climinf2  39939  limsuppnf  39943  climinfmpt  39947  limsupre2  39957  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uz  39968  limsupreuz  39969  limsupvaluz2  39970  limsupreuzmpt  39971  limsupge  39993  liminfreuz  40035  liminflt  40037  liminflimsupclim  40039  cnrefiisp  40056  xlimpnf  40068  xlimpnfmpt  40070  climxlim2lem  40071  dfxlim2  40074  cncficcgt0  40101  stoweidlem3  40220  stoweidlem7  40224  stoweidlem15  40232  stoweidlem16  40233  stoweidlem18  40235  stoweidlem26  40243  stoweidlem27  40244  stoweidlem28  40245  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem37  40254  stoweidlem41  40258  stoweidlem44  40261  stoweidlem45  40262  stoweidlem46  40263  stoweidlem48  40265  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  fourierdlem42  40366  fourierdlem50  40373  fourierdlem54  40377  fourierdlem68  40391  fourierdlem79  40402  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem105  40428  fourierdlem108  40431  fourierdlem110  40433  fourierdlem111  40434  etransclem24  40475  etransclem25  40476  etransclem35  40486  etransclem37  40488  etransclem41  40492  etransclem44  40495  sge0gerp  40612  sge0pnffigt  40613  sge0gerpmpt  40619  omessle  40712  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  hoidmv1lelem2  40806  hoidmvlelem3  40811  hoidmvle  40814  ovncvr2  40825  hoidifhspval2  40829  hoidifhspval3  40833  hspmbllem2  40841  hspmbl  40843  pimgtpnf2  40917  pimgtmnf2  40924  pimdecfgtioc  40925  pimdecfgtioo  40927  pimincfltioo  40928  pimgtmnf  40932  incsmf  40951  issmfgt  40965  decsmf  40975  smfpreimagtf  40976  issmfge  40978  smflimlem4  40982  smflim  40985  smfpimgtxr  40988  smfpimgtmpt  40989  smfpimgtxrmpt  40992  smfinflem  41023  smfinf  41024  smfinfmpt  41025  ltsubsubaddltsub  41315  subsubelfzo0  41336  smonoord  41341  iccpartiltu  41358  iccpartlt  41360  iccpartgtl  41362  iccpartgt  41363  iccpartgel  41365  iccpartrn  41366  iccpartiun  41370  icceuelpartlem  41371  iccpartdisj  41373  iccpartnel  41374  goldbachthlem2  41458  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnofac1  41482  2pwp1prm  41503  flsqrt  41508  lighneallem1  41522  lighneallem3  41524  lighneallem4  41527  bits0ALTV  41590  sbgoldbaltlem1  41667  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  1hegrlfgr  41713  lcoop  42200  islininds  42235  ldepsnlinc  42297  ltsubaddb  42304  ltsubsubb  42305  ltsubadd2b  42306  bigoval  42343  elbigo2r  42347  logbge0b  42357  logblt1b  42358  fldivexpfllog2  42359  nnlog2ge0lt1  42360  fllog2  42362  nnpw2pmod  42377  dignn0ldlem  42396  dig2nn1st  42399