Theorem breqtrd 5128

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtrrd  5130  breqtrid  5139  domunsn  9068  mapdom2  9089  phplem2  9146  mapfien2  9336  wemaplem2  9476  infdifsn  9586  cantnff  9603  ttrclss  9649  rnttrcl  9651  infxpenlem  9942  infmap2  10146  ssfin4  10239  canthp1lem1  10581  nqereq  10864  ltexnq  10904  ltbtwnnq  10907  add20  11666  mullt0  11673  ltm1  12000  recgt0  12004  prodgt0  12005  ltmul1a  12007  mulge0b  12029  recp1lt1  12057  recreclt  12058  ledivp1  12061  ledivp1i  12084  ltdivp1i  12085  eluzmn  12776  ltaddrp2d  13005  mul2lt0bi  13035  prodge0rd  13036  xleadd1a  13189  xov1plusxeqvd  13435  fz01en  13489  fzonmapblen  13645  fladdz  13763  flhalf  13768  fldiv  13798  modsubdir  13881  fzen2  13910  serle  13998  ltexp2a  14107  leexp2a  14113  exple1  14118  expubnd  14119  bernneq  14170  expmulnbnd  14176  discr1  14180  discr  14181  faclbnd6  14240  hashfz  14368  hashfun  14378  seqcoll  14405  sqeqd  15108  01sqrexlem7  15190  sqrtge0  15199  sqrtneglem  15208  abslt  15257  absle  15258  abstri  15273  rlimge0  15523  reccn2  15539  climaddc2  15578  isercolllem1  15607  caucvgrlem  15615  summolem2a  15657  isumge0  15708  fsumle  15741  fsumlt  15742  o1fsum  15755  supcvg  15798  expcnv  15806  geolim  15812  geolim2  15813  georeclim  15814  geo2lim  15817  mertenslem1  15826  mertens  15828  prodmolem2a  15876  efcllem  16019  ef0lem  16020  efgt0  16047  eftlub  16053  eflt  16061  sinbnd  16124  cosbnd  16125  ef01bndlem  16128  sin01gt0  16134  cos01gt0  16135  sin02gt0  16136  eirrlem  16148  rpnnen2lem11  16168  rpnnen2lem12  16169  ruclem11  16184  dvdssub2  16247  dvdsadd2b  16252  dvdsexp  16274  3dvds  16277  opoe  16309  bitsfzolem  16380  bitsinv1lem  16387  bezoutlem4  16488  dvdsgcd  16490  dvdsmulgcd  16502  bezoutr1  16515  nn0seqcvgd  16516  rpmulgcd2  16602  qredeq  16603  rpdvds  16606  prmind2  16631  divdenle  16695  hashdvds  16721  phimullem  16725  eulerthlem2  16728  prmdiveq  16732  prmdivdiv  16733  pythagtriplem4  16766  pythagtriplem10  16767  pythagtriplem19  16780  iserodd  16782  pcpre1  16789  pcadd2  16837  qexpz  16848  expnprm  16849  oddprmdvds  16850  pockthlem  16852  prmreclem2  16864  prmreclem3  16865  4sqlem7  16891  4sqlem10  16894  4sqlem11  16902  4sqlem12  16903  4sqlem14  16905  4sqlem15  16906  4sqlem16  16907  0ram  16967  ffthiso  17873  latmlej12  18420  qusgrp  19100  pgpfi1  19509  sylow1lem4  19515  sylow1lem5  19516  odcau  19518  pgpfi  19519  pgpssslw  19528  sylow3lem4  19544  sylow3lem6  19546  efgsfo  19653  frgp0  19674  odadd1  19762  odadd2  19763  odadd  19764  gexexlem  19766  lt6abl  19809  gsumzsubmcl  19832  pwsgsum  19896  dprd2dlem1  19957  dprd2d2  19960  ablfacrplem  19981  ablfacrp  19982  ablfacrp2  19983  ablfac1b  19986  ablfac1eu  19989  pgpfac1lem3a  19992  ablfaclem2  20002  dvdsrid  20287  dvdsrtr  20288  dvdsrneg  20290  unitmulcl  20300  unitgrp  20303  unitnegcl  20317  subrguss  20507  subrgunit  20510  isdrng2  20663  fidomndrnglem  20692  abvsubtri  20747  orngsqr  20786  ornglmulle  20787  orngrmulle  20788  orng0le1  20794  gzrngunit  21375  prmirredlem  21414  znidomb  21503  frlmgsum  21714  psrbaglesupp  21864  psdmul  22086  psdmvr  22089  invrvald  22596  psmetsym  24231  psmettri  24232  mettri2  24262  xmetsym  24268  xmettri  24272  prdsxmetlem  24289  xblss2ps  24322  xblss2  24323  blhalf  24326  xmsge0  24384  ngptgp  24557  nrginvrcnlem  24612  nmoeq0  24657  cnmet  24692  blcvx  24719  opnreen  24753  metdcnlem  24758  metdstri  24773  metdsle  24774  metnrmlem1  24781  metnrmlem3  24783  lebnumlem1  24893  pi1inv  24985  cphnmf  25128  ipge0  25131  ipcau2  25167  tcphcphlem1  25168  csbren  25332  minveclem2  25359  minveclem3  25362  ovolssnul  25421  ovolctb  25424  ovolunnul  25434  ovoliunlem1  25436  ovoliun2  25440  ovoliunnul  25441  ioombl1lem4  25495  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  uniioombl  25523  volcn  25540  vitalilem2  25543  vitalilem5  25546  itg1lea  25646  mbfi1fseqlem6  25654  mbfi1flimlem  25656  itg2eqa  25679  itg2splitlem  25682  itg2split  25683  itg2monolem1  25684  itg2cnlem2  25696  iblabsr  25764  iblmulc2  25765  bddiblnc  25776  dveflem  25916  dvef  25917  dvferm2lem  25923  dvlip  25931  c1liplem1  25934  dveq0  25938  dvlt0  25943  dvivthlem1  25946  lhop1  25952  dvfsumle  25959  dvfsumleOLD  25960  dvfsumlem4  25969  dvfsumrlim3  25973  dvfsum2  25974  ftc1a  25977  ftc1lem4  25979  deg1add  26041  ply1divex  26075  ply1rem  26104  fta1glem2  26107  fta1blem  26109  ig1pdvds  26118  plyeq0lem  26148  dgrcolem2  26213  plydivlem4  26237  plyrem  26246  fta1lem  26248  aalioulem3  26275  aaliou2b  26282  aaliou3lem3  26285  aaliou3lem8  26286  ulmcn  26341  ulmdvlem1  26342  itgulm  26350  pserulm  26364  pserdvlem2  26371  abelthlem2  26375  abelthlem5  26378  abelthlem6  26379  abelthlem7  26381  abelthlem8  26382  abelthlem9  26383  sinq12gt0  26449  sinq34lt0t  26451  cosq14gt0  26452  cosq14ge0  26453  cos02pilt1  26468  efif1olem3  26486  argimgt0  26554  argimlt0  26555  logneg2  26557  logcnlem3  26586  logcnlem4  26587  logtayllem  26601  logtayl2  26604  cxpsqrtlem  26644  cxpsqrt  26645  cxpaddlelem  26694  abscxpbnd  26696  zrtdvds  26702  rtprmirr  26703  loglesqrt  26704  ang180lem2  26753  atanlogaddlem  26856  atanlogsublem  26858  atantan  26866  atans2  26874  atantayl  26880  leibpi  26885  log2tlbnd  26888  birthdaylem2  26895  birthdaylem3  26896  cxp2limlem  26919  jensenlem2  26931  jensen  26932  logdiflbnd  26938  emcllem2  26940  emcllem4  26942  harmonicbnd4  26954  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulm2  26979  lgambdd  26980  lgamucov  26981  lgamcvglem  26983  lgamcvg2  26998  gamcvg  26999  wilthlem3  27013  basellem1  27024  basellem3  27026  basellem4  27027  fsumdvdsdiaglem  27126  dvdsppwf1o  27129  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chteq0  27153  chtub  27156  chpub  27164  logfacubnd  27165  logfaclbnd  27166  logexprlim  27169  perfectlem2  27174  dchrfi  27199  bclbnd  27224  bposlem1  27228  bposlem3  27230  bposlem4  27231  bposlem6  27233  lgslem1  27241  lgsqrlem2  27291  lgsqrlem4  27293  lgseisenlem2  27320  lgsquadlem1  27324  lgsquadlem2  27325  lgsquad2lem1  27328  2sqlem3  27364  2sqlem4  27365  2sqlem8  27370  2sqlem11  27373  2sqcoprm  27379  2sqmod  27380  chebbnd1lem2  27414  chebbnd1lem3  27415  chtppilimlem1  27417  chpchtlim  27423  vmadivsum  27426  vmadivsumb  27427  rpvmasumlem  27431  dchrisumlem2  27434  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumlem3  27443  dchrisum0flblem2  27453  dchrisum0fno1  27455  dchrisum0re  27457  dchrisum0lem1  27460  dchrisum0lem2a  27461  mudivsum  27474  mulogsumlem  27475  mulog2sumlem2  27479  vmalogdivsum2  27482  selberglem2  27490  selbergb  27493  selberg2b  27496  logdivbnd  27500  selberg3lem1  27501  selberg3lem2  27502  selberg4lem1  27504  pntrmax  27508  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem5  27525  pntrlog2bndlem6a  27526  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem1  27533  pntibndlem2  27535  pntlemb  27541  pntlemq  27545  pntlemr  27546  pntlemj  27547  pntlemk  27550  qabvle  27569  padicabvcxp  27576  ostth2lem2  27578  ostth2lem3  27579  ostth2lem4  27580  ostth3  27582  addsuniflem  27948  negsid  27987  negsunif  28001  mulsuniflem  28092  sltmul2  28114  precsexlem9  28157  absmuls  28186  zscut  28335  addhalfcut  28382  zs12ge0  28395  legtrid  28571  legov3  28578  krippenlem  28670  mideulem2  28714  midex  28717  opphllem5  28731  opphllem6  28732  opphl  28734  lmieu  28764  lmiisolem  28776  ttgcontlem1  28865  colinearalglem4  28889  axpaschlem  28920  axcontlem7  28950  nbfusgrlevtxm2  29358  clwlksndivn  30065  eucrct2eupth  30224  nvge0  30652  smcnlem  30676  nmoub3i  30752  nmoub2i  30753  nmlno0lem  30772  minvecolem2  30854  htthlem  30896  norm3dif2  31130  bcs2  31161  chscllem2  31617  eigposi  31815  nmopub2tALT  31888  nmfnleub2  31905  nmlnop0iALT  31974  riesz1  32044  cnlnadjlem2  32047  nmopcoadji  32080  leopsq  32108  leopmul  32113  leopnmid  32117  nmopleid  32118  opsqrlem6  32124  0leopj  32165  hstle1  32205  strlem3a  32231  mdslmd4i  32312  cvexchlem  32347  cdj1i  32412  unidifsnel  32514  unidifsnne  32515  le2halvesd  32729  xlt2addrd  32732  fsumub  32803  sgnmulsgp  32818  2exple2exp  32820  oexpled  32822  wrdt2ind  32925  xrge0tsmsd  33045  fzto1st1  33074  cycpmco2lem4  33101  cycpmco2lem6  33103  cyc3conja  33129  archiabllem1a  33160  archiabllem2a  33163  archiabllem2c  33164  rprmdvdsprod  33498  1arithidomlem1  33499  1arithidomlem2  33500  1arithidom  33501  ply1dg3rt0irred  33544  exsslsb  33585  fedgmullem1  33618  fedgmullem2  33619  fldsdrgfldext2  33651  fldextrspundgdvdslem  33668  fldextrspundgdvds  33669  fldext2rspun  33670  algextdeglem8  33707  rtelextdg2lem  33709  constrext2chnlem  33733  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  metideq  33876  metider  33877  sqsscirc1  33891  esummono  34037  esumpad2  34039  esumle  34041  esumlef  34045  esumcst  34046  esumrnmpt2  34051  esum2d  34076  aean  34227  dya2ub  34254  dya2icoseg  34261  omssubadd  34284  inelcarsg  34295  carsgsigalem  34299  carsggect  34302  carsgclctunlem2  34303  eulerpartlemb  34352  fibp1  34385  signsplypnf  34534  signsply0  34535  fdvposlt  34583  fdvposle  34585  reprgt  34605  logdivsqrle  34634  hgt750lemb  34640  hgt750leme  34642  tgoldbachgtde  34644  subfacval3  35169  sconnpht2  35218  sconnpi1  35219  resconn  35226  snmlff  35309  sinccvglem  35652  faclimlem2  35724  btwnouttr2  36003  weiunpo  36446  dnibndlem5  36463  dnibndlem7  36465  dnibndlem8  36466  dnibndlem9  36467  dnibndlem10  36468  dnibnd  36472  knoppcnlem4  36477  knoppcnlem9  36482  unbdqndv2lem1  36490  unbdqndv2lem2  36491  knoppndvlem11  36503  knoppndvlem12  36504  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem17  36509  knoppndvlem18  36510  knoppndvlem19  36511  knoppndvlem21  36513  ltflcei  37595  poimirlem9  37616  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  heicant  37642  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  volsupnfl  37652  itg2addnclem  37658  itg2addnclem3  37660  iblmulc2nc  37672  ftc1cnnclem  37678  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  ftc2nc  37689  dvasin  37691  geomcau  37746  bfplem2  37810  rrncmslem  37819  rrnequiv  37822  lsatcvatlem  39035  islshpcv  39039  atlatmstc  39305  cvlsupr7  39334  cvrval3  39400  cvrval5  39402  cvrexchlem  39406  atcvrj1  39418  cvrat3  39429  cvrat4  39430  atbtwn  39433  1cvratex  39460  hlatexch4  39468  3atlem1  39470  3atlem2  39471  atcvrlln2  39506  atcvrlln  39507  lplnllnneN  39543  llncvrlpln2  39544  4atlem3b  39585  lplncvrlvol2  39602  dalemswapyz  39643  dalemswapyzps  39677  dalem25  39685  dalem39  39698  dalem58  39717  dalem59  39718  lneq2at  39765  lncvrat  39769  dalawlem2  39859  dalawlem3  39860  dalawlem4  39861  dalawlem6  39863  dalawlem9  39866  dalawlem11  39868  dalawlem12  39869  lhpocnle  40003  lhpmcvr3  40012  lhpmcvr5N  40014  lhpmcvr6N  40015  4atexlemunv  40053  4atexlemc  40056  4atexlemex2  40058  lautm  40081  cdlemc2  40179  cdleme5  40227  cdleme11j  40254  cdleme16b  40266  cdlemednpq  40286  cdleme19e  40294  cdleme20i  40304  cdleme22a  40327  cdleme22cN  40329  cdleme22d  40330  cdleme22e  40331  cdleme22eALTN  40332  cdleme22f  40333  cdleme23c  40338  cdleme30a  40365  cdleme35a  40435  cdleme35b  40437  cdleme42h  40469  cdlemeg46rgv  40515  cdlemg8b  40615  cdlemg12e  40634  cdlemg13a  40638  cdlemg17pq  40659  cdlemg18c  40667  cdlemg19  40671  cdlemg21  40673  cdlemg31d  40687  cdlemg33a  40693  tendoid  40760  cdlemk4  40821  cdlemki  40828  cdlemk10  40830  cdlemksv2  40834  cdlemk12  40837  cdlemk14  40841  cdlemk15  40842  cdlemk1u  40846  cdlemk5u  40848  cdlemk12u  40859  cdlemk45  40934  cdlemk48  40937  dia2dimlem1  41051  dia2dimlem2  41052  dia2dimlem3  41053  cdlemm10N  41105  cdlemn2  41182  dihjustlem  41203  dihglbcpreN  41287  dihmeetlem3N  41292  nnproddivdvdsd  41981  lcmineqlem17  42026  lcmineqlem18  42027  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p3  42059  aks4d1p8  42068  posbezout  42081  primrootspoweq0  42087  aks6d1c1  42097  hashscontpow1  42102  aks6d1c4  42105  aks6d1c2  42111  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  sticksstones7  42133  sticksstones10  42136  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem1  42151  aks6d1c6lem3  42153  aks6d1c6lem4  42154  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  unitscyglem4  42179  aks5lem7  42181  aks5  42185  explt1d  42304  mulgt0b2d  42459  evlselv  42568  dffltz  42615  fltdvdsabdvdsc  42619  fltaccoprm  42621  fltabcoprm  42623  flt4lem5elem  42632  flt4lem7  42640  fltnlta  42644  irrapxlem1  42803  pell1qrgaplem  42854  pell1qrgap  42855  monotoddzzfi  42924  jm2.24nn  42941  congtr  42947  congmul  42949  congsub  42952  fzmaxdif  42963  acongeq  42965  jm2.20nn  42979  jm2.25  42981  hbtlem4  43108  dgrsub2  43117  mpaaeu  43132  idomsubgmo  43175  iscard4  43515  sqrtcvallem4  43621  leeq2d  44140  int-sqgeq0d  44168  int-ineqmvtd  44173  cvgdvgrat  44295  radcnvrat  44296  hashnzfzclim  44304  dvconstbi  44316  binomcxplemdvbinom  44335  isosctrlem1ALT  44916  mulltgt0  45009  rnmptbd2lem  45235  oddfl  45269  2timesgt  45279  lt3addmuld  45292  lt4addmuld  45297  supxrgere  45322  supxrgelem  45326  supxrge  45327  xadd0ge2  45330  infrpge  45340  xrlexaddrp  45341  xralrple2  45343  infxr  45356  infleinflem1  45359  infleinflem2  45360  infleinf  45361  xralrple4  45362  xralrple3  45363  recnnltrp  45366  rpgtrecnn  45369  xrralrecnnge  45379  rexabslelem  45407  infrnmptle  45412  supminfxr  45453  xrpnf  45474  iccshift  45509  iooshift  45513  ressiocsup  45545  ressioosup  45546  fsumnncl  45563  fmul01  45571  fmul01lt1lem1  45575  fmul01lt1lem2  45576  mccllem  45588  climrec  45594  climexp  45596  climneg  45601  limcrecl  45620  sumnnodd  45621  lptioo2  45622  lptioo1  45623  ltmod  45629  lptre2pt  45631  0ellimcdiv  45640  limclner  45642  fnlimcnv  45658  climinf2lem  45697  limsupubuzlem  45703  limsup10exlem  45763  limsupgtlem  45768  dfxlim2v  45838  xlimliminflimsup  45853  cncficcgt0  45879  cncfioobdlem  45887  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvdsn1add  45930  dvnxpaek  45933  dvnmul  45934  dvnprodlem1  45937  itgiccshift  45971  itgperiod  45972  sublevolico  45975  ismbl3  45977  ovolsplit  45979  ismbl4  45984  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem26  46017  stoweidlem34  46025  stoweidlem38  46029  stoweidlem42  46033  stoweidlem51  46042  stoweidlem59  46050  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem13  46077  stirlinglem15  46079  dirkercncflem1  46094  dirkercncflem4  46097  fourierdlem4  46102  fourierdlem10  46108  fourierdlem11  46109  fourierdlem15  46113  fourierdlem20  46118  fourierdlem25  46123  fourierdlem26  46124  fourierdlem30  46128  fourierdlem37  46135  fourierdlem39  46137  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem44  46142  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem51  46148  fourierdlem52  46149  fourierdlem54  46151  fourierdlem60  46157  fourierdlem61  46158  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem81  46178  fourierdlem84  46181  fourierdlem87  46184  fourierdlem92  46189  fourierdlem93  46190  fourierdlem101  46198  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem114  46211  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  etransclem19  46244  etransclem23  46248  etransclem24  46249  etransclem25  46250  etransclem27  46252  etransclem32  46257  etransclem35  46260  etransclem48  46273  qndenserrnbllem  46285  ioorrnopnlem  46295  ioorrnopnxrlem  46297  fsumlesge0  46368  sge0cl  46372  sge0supre  46380  sge0less  46383  sge0gerp  46386  sge0ltfirp  46391  sge0le  46398  sge0ltfirpmpt  46399  sge0split  46400  sge0rpcpnf  46412  sge0ltfirpmpt2  46417  sge0isum  46418  sge0xaddlem1  46424  sge0pnffigtmpt  46431  sge0pnffsumgt  46433  sge0gtfsumgt  46434  sge0seq  46437  nnfoctbdjlem  46446  meassle  46454  meaiuninclem  46471  meaiininclem  46477  omeiunle  46508  omeiunltfirp  46510  carageniuncllem2  46513  carageniuncl  46514  omess0  46525  hoicvr  46539  ovnlerp  46553  ovnsubaddlem1  46561  hsphoidmvle2  46576  hoidmv1lelem2  46583  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem5  46590  ovnhoilem2  46593  ovnhoi  46594  hoidifhspdmvle  46611  hoiqssbllem2  46614  hspmbllem2  46618  hspmbllem3  46619  hspmbl  46620  vonioolem2  46672  vonicclem2  46675  smfaddlem1  46754  smflimlem2  46763  smflimlem4  46765  smfmullem1  46782  smfinflem  46808  smflimsuplem4  46814  smflimsuplem8  46818  perfectALTVlem2  47716  nnpw2blen  48562  itscnhlinecirc02plem1  48764  funcoppc3  49129  oppcuprcl2  49184  isinito3  49482