Theorem breqtrd 5136

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
breqtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 5120	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1568   class class class wbr 5108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is referenced by:  breqtrrd  5138  breqtrid  5147  domunsn  9114  mapdom2  9135  phplem2  9188  mapfien2  9368  wemaplem2  9508  infdifsn  9625  cantnff  9642  ttrclss  9688  rnttrcl  9690  infxpenlem  9996  infmap2  10199  ssfin4  10293  canthp1lem1  10636  nqereq  10919  ltexnq  10959  ltbtwnnq  10962  add20  11725  mullt0  11732  ltm1  12056  recgt0  12060  prodgt0  12061  ltmul1a  12063  mulge0b  12084  recp1lt1  12112  recreclt  12113  ledivp1  12116  ledivp1i  12139  ltdivp1i  12140  eluzmn  12868  ltaddrp2d  13093  mul2lt0bi  13123  prodge0rd  13124  xleadd1a  13278  xov1plusxeqvd  13524  fz01en  13579  fzonmapblen  13736  fladdz  13857  flhalf  13862  fldiv  13892  modsubdir  13975  fzen2  14004  serle  14092  ltexp2a  14201  leexp2a  14207  exple1  14212  expubnd  14213  bernneq  14264  expmulnbnd  14270  discr1  14274  discr  14275  faclbnd6  14334  hashfz  14463  hashfun  14473  seqcoll  14500  sqeqd  15216  01sqrexlem7  15298  sqrtge0  15307  sqrtneglem  15316  abslt  15365  absle  15366  abstri  15381  rlimge0  15631  reccn2  15647  climaddc2  15686  isercolllem1  15715  caucvgrlem  15723  summolem2a  15765  isumge0  15816  fsumle  15850  fsumlt  15851  o1fsum  15864  supcvg  15909  expcnv  15917  geolim  15923  geolim2  15924  georeclim  15925  geo2lim  15928  mertenslem1  15937  mertens  15939  prodmolem2a  15987  efcllem  16130  ef0lem  16131  efgt0  16158  eftlub  16164  eflt  16172  sinbnd  16235  cosbnd  16236  ef01bndlem  16239  sin01gt0  16245  cos01gt0  16246  sin02gt0  16247  eirrlem  16259  rpnnen2lem11  16279  rpnnen2lem12  16280  ruclem11  16295  dvdssub2  16358  dvdsadd2b  16363  dvdsexp  16385  3dvds  16388  opoe  16420  bitsfzolem  16491  bitsinv1lem  16498  bezoutlem4  16599  dvdsgcd  16601  dvdsmulgcd  16613  bezoutr1  16626  nn0seqcvgd  16627  rpmulgcd2  16713  qredeq  16714  rpdvds  16717  prmind2  16742  divdenle  16807  hashdvds  16833  phimullem  16837  eulerthlem2  16840  prmdiveq  16844  prmdivdiv  16845  pythagtriplem4  16878  pythagtriplem10  16879  pythagtriplem19  16892  iserodd  16894  pcpre1  16901  pcadd2  16949  qexpz  16960  expnprm  16961  oddprmdvds  16962  pockthlem  16964  prmreclem2  16976  prmreclem3  16977  4sqlem7  17003  4sqlem10  17006  4sqlem11  17014  4sqlem12  17015  4sqlem14  17017  4sqlem15  17018  4sqlem16  17019  0ram  17079  ffthiso  17987  latmlej12  18534  qusgrp  19256  pgpfi1  19664  sylow1lem4  19670  sylow1lem5  19671  odcau  19673  pgpfi  19674  pgpssslw  19683  sylow3lem4  19699  sylow3lem6  19701  efgsfo  19808  frgp0  19829  odadd1  19917  odadd2  19918  odadd  19919  gexexlem  19921  lt6abl  19964  gsumzsubmcl  19987  pwsgsum  20051  dprd2dlem1  20112  dprd2d2  20115  ablfacrplem  20136  ablfacrp  20137  ablfacrp2  20138  ablfac1b  20141  ablfac1eu  20144  pgpfac1lem3a  20147  ablfaclem2  20157  dvdsrid  20448  dvdsrtr  20449  dvdsrneg  20451  unitmulcl  20461  unitgrp  20464  unitnegcl  20478  subrguss  20671  subrgunit  20674  isdrng2  20828  fidomndrnglem  20855  abvsubtri  20909  orngsqr  20948  ornglmulle  20949  orngrmulle  20950  orng0le1  20956  gzrngunit  21562  prmirredlem  21601  znidomb  21690  frlmgsum  21901  psrbaglesupp  22051  psdmul  22308  psdmvr  22311  invrvald  22812  psmetsym  24446  psmettri  24447  mettri2  24477  xmetsym  24483  xmettri  24487  prdsxmetlem  24504  xblss2ps  24537  xblss2  24538  blhalf  24541  xmsge0  24599  ngptgp  24772  nrginvrcnlem  24827  nmoeq0  24872  cnmet  24907  blcvx  24934  opnreen  24968  metdcnlem  24973  metdstri  24988  metdsle  24989  metnrmlem1  24996  metnrmlem3  24998  lebnumlem1  25099  pi1inv  25190  cphnmf  25333  ipge0  25336  ipcau2  25372  tcphcphlem1  25373  csbren  25537  minveclem2  25564  minveclem3  25567  ovolssnul  25625  ovolctb  25628  ovolunnul  25638  ovoliunlem1  25640  ovoliun2  25644  ovoliunnul  25645  ioombl1lem4  25699  uniioombllem3  25723  uniioombllem4  25724  uniioombllem5  25725  uniioombl  25727  volcn  25744  vitalilem2  25747  vitalilem5  25750  itg1lea  25850  mbfi1fseqlem6  25858  mbfi1flimlem  25860  itg2eqa  25883  itg2splitlem  25886  itg2split  25887  itg2monolem1  25888  itg2cnlem2  25900  iblabsr  25968  iblmulc2  25969  bddiblnc  25980  dveflem  26117  dvef  26118  dvferm2lem  26124  dvlip  26131  c1liplem1  26134  dveq0  26138  dvlt0  26143  dvivthlem1  26146  lhop1  26152  dvfsumle  26159  dvfsumlem4  26167  dvfsumrlim3  26171  dvfsum2  26172  ftc1a  26175  ftc1lem4  26177  deg1add  26239  ply1divex  26273  ply1rem  26302  fta1glem2  26305  fta1blem  26307  ig1pdvds  26316  plyeq0lem  26346  dgrcolem2  26410  plydivlem4  26436  plyrem  26445  fta1lem  26447  aalioulem3  26474  aaliou2b  26481  aaliou3lem3  26484  aaliou3lem8  26485  ulmcn  26538  ulmdvlem1  26539  itgulm  26547  pserulm  26561  pserdvlem2  26567  abelthlem2  26571  abelthlem5  26574  abelthlem6  26575  abelthlem7  26577  abelthlem8  26578  abelthlem9  26579  sinq12gt0  26648  sinq34lt0t  26650  cosq14gt0  26651  cosq14ge0  26652  cos02pilt1  26667  efif1olem3  26685  argimgt0  26753  argimlt0  26754  logneg2  26756  logcnlem3  26785  logcnlem4  26786  logtayllem  26800  logtayl2  26803  cxpsqrtlem  26843  cxpsqrt  26844  cxpaddlelem  26892  abscxpbnd  26894  zrtdvds  26900  rtprmirr  26901  loglesqrt  26902  ang180lem2  26951  atanlogaddlem  27054  atanlogsublem  27056  atantan  27064  atans2  27072  atantayl  27078  leibpi  27083  log2tlbnd  27086  birthdaylem2  27093  birthdaylem3  27094  cxp2limlem  27116  jensenlem2  27128  jensen  27129  logdiflbnd  27135  emcllem2  27137  emcllem4  27139  harmonicbnd4  27151  fsumharmonic  27152  lgamgulmlem2  27170  lgamgulm2  27176  lgambdd  27177  lgamucov  27178  lgamcvglem  27180  lgamcvg2  27195  gamcvg  27196  wilthlem3  27210  basellem1  27221  basellem3  27223  basellem4  27224  fsumdvdsdiaglem  27323  dvdsppwf1o  27326  mpodvdsmulf1o  27334  dvdsmulf1o  27336  chteq0  27349  chtub  27352  chpub  27360  logfacubnd  27361  logfaclbnd  27362  logexprlim  27365  perfectlem2  27370  dchrfi  27395  bclbnd  27420  bposlem1  27424  bposlem3  27426  bposlem4  27427  bposlem6  27429  lgslem1  27437  lgsqrlem2  27487  lgsqrlem4  27489  lgseisenlem2  27516  lgsquadlem1  27520  lgsquadlem2  27521  lgsquad2lem1  27524  2sqlem3  27560  2sqlem4  27561  2sqlem8  27566  2sqlem11  27569  2sqcoprm  27575  2sqmod  27576  chebbnd1lem2  27610  chebbnd1lem3  27611  chtppilimlem1  27613  chpchtlim  27619  vmadivsum  27622  vmadivsumb  27623  rpvmasumlem  27627  dchrisumlem2  27630  dchrmusum2  27634  dchrvmasumlem2  27638  dchrvmasumlem3  27639  dchrisum0flblem2  27649  dchrisum0fno1  27651  dchrisum0re  27653  dchrisum0lem1  27656  dchrisum0lem2a  27657  mudivsum  27670  mulogsumlem  27671  mulog2sumlem2  27675  vmalogdivsum2  27678  selberglem2  27686  selbergb  27689  selberg2b  27692  logdivbnd  27696  selberg3lem1  27697  selberg3lem2  27698  selberg4lem1  27700  pntrmax  27704  pntrlog2bndlem2  27718  pntrlog2bndlem3  27719  pntrlog2bndlem5  27721  pntrlog2bndlem6a  27722  pntrlog2bndlem6  27723  pntrlog2bnd  27724  pntpbnd1a  27725  pntpbnd1  27726  pntpbnd2  27727  pntibndlem1  27729  pntibndlem2  27731  pntlemb  27737  pntlemq  27741  pntlemr  27742  pntlemj  27743  pntlemk  27746  qabvle  27765  padicabvcxp  27772  ostth2lem2  27774  ostth2lem3  27775  ostth2lem4  27776  ostth3  27778  addsuniflem  28170  negsid  28210  negsunif  28224  negright  28228  mulsuniflem  28318  ltmuls2  28340  precsexlem9  28384  absmuls  28413  zcuts  28576  addhalfcut  28628  pw2cut2  28631  bdayfinbndlem1  28636  z12sge0  28652  legtrid  28836  legov3  28843  krippenlem  28943  mideulem2  28990  midex  28993  opphllem5  29007  opphllem6  29008  opphl  29010  lmieu  29067  lmiisolem  29079  perpeqlem  29123  prlnghpg  29169  perpprlng  29173  ttgcontlem1  29200  colinearalglem4  29225  axpaschlem  29256  axcontlem7  29286  nbfusgrlevtxm2  29694  clwlksndivn  30403  eucrct2eupth  30562  nvge0  30991  smcnlem  31015  nmoub3i  31091  nmoub2i  31092  nmlno0lem  31111  minvecolem2  31193  htthlem  31235  norm3dif2  31469  bcs2  31500  chscllem2  31956  eigposi  32154  nmopub2tALT  32227  nmfnleub2  32244  nmlnop0iALT  32313  riesz1  32383  cnlnadjlem2  32386  nmopcoadji  32419  leopsq  32447  leopmul  32452  leopnmid  32456  nmopleid  32457  opsqrlem6  32463  0leopj  32504  hstle1  32544  strlem3a  32570  mdslmd4i  32651  cvexchlem  32686  cdj1i  32751  unidifsnel  32847  unidifsnne  32848  le2halvesd  33067  xlt2addrd  33070  fsumub  33138  sgnmulsgp  33142  2exple2exp  33144  oexpled  33146  wrdt2ind  33239  xrge0tsmsd  33359  fzto1st1  33388  cycpmco2lem4  33415  cycpmco2lem6  33417  cyc3conja  33443  archiabllem1a  33477  archiabllem2a  33480  archiabllem2c  33481  rprmdvdsprod  33790  1arithidomlem1  33791  1arithidomlem2  33792  1arithidom  33793  ply1dg3rt0irred  33840  mplmulmvr  33895  mplvrpmrhm  33903  exsslsb  33953  fedgmullem1  33985  fedgmullem2  33986  fldsdrgfldext2  34018  fldextrspundgdvdslem  34036  fldextrspundgdvds  34037  fldext2rspun  34038  extdgfialglem2  34049  algextdeglem8  34080  rtelextdg2lem  34082  constrext2chnlem  34106  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  metideq  34249  metider  34250  sqsscirc1  34264  esummono  34410  esumpad2  34412  esumle  34414  esumlef  34418  esumcst  34419  esumrnmpt2  34424  esum2d  34449  aean  34600  dya2ub  34626  dya2icoseg  34633  omssubadd  34656  inelcarsg  34667  carsgsigalem  34671  carsggect  34674  carsgclctunlem2  34675  eulerpartlemb  34724  fibp1  34757  signsplypnf  34903  signsply0  34904  fdvposlt  34952  fdvposle  34954  reprgt  34974  logdivsqrle  35003  hgt750lemb  35009  hgt750leme  35011  tgoldbachgtde  35013  subfacval3  35635  sconnpht2  35684  sconnpi1  35685  resconn  35692  snmlff  35775  sinccvglem  36118  faclimlem2  36190  btwnouttr2  36468  weiunpo  36920  dnibndlem5  37015  dnibndlem7  37017  dnibndlem8  37018  dnibndlem9  37019  dnibndlem10  37020  dnibnd  37024  knoppcnlem4  37029  knoppcnlem9  37034  unbdqndv2lem1  37042  unbdqndv2lem2  37043  knoppndvlem11  37055  knoppndvlem12  37056  knoppndvlem14  37058  knoppndvlem15  37059  knoppndvlem17  37061  knoppndvlem18  37062  knoppndvlem19  37063  knoppndvlem21  37065  ltflcei  38203  poimirlem9  38224  poimirlem26  38241  poimirlem27  38242  poimirlem29  38244  heicant  38250  mblfinlem2  38253  mblfinlem3  38254  mblfinlem4  38255  volsupnfl  38260  itg2addnclem  38266  itg2addnclem3  38268  iblmulc2nc  38280  ftc1cnnclem  38286  ftc1anclem6  38293  ftc1anclem7  38294  ftc1anclem8  38295  ftc2nc  38297  dvasin  38299  geomcau  38354  bfplem2  38418  rrncmslem  38427  rrnequiv  38430  lsatcvatlem  39769  islshpcv  39773  atlatmstc  40039  cvlsupr7  40068  cvrval3  40133  cvrval5  40135  cvrexchlem  40139  atcvrj1  40151  cvrat3  40162  cvrat4  40163  atbtwn  40166  1cvratex  40193  hlatexch4  40201  3atlem1  40203  3atlem2  40204  atcvrlln2  40239  atcvrlln  40240  lplnllnneN  40276  llncvrlpln2  40277  4atlem3b  40318  lplncvrlvol2  40335  dalemswapyz  40376  dalemswapyzps  40410  dalem25  40418  dalem39  40431  dalem58  40450  dalem59  40451  lneq2at  40498  lncvrat  40502  dalawlem2  40592  dalawlem3  40593  dalawlem4  40594  dalawlem6  40596  dalawlem9  40599  dalawlem11  40601  dalawlem12  40602  lhpocnle  40736  lhpmcvr3  40745  lhpmcvr5N  40747  lhpmcvr6N  40748  4atexlemunv  40786  4atexlemc  40789  4atexlemex2  40791  lautm  40814  cdlemc2  40912  cdleme5  40960  cdleme11j  40987  cdleme16b  40999  cdlemednpq  41019  cdleme19e  41027  cdleme20i  41037  cdleme22a  41060  cdleme22cN  41062  cdleme22d  41063  cdleme22e  41064  cdleme22eALTN  41065  cdleme22f  41066  cdleme23c  41071  cdleme30a  41098  cdleme35a  41168  cdleme35b  41170  cdleme42h  41202  cdlemeg46rgv  41248  cdlemg8b  41348  cdlemg12e  41367  cdlemg13a  41371  cdlemg17pq  41392  cdlemg18c  41400  cdlemg19  41404  cdlemg21  41406  cdlemg31d  41420  cdlemg33a  41426  tendoid  41493  cdlemk4  41554  cdlemki  41561  cdlemk10  41563  cdlemksv2  41567  cdlemk12  41570  cdlemk14  41574  cdlemk15  41575  cdlemk1u  41579  cdlemk5u  41581  cdlemk12u  41592  cdlemk45  41667  cdlemk48  41670  dia2dimlem1  41784  dia2dimlem2  41785  dia2dimlem3  41786  cdlemm10N  41838  cdlemn2  41915  dihjustlem  41936  dihglbcpreN  42020  dihmeetlem3N  42025  nnproddivdvdsd  42713  lcmineqlem17  42758  lcmineqlem18  42759  3lexlogpow2ineq1  42771  3lexlogpow2ineq2  42772  3lexlogpow5ineq5  42773  aks4d1p1p3  42782  aks4d1p1p2  42783  aks4d1p1p4  42784  aks4d1p1p5  42788  aks4d1p1  42789  aks4d1p3  42791  aks4d1p8  42800  posbezout  42813  primrootspoweq0  42819  aks6d1c1  42829  hashscontpow1  42834  aks6d1c4  42837  aks6d1c2  42843  aks6d1c5lem1  42849  aks6d1c5lem3  42850  aks6d1c5lem2  42851  deg1gprod  42853  sticksstones7  42865  sticksstones10  42868  sticksstones12  42871  sticksstones22  42881  aks6d1c6lem1  42883  aks6d1c6lem3  42885  aks6d1c6lem4  42886  bcled  42891  bcle2d  42892  aks6d1c7lem1  42893  unitscyglem4  42911  aks5lem7  42913  aks5  42917  explt1d  43030  mulgt0b2d  43198  evlselv  43269  dffltz  43314  fltdvdsabdvdsc  43318  fltaccoprm  43320  fltabcoprm  43322  flt4lem5elem  43331  flt4lem7  43339  fltnlta  43343  irrapxlem1  43497  pell1qrgaplem  43548  pell1qrgap  43549  monotoddzzfi  43617  jm2.24nn  43634  congtr  43640  congmul  43642  congsub  43645  fzmaxdif  43656  acongeq  43658  jm2.20nn  43672  jm2.25  43674  hbtlem4  43801  dgrsub2  43810  mpaaeu  43825  idomsubgmo  43868  iscard4  44207  sqrtcvallem4  44313  leeq2d  44832  int-sqgeq0d  44860  int-ineqmvtd  44865  cvgdvgrat  44971  radcnvrat  44972  hashnzfzclim  44980  dvconstbi  44992  binomcxplemdvbinom  45011  isosctrlem1ALT  45590  mulltgt0  45690  rnmptbd2lem  45911  oddfl  45945  2timesgt  45955  lt3addmuld  45968  lt4addmuld  45973  supxrgere  45997  supxrgelem  46001  supxrge  46002  xadd0ge2  46005  infrpge  46015  xrlexaddrp  46016  xralrple2  46018  infxr  46030  infleinflem1  46033  infleinflem2  46034  infleinf  46035  xralrple4  46036  xralrple3  46037  recnnltrp  46040  rpgtrecnn  46043  xrralrecnnge  46053  rexabslelem  46080  infrnmptle  46085  supminfxr  46126  xrpnf  46147  iccshift  46182  iooshift  46186  ressiocsup  46218  ressioosup  46219  fsumnncl  46236  fmul01  46244  fmul01lt1lem1  46248  fmul01lt1lem2  46249  mccllem  46261  climrec  46267  climexp  46269  climneg  46274  limcrecl  46293  sumnnodd  46294  lptioo2  46295  lptioo1  46296  ltmod  46300  lptre2pt  46302  0ellimcdiv  46311  limclner  46313  fnlimcnv  46329  climinf2lem  46368  limsupubuzlem  46374  limsup10exlem  46434  limsupgtlem  46439  dfxlim2v  46509  xlimliminflimsup  46524  cncficcgt0  46550  cncfioobdlem  46558  ioodvbdlimc1lem1  46593  ioodvbdlimc1lem2  46594  ioodvbdlimc2lem  46596  dvdsn1add  46601  dvnxpaek  46604  dvnmul  46605  dvnprodlem1  46608  itgiccshift  46642  itgperiod  46643  sublevolico  46646  ismbl3  46648  ovolsplit  46650  ismbl4  46655  stoweidlem1  46663  stoweidlem11  46673  stoweidlem13  46675  stoweidlem26  46688  stoweidlem34  46696  stoweidlem38  46700  stoweidlem42  46704  stoweidlem51  46713  stoweidlem59  46721  stirlinglem5  46740  stirlinglem6  46741  stirlinglem7  46742  stirlinglem10  46745  stirlinglem11  46746  stirlinglem13  46748  stirlinglem15  46750  dirkercncflem1  46765  dirkercncflem4  46768  fourierdlem4  46773  fourierdlem10  46779  fourierdlem11  46780  fourierdlem15  46784  fourierdlem20  46789  fourierdlem25  46794  fourierdlem26  46795  fourierdlem30  46799  fourierdlem37  46806  fourierdlem39  46808  fourierdlem40  46809  fourierdlem41  46810  fourierdlem42  46811  fourierdlem44  46813  fourierdlem47  46815  fourierdlem48  46816  fourierdlem49  46817  fourierdlem50  46818  fourierdlem51  46819  fourierdlem52  46820  fourierdlem54  46822  fourierdlem60  46828  fourierdlem61  46829  fourierdlem63  46831  fourierdlem64  46832  fourierdlem65  46833  fourierdlem73  46841  fourierdlem74  46842  fourierdlem75  46843  fourierdlem76  46844  fourierdlem78  46846  fourierdlem79  46847  fourierdlem81  46849  fourierdlem84  46852  fourierdlem87  46855  fourierdlem92  46860  fourierdlem93  46861  fourierdlem101  46869  fourierdlem102  46870  fourierdlem103  46871  fourierdlem104  46872  fourierdlem111  46879  fourierdlem114  46882  sqwvfoura  46890  sqwvfourb  46891  fouriersw  46893  etransclem19  46915  etransclem23  46919  etransclem24  46920  etransclem25  46921  etransclem27  46923  etransclem32  46928  etransclem35  46931  etransclem48  46944  qndenserrnbllem  46956  ioorrnopnlem  46966  ioorrnopnxrlem  46968  fsumlesge0  47039  sge0cl  47043  sge0supre  47051  sge0less  47054  sge0gerp  47057  sge0ltfirp  47062  sge0le  47069  sge0ltfirpmpt  47070  sge0split  47071  sge0rpcpnf  47083  sge0ltfirpmpt2  47088  sge0isum  47089  sge0xaddlem1  47095  sge0pnffigtmpt  47102  sge0pnffsumgt  47104  sge0gtfsumgt  47105  sge0seq  47108  nnfoctbdjlem  47117  meassle  47125  meaiuninclem  47142  meaiininclem  47148  omeiunle  47179  omeiunltfirp  47181  carageniuncllem2  47184  carageniuncl  47185  omess0  47196  hoicvr  47210  ovnlerp  47224  ovnsubaddlem1  47232  hsphoidmvle2  47247  hoidmv1lelem2  47254  hoidmv1le  47256  hoidmvlelem1  47257  hoidmvlelem2  47258  hoidmvlelem3  47259  hoidmvlelem5  47261  ovnhoilem2  47264  ovnhoi  47265  hoidifhspdmvle  47282  hoiqssbllem2  47285  hspmbllem2  47289  hspmbllem3  47290  hspmbl  47291  vonioolem2  47343  vonicclem2  47346  smfaddlem1  47425  smflimlem2  47434  smflimlem4  47436  smfmullem1  47453  smfinflem  47479  smflimsuplem4  47485  smflimsuplem8  47489  chnsubseq  47544  perfectALTVlem2  48432  nnpw2blen  49305  itscnhlinecirc02plem1  49507  funcoppc3  49870  oppcuprcl2  49925  isinito3  50223