Theorem breqtrd 5114

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 5100	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5089

This theorem is referenced by:  breqtrrd  5116  breqtrid  5125  domunsn  9034  mapdom2  9055  phplem2  9108  mapfien2  9287  wemaplem2  9427  infdifsn  9541  cantnff  9558  ttrclss  9604  rnttrcl  9606  infxpenlem  9895  infmap2  10099  ssfin4  10192  canthp1lem1  10534  nqereq  10817  ltexnq  10857  ltbtwnnq  10860  add20  11620  mullt0  11627  ltm1  11954  recgt0  11958  prodgt0  11959  ltmul1a  11961  mulge0b  11983  recp1lt1  12011  recreclt  12012  ledivp1  12015  ledivp1i  12038  ltdivp1i  12039  eluzmn  12730  ltaddrp2d  12959  mul2lt0bi  12989  prodge0rd  12990  xleadd1a  13143  xov1plusxeqvd  13389  fz01en  13443  fzonmapblen  13599  fladdz  13717  flhalf  13722  fldiv  13752  modsubdir  13835  fzen2  13864  serle  13952  ltexp2a  14061  leexp2a  14067  exple1  14072  expubnd  14073  bernneq  14124  expmulnbnd  14130  discr1  14134  discr  14135  faclbnd6  14194  hashfz  14322  hashfun  14332  seqcoll  14359  sqeqd  15060  01sqrexlem7  15142  sqrtge0  15151  sqrtneglem  15160  abslt  15209  absle  15210  abstri  15225  rlimge0  15475  reccn2  15491  climaddc2  15530  isercolllem1  15559  caucvgrlem  15567  summolem2a  15609  isumge0  15660  fsumle  15693  fsumlt  15694  o1fsum  15707  supcvg  15750  expcnv  15758  geolim  15764  geolim2  15765  georeclim  15766  geo2lim  15769  mertenslem1  15778  mertens  15780  prodmolem2a  15828  efcllem  15971  ef0lem  15972  efgt0  15999  eftlub  16005  eflt  16013  sinbnd  16076  cosbnd  16077  ef01bndlem  16080  sin01gt0  16086  cos01gt0  16087  sin02gt0  16088  eirrlem  16100  rpnnen2lem11  16120  rpnnen2lem12  16121  ruclem11  16136  dvdssub2  16199  dvdsadd2b  16204  dvdsexp  16226  3dvds  16229  opoe  16261  bitsfzolem  16332  bitsinv1lem  16339  bezoutlem4  16440  dvdsgcd  16442  dvdsmulgcd  16454  bezoutr1  16467  nn0seqcvgd  16468  rpmulgcd2  16554  qredeq  16555  rpdvds  16558  prmind2  16583  divdenle  16647  hashdvds  16673  phimullem  16677  eulerthlem2  16680  prmdiveq  16684  prmdivdiv  16685  pythagtriplem4  16718  pythagtriplem10  16719  pythagtriplem19  16732  iserodd  16734  pcpre1  16741  pcadd2  16789  qexpz  16800  expnprm  16801  oddprmdvds  16802  pockthlem  16804  prmreclem2  16816  prmreclem3  16817  4sqlem7  16843  4sqlem10  16846  4sqlem11  16854  4sqlem12  16855  4sqlem14  16857  4sqlem15  16858  4sqlem16  16859  0ram  16919  ffthiso  17825  latmlej12  18372  qusgrp  19052  pgpfi1  19461  sylow1lem4  19467  sylow1lem5  19468  odcau  19470  pgpfi  19471  pgpssslw  19480  sylow3lem4  19496  sylow3lem6  19498  efgsfo  19605  frgp0  19626  odadd1  19714  odadd2  19715  odadd  19716  gexexlem  19718  lt6abl  19761  gsumzsubmcl  19784  pwsgsum  19848  dprd2dlem1  19909  dprd2d2  19912  ablfacrplem  19933  ablfacrp  19934  ablfacrp2  19935  ablfac1b  19938  ablfac1eu  19941  pgpfac1lem3a  19944  ablfaclem2  19954  dvdsrid  20239  dvdsrtr  20240  dvdsrneg  20242  unitmulcl  20252  unitgrp  20255  unitnegcl  20269  subrguss  20456  subrgunit  20459  isdrng2  20612  fidomndrnglem  20641  abvsubtri  20696  orngsqr  20735  ornglmulle  20736  orngrmulle  20737  orng0le1  20743  gzrngunit  21324  prmirredlem  21363  znidomb  21452  frlmgsum  21663  psrbaglesupp  21813  psdmul  22035  psdmvr  22038  invrvald  22545  psmetsym  24179  psmettri  24180  mettri2  24210  xmetsym  24216  xmettri  24220  prdsxmetlem  24237  xblss2ps  24270  xblss2  24271  blhalf  24274  xmsge0  24332  ngptgp  24505  nrginvrcnlem  24560  nmoeq0  24605  cnmet  24640  blcvx  24667  opnreen  24701  metdcnlem  24706  metdstri  24721  metdsle  24722  metnrmlem1  24729  metnrmlem3  24731  lebnumlem1  24841  pi1inv  24933  cphnmf  25076  ipge0  25079  ipcau2  25115  tcphcphlem1  25116  csbren  25280  minveclem2  25307  minveclem3  25310  ovolssnul  25369  ovolctb  25372  ovolunnul  25382  ovoliunlem1  25384  ovoliun2  25388  ovoliunnul  25389  ioombl1lem4  25443  uniioombllem3  25467  uniioombllem4  25468  uniioombllem5  25469  uniioombl  25471  volcn  25488  vitalilem2  25491  vitalilem5  25494  itg1lea  25594  mbfi1fseqlem6  25602  mbfi1flimlem  25604  itg2eqa  25627  itg2splitlem  25630  itg2split  25631  itg2monolem1  25632  itg2cnlem2  25644  iblabsr  25712  iblmulc2  25713  bddiblnc  25724  dveflem  25864  dvef  25865  dvferm2lem  25871  dvlip  25879  c1liplem1  25882  dveq0  25886  dvlt0  25891  dvivthlem1  25894  lhop1  25900  dvfsumle  25907  dvfsumleOLD  25908  dvfsumlem4  25917  dvfsumrlim3  25921  dvfsum2  25922  ftc1a  25925  ftc1lem4  25927  deg1add  25989  ply1divex  26023  ply1rem  26052  fta1glem2  26055  fta1blem  26057  ig1pdvds  26066  plyeq0lem  26096  dgrcolem2  26161  plydivlem4  26185  plyrem  26194  fta1lem  26196  aalioulem3  26223  aaliou2b  26230  aaliou3lem3  26233  aaliou3lem8  26234  ulmcn  26289  ulmdvlem1  26290  itgulm  26298  pserulm  26312  pserdvlem2  26319  abelthlem2  26323  abelthlem5  26326  abelthlem6  26327  abelthlem7  26329  abelthlem8  26330  abelthlem9  26331  sinq12gt0  26397  sinq34lt0t  26399  cosq14gt0  26400  cosq14ge0  26401  cos02pilt1  26416  efif1olem3  26434  argimgt0  26502  argimlt0  26503  logneg2  26505  logcnlem3  26534  logcnlem4  26535  logtayllem  26549  logtayl2  26552  cxpsqrtlem  26592  cxpsqrt  26593  cxpaddlelem  26642  abscxpbnd  26644  zrtdvds  26650  rtprmirr  26651  loglesqrt  26652  ang180lem2  26701  atanlogaddlem  26804  atanlogsublem  26806  atantan  26814  atans2  26822  atantayl  26828  leibpi  26833  log2tlbnd  26836  birthdaylem2  26843  birthdaylem3  26844  cxp2limlem  26867  jensenlem2  26879  jensen  26880  logdiflbnd  26886  emcllem2  26888  emcllem4  26890  harmonicbnd4  26902  fsumharmonic  26903  lgamgulmlem2  26921  lgamgulm2  26927  lgambdd  26928  lgamucov  26929  lgamcvglem  26931  lgamcvg2  26946  gamcvg  26947  wilthlem3  26961  basellem1  26972  basellem3  26974  basellem4  26975  fsumdvdsdiaglem  27074  dvdsppwf1o  27077  mpodvdsmulf1o  27085  dvdsmulf1o  27087  chteq0  27101  chtub  27104  chpub  27112  logfacubnd  27113  logfaclbnd  27114  logexprlim  27117  perfectlem2  27122  dchrfi  27147  bclbnd  27172  bposlem1  27176  bposlem3  27178  bposlem4  27179  bposlem6  27181  lgslem1  27189  lgsqrlem2  27239  lgsqrlem4  27241  lgseisenlem2  27268  lgsquadlem1  27272  lgsquadlem2  27273  lgsquad2lem1  27276  2sqlem3  27312  2sqlem4  27313  2sqlem8  27318  2sqlem11  27321  2sqcoprm  27327  2sqmod  27328  chebbnd1lem2  27362  chebbnd1lem3  27363  chtppilimlem1  27365  chpchtlim  27371  vmadivsum  27374  vmadivsumb  27375  rpvmasumlem  27379  dchrisumlem2  27382  dchrmusum2  27386  dchrvmasumlem2  27390  dchrvmasumlem3  27391  dchrisum0flblem2  27401  dchrisum0fno1  27403  dchrisum0re  27405  dchrisum0lem1  27408  dchrisum0lem2a  27409  mudivsum  27422  mulogsumlem  27423  mulog2sumlem2  27427  vmalogdivsum2  27430  selberglem2  27438  selbergb  27441  selberg2b  27444  logdivbnd  27448  selberg3lem1  27449  selberg3lem2  27450  selberg4lem1  27452  pntrmax  27456  pntrlog2bndlem2  27470  pntrlog2bndlem3  27471  pntrlog2bndlem5  27473  pntrlog2bndlem6a  27474  pntrlog2bndlem6  27475  pntrlog2bnd  27476  pntpbnd1a  27477  pntpbnd1  27478  pntpbnd2  27479  pntibndlem1  27481  pntibndlem2  27483  pntlemb  27489  pntlemq  27493  pntlemr  27494  pntlemj  27495  pntlemk  27498  qabvle  27517  padicabvcxp  27524  ostth2lem2  27526  ostth2lem3  27527  ostth2lem4  27528  ostth3  27530  addsuniflem  27898  negsid  27937  negsunif  27951  mulsuniflem  28042  sltmul2  28064  precsexlem9  28107  absmuls  28136  zscut  28285  addhalfcut  28333  pw2cut2  28336  zs12ge0  28347  legtrid  28523  legov3  28530  krippenlem  28622  mideulem2  28666  midex  28669  opphllem5  28683  opphllem6  28684  opphl  28686  lmieu  28716  lmiisolem  28728  ttgcontlem1  28817  colinearalglem4  28841  axpaschlem  28872  axcontlem7  28902  nbfusgrlevtxm2  29310  clwlksndivn  30017  eucrct2eupth  30176  nvge0  30604  smcnlem  30628  nmoub3i  30704  nmoub2i  30705  nmlno0lem  30724  minvecolem2  30806  htthlem  30848  norm3dif2  31082  bcs2  31113  chscllem2  31569  eigposi  31767  nmopub2tALT  31840  nmfnleub2  31857  nmlnop0iALT  31926  riesz1  31996  cnlnadjlem2  31999  nmopcoadji  32032  leopsq  32060  leopmul  32065  leopnmid  32069  nmopleid  32070  opsqrlem6  32076  0leopj  32117  hstle1  32157  strlem3a  32183  mdslmd4i  32264  cvexchlem  32299  cdj1i  32364  unidifsnel  32467  unidifsnne  32468  le2halvesd  32691  xlt2addrd  32694  fsumub  32766  sgnmulsgp  32781  2exple2exp  32783  oexpled  32785  wrdt2ind  32890  xrge0tsmsd  33010  fzto1st1  33039  cycpmco2lem4  33066  cycpmco2lem6  33068  cyc3conja  33094  archiabllem1a  33128  archiabllem2a  33131  archiabllem2c  33132  rprmdvdsprod  33467  1arithidomlem1  33468  1arithidomlem2  33469  1arithidom  33470  ply1dg3rt0irred  33514  mplvrpmrhm  33545  exsslsb  33577  fedgmullem1  33610  fedgmullem2  33611  fldsdrgfldext2  33643  fldextrspundgdvdslem  33661  fldextrspundgdvds  33662  fldext2rspun  33663  extdgfialglem2  33674  algextdeglem8  33705  rtelextdg2lem  33707  constrext2chnlem  33731  cos9thpiminplylem1  33763  cos9thpiminplylem2  33764  metideq  33874  metider  33875  sqsscirc1  33889  esummono  34035  esumpad2  34037  esumle  34039  esumlef  34043  esumcst  34044  esumrnmpt2  34049  esum2d  34074  aean  34225  dya2ub  34251  dya2icoseg  34258  omssubadd  34281  inelcarsg  34292  carsgsigalem  34296  carsggect  34299  carsgclctunlem2  34300  eulerpartlemb  34349  fibp1  34382  signsplypnf  34531  signsply0  34532  fdvposlt  34580  fdvposle  34582  reprgt  34602  logdivsqrle  34631  hgt750lemb  34637  hgt750leme  34639  tgoldbachgtde  34641  subfacval3  35179  sconnpht2  35228  sconnpi1  35229  resconn  35236  snmlff  35319  sinccvglem  35662  faclimlem2  35734  btwnouttr2  36013  weiunpo  36456  dnibndlem5  36473  dnibndlem7  36475  dnibndlem8  36476  dnibndlem9  36477  dnibndlem10  36478  dnibnd  36482  knoppcnlem4  36487  knoppcnlem9  36492  unbdqndv2lem1  36500  unbdqndv2lem2  36501  knoppndvlem11  36513  knoppndvlem12  36514  knoppndvlem14  36516  knoppndvlem15  36517  knoppndvlem17  36519  knoppndvlem18  36520  knoppndvlem19  36521  knoppndvlem21  36523  ltflcei  37605  poimirlem9  37626  poimirlem26  37643  poimirlem27  37644  poimirlem29  37646  heicant  37652  mblfinlem2  37655  mblfinlem3  37656  mblfinlem4  37657  volsupnfl  37662  itg2addnclem  37668  itg2addnclem3  37670  iblmulc2nc  37682  ftc1cnnclem  37688  ftc1anclem6  37695  ftc1anclem7  37696  ftc1anclem8  37697  ftc2nc  37699  dvasin  37701  geomcau  37756  bfplem2  37820  rrncmslem  37829  rrnequiv  37832  lsatcvatlem  39045  islshpcv  39049  atlatmstc  39315  cvlsupr7  39344  cvrval3  39409  cvrval5  39411  cvrexchlem  39415  atcvrj1  39427  cvrat3  39438  cvrat4  39439  atbtwn  39442  1cvratex  39469  hlatexch4  39477  3atlem1  39479  3atlem2  39480  atcvrlln2  39515  atcvrlln  39516  lplnllnneN  39552  llncvrlpln2  39553  4atlem3b  39594  lplncvrlvol2  39611  dalemswapyz  39652  dalemswapyzps  39686  dalem25  39694  dalem39  39707  dalem58  39726  dalem59  39727  lneq2at  39774  lncvrat  39778  dalawlem2  39868  dalawlem3  39869  dalawlem4  39870  dalawlem6  39872  dalawlem9  39875  dalawlem11  39877  dalawlem12  39878  lhpocnle  40012  lhpmcvr3  40021  lhpmcvr5N  40023  lhpmcvr6N  40024  4atexlemunv  40062  4atexlemc  40065  4atexlemex2  40067  lautm  40090  cdlemc2  40188  cdleme5  40236  cdleme11j  40263  cdleme16b  40275  cdlemednpq  40295  cdleme19e  40303  cdleme20i  40313  cdleme22a  40336  cdleme22cN  40338  cdleme22d  40339  cdleme22e  40340  cdleme22eALTN  40341  cdleme22f  40342  cdleme23c  40347  cdleme30a  40374  cdleme35a  40444  cdleme35b  40446  cdleme42h  40478  cdlemeg46rgv  40524  cdlemg8b  40624  cdlemg12e  40643  cdlemg13a  40647  cdlemg17pq  40668  cdlemg18c  40676  cdlemg19  40680  cdlemg21  40682  cdlemg31d  40696  cdlemg33a  40702  tendoid  40769  cdlemk4  40830  cdlemki  40837  cdlemk10  40839  cdlemksv2  40843  cdlemk12  40846  cdlemk14  40850  cdlemk15  40851  cdlemk1u  40855  cdlemk5u  40857  cdlemk12u  40868  cdlemk45  40943  cdlemk48  40946  dia2dimlem1  41060  dia2dimlem2  41061  dia2dimlem3  41062  cdlemm10N  41114  cdlemn2  41191  dihjustlem  41212  dihglbcpreN  41296  dihmeetlem3N  41301  nnproddivdvdsd  41990  lcmineqlem17  42035  lcmineqlem18  42036  3lexlogpow2ineq1  42048  3lexlogpow2ineq2  42049  3lexlogpow5ineq5  42050  aks4d1p1p3  42059  aks4d1p1p2  42060  aks4d1p1p4  42061  aks4d1p1p5  42065  aks4d1p1  42066  aks4d1p3  42068  aks4d1p8  42077  posbezout  42090  primrootspoweq0  42096  aks6d1c1  42106  hashscontpow1  42111  aks6d1c4  42114  aks6d1c2  42120  aks6d1c5lem1  42126  aks6d1c5lem3  42127  aks6d1c5lem2  42128  deg1gprod  42130  sticksstones7  42142  sticksstones10  42145  sticksstones12  42148  sticksstones22  42158  aks6d1c6lem1  42160  aks6d1c6lem3  42162  aks6d1c6lem4  42163  bcled  42168  bcle2d  42169  aks6d1c7lem1  42170  unitscyglem4  42188  aks5lem7  42190  aks5  42194  explt1d  42313  mulgt0b2d  42468  evlselv  42577  dffltz  42624  fltdvdsabdvdsc  42628  fltaccoprm  42630  fltabcoprm  42632  flt4lem5elem  42641  flt4lem7  42649  fltnlta  42653  irrapxlem1  42812  pell1qrgaplem  42863  pell1qrgap  42864  monotoddzzfi  42932  jm2.24nn  42949  congtr  42955  congmul  42957  congsub  42960  fzmaxdif  42971  acongeq  42973  jm2.20nn  42987  jm2.25  42989  hbtlem4  43116  dgrsub2  43125  mpaaeu  43140  idomsubgmo  43183  iscard4  43523  sqrtcvallem4  43629  leeq2d  44148  int-sqgeq0d  44176  int-ineqmvtd  44181  cvgdvgrat  44303  radcnvrat  44304  hashnzfzclim  44312  dvconstbi  44324  binomcxplemdvbinom  44343  isosctrlem1ALT  44923  mulltgt0  45016  rnmptbd2lem  45242  oddfl  45276  2timesgt  45286  lt3addmuld  45299  lt4addmuld  45304  supxrgere  45329  supxrgelem  45333  supxrge  45334  xadd0ge2  45337  infrpge  45347  xrlexaddrp  45348  xralrple2  45350  infxr  45362  infleinflem1  45365  infleinflem2  45366  infleinf  45367  xralrple4  45368  xralrple3  45369  recnnltrp  45372  rpgtrecnn  45375  xrralrecnnge  45385  rexabslelem  45413  infrnmptle  45418  supminfxr  45459  xrpnf  45480  iccshift  45515  iooshift  45519  ressiocsup  45551  ressioosup  45552  fsumnncl  45569  fmul01  45577  fmul01lt1lem1  45581  fmul01lt1lem2  45582  mccllem  45594  climrec  45600  climexp  45602  climneg  45607  limcrecl  45626  sumnnodd  45627  lptioo2  45628  lptioo1  45629  ltmod  45633  lptre2pt  45635  0ellimcdiv  45644  limclner  45646  fnlimcnv  45662  climinf2lem  45701  limsupubuzlem  45707  limsup10exlem  45767  limsupgtlem  45772  dfxlim2v  45842  xlimliminflimsup  45857  cncficcgt0  45883  cncfioobdlem  45891  ioodvbdlimc1lem1  45926  ioodvbdlimc1lem2  45927  ioodvbdlimc2lem  45929  dvdsn1add  45934  dvnxpaek  45937  dvnmul  45938  dvnprodlem1  45941  itgiccshift  45975  itgperiod  45976  sublevolico  45979  ismbl3  45981  ovolsplit  45983  ismbl4  45988  stoweidlem1  45996  stoweidlem11  46006  stoweidlem13  46008  stoweidlem26  46021  stoweidlem34  46029  stoweidlem38  46033  stoweidlem42  46037  stoweidlem51  46046  stoweidlem59  46054  stirlinglem5  46073  stirlinglem6  46074  stirlinglem7  46075  stirlinglem10  46078  stirlinglem11  46079  stirlinglem13  46081  stirlinglem15  46083  dirkercncflem1  46098  dirkercncflem4  46101  fourierdlem4  46106  fourierdlem10  46112  fourierdlem11  46113  fourierdlem15  46117  fourierdlem20  46122  fourierdlem25  46127  fourierdlem26  46128  fourierdlem30  46132  fourierdlem37  46139  fourierdlem39  46141  fourierdlem40  46142  fourierdlem41  46143  fourierdlem42  46144  fourierdlem44  46146  fourierdlem47  46148  fourierdlem48  46149  fourierdlem49  46150  fourierdlem50  46151  fourierdlem51  46152  fourierdlem52  46153  fourierdlem54  46155  fourierdlem60  46161  fourierdlem61  46162  fourierdlem63  46164  fourierdlem64  46165  fourierdlem65  46166  fourierdlem73  46174  fourierdlem74  46175  fourierdlem75  46176  fourierdlem76  46177  fourierdlem78  46179  fourierdlem79  46180  fourierdlem81  46182  fourierdlem84  46185  fourierdlem87  46188  fourierdlem92  46193  fourierdlem93  46194  fourierdlem101  46202  fourierdlem102  46203  fourierdlem103  46204  fourierdlem104  46205  fourierdlem111  46212  fourierdlem114  46215  sqwvfoura  46223  sqwvfourb  46224  fouriersw  46226  etransclem19  46248  etransclem23  46252  etransclem24  46253  etransclem25  46254  etransclem27  46256  etransclem32  46261  etransclem35  46264  etransclem48  46277  qndenserrnbllem  46289  ioorrnopnlem  46299  ioorrnopnxrlem  46301  fsumlesge0  46372  sge0cl  46376  sge0supre  46384  sge0less  46387  sge0gerp  46390  sge0ltfirp  46395  sge0le  46402  sge0ltfirpmpt  46403  sge0split  46404  sge0rpcpnf  46416  sge0ltfirpmpt2  46421  sge0isum  46422  sge0xaddlem1  46428  sge0pnffigtmpt  46435  sge0pnffsumgt  46437  sge0gtfsumgt  46438  sge0seq  46441  nnfoctbdjlem  46450  meassle  46458  meaiuninclem  46475  meaiininclem  46481  omeiunle  46512  omeiunltfirp  46514  carageniuncllem2  46517  carageniuncl  46518  omess0  46529  hoicvr  46543  ovnlerp  46557  ovnsubaddlem1  46565  hsphoidmvle2  46580  hoidmv1lelem2  46587  hoidmv1le  46589  hoidmvlelem1  46590  hoidmvlelem2  46591  hoidmvlelem3  46592  hoidmvlelem5  46594  ovnhoilem2  46597  ovnhoi  46598  hoidifhspdmvle  46615  hoiqssbllem2  46618  hspmbllem2  46622  hspmbllem3  46623  hspmbl  46624  vonioolem2  46676  vonicclem2  46679  smfaddlem1  46758  smflimlem2  46767  smflimlem4  46769  smfmullem1  46786  smfinflem  46812  smflimsuplem4  46818  smflimsuplem8  46822  perfectALTVlem2  47720  nnpw2blen  48579  itscnhlinecirc02plem1  48781  funcoppc3  49146  oppcuprcl2  49201  isinito3  49499