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  9069  mapdom2  9090  phplem2  9147  mapfien2  9337  wemaplem2  9477  infdifsn  9589  cantnff  9606  ttrclss  9652  rnttrcl  9654  infxpenlem  9945  infmap2  10149  ssfin4  10242  canthp1lem1  10584  nqereq  10867  ltexnq  10907  ltbtwnnq  10910  add20  11669  mullt0  11676  ltm1  12003  recgt0  12007  prodgt0  12008  ltmul1a  12010  mulge0b  12032  recp1lt1  12060  recreclt  12061  ledivp1  12064  ledivp1i  12087  ltdivp1i  12088  eluzmn  12779  ltaddrp2d  13008  mul2lt0bi  13038  prodge0rd  13039  xleadd1a  13192  xov1plusxeqvd  13438  fz01en  13492  fzonmapblen  13648  fladdz  13766  flhalf  13771  fldiv  13801  modsubdir  13884  fzen2  13913  serle  14001  ltexp2a  14110  leexp2a  14116  exple1  14121  expubnd  14122  bernneq  14173  expmulnbnd  14179  discr1  14183  discr  14184  faclbnd6  14243  hashfz  14371  hashfun  14381  seqcoll  14408  sqeqd  15110  01sqrexlem7  15192  sqrtge0  15201  sqrtneglem  15210  abslt  15259  absle  15260  abstri  15275  rlimge0  15525  reccn2  15541  climaddc2  15580  isercolllem1  15609  caucvgrlem  15617  summolem2a  15659  isumge0  15710  fsumle  15743  fsumlt  15744  o1fsum  15757  supcvg  15800  expcnv  15808  geolim  15814  geolim2  15815  georeclim  15816  geo2lim  15819  mertenslem1  15828  mertens  15830  prodmolem2a  15878  efcllem  16021  ef0lem  16022  efgt0  16049  eftlub  16055  eflt  16063  sinbnd  16126  cosbnd  16127  ef01bndlem  16130  sin01gt0  16136  cos01gt0  16137  sin02gt0  16138  eirrlem  16150  rpnnen2lem11  16170  rpnnen2lem12  16171  ruclem11  16186  dvdssub2  16249  dvdsadd2b  16254  dvdsexp  16276  3dvds  16279  opoe  16311  bitsfzolem  16382  bitsinv1lem  16389  bezoutlem4  16490  dvdsgcd  16492  dvdsmulgcd  16504  bezoutr1  16517  nn0seqcvgd  16518  rpmulgcd2  16604  qredeq  16605  rpdvds  16608  prmind2  16633  divdenle  16697  hashdvds  16723  phimullem  16727  eulerthlem2  16730  prmdiveq  16734  prmdivdiv  16735  pythagtriplem4  16768  pythagtriplem10  16769  pythagtriplem19  16782  iserodd  16784  pcpre1  16791  pcadd2  16839  qexpz  16850  expnprm  16851  oddprmdvds  16852  pockthlem  16854  prmreclem2  16866  prmreclem3  16867  4sqlem7  16893  4sqlem10  16896  4sqlem11  16904  4sqlem12  16905  4sqlem14  16907  4sqlem15  16908  4sqlem16  16909  0ram  16969  ffthiso  17875  latmlej12  18422  qusgrp  19102  pgpfi1  19511  sylow1lem4  19517  sylow1lem5  19518  odcau  19520  pgpfi  19521  pgpssslw  19530  sylow3lem4  19546  sylow3lem6  19548  efgsfo  19655  frgp0  19676  odadd1  19764  odadd2  19765  odadd  19766  gexexlem  19768  lt6abl  19811  gsumzsubmcl  19834  pwsgsum  19898  dprd2dlem1  19959  dprd2d2  19962  ablfacrplem  19983  ablfacrp  19984  ablfacrp2  19985  ablfac1b  19988  ablfac1eu  19991  pgpfac1lem3a  19994  ablfaclem2  20004  dvdsrid  20289  dvdsrtr  20290  dvdsrneg  20292  unitmulcl  20302  unitgrp  20305  unitnegcl  20319  subrguss  20509  subrgunit  20512  isdrng2  20665  fidomndrnglem  20694  abvsubtri  20749  orngsqr  20788  ornglmulle  20789  orngrmulle  20790  orng0le1  20796  gzrngunit  21377  prmirredlem  21416  znidomb  21505  frlmgsum  21716  psrbaglesupp  21866  psdmul  22088  psdmvr  22091  invrvald  22598  psmetsym  24233  psmettri  24234  mettri2  24264  xmetsym  24270  xmettri  24274  prdsxmetlem  24291  xblss2ps  24324  xblss2  24325  blhalf  24328  xmsge0  24386  ngptgp  24559  nrginvrcnlem  24614  nmoeq0  24659  cnmet  24694  blcvx  24721  opnreen  24755  metdcnlem  24760  metdstri  24775  metdsle  24776  metnrmlem1  24783  metnrmlem3  24785  lebnumlem1  24895  pi1inv  24987  cphnmf  25130  ipge0  25133  ipcau2  25169  tcphcphlem1  25170  csbren  25334  minveclem2  25361  minveclem3  25364  ovolssnul  25423  ovolctb  25426  ovolunnul  25436  ovoliunlem1  25438  ovoliun2  25442  ovoliunnul  25443  ioombl1lem4  25497  uniioombllem3  25521  uniioombllem4  25522  uniioombllem5  25523  uniioombl  25525  volcn  25542  vitalilem2  25545  vitalilem5  25548  itg1lea  25648  mbfi1fseqlem6  25656  mbfi1flimlem  25658  itg2eqa  25681  itg2splitlem  25684  itg2split  25685  itg2monolem1  25686  itg2cnlem2  25698  iblabsr  25766  iblmulc2  25767  bddiblnc  25778  dveflem  25918  dvef  25919  dvferm2lem  25925  dvlip  25933  c1liplem1  25936  dveq0  25940  dvlt0  25945  dvivthlem1  25948  lhop1  25954  dvfsumle  25961  dvfsumleOLD  25962  dvfsumlem4  25971  dvfsumrlim3  25975  dvfsum2  25976  ftc1a  25979  ftc1lem4  25981  deg1add  26043  ply1divex  26077  ply1rem  26106  fta1glem2  26109  fta1blem  26111  ig1pdvds  26120  plyeq0lem  26150  dgrcolem2  26215  plydivlem4  26239  plyrem  26248  fta1lem  26250  aalioulem3  26277  aaliou2b  26284  aaliou3lem3  26287  aaliou3lem8  26288  ulmcn  26343  ulmdvlem1  26344  itgulm  26352  pserulm  26366  pserdvlem2  26373  abelthlem2  26377  abelthlem5  26380  abelthlem6  26381  abelthlem7  26383  abelthlem8  26384  abelthlem9  26385  sinq12gt0  26451  sinq34lt0t  26453  cosq14gt0  26454  cosq14ge0  26455  cos02pilt1  26470  efif1olem3  26488  argimgt0  26556  argimlt0  26557  logneg2  26559  logcnlem3  26588  logcnlem4  26589  logtayllem  26603  logtayl2  26606  cxpsqrtlem  26646  cxpsqrt  26647  cxpaddlelem  26696  abscxpbnd  26698  zrtdvds  26704  rtprmirr  26705  loglesqrt  26706  ang180lem2  26755  atanlogaddlem  26858  atanlogsublem  26860  atantan  26868  atans2  26876  atantayl  26882  leibpi  26887  log2tlbnd  26890  birthdaylem2  26897  birthdaylem3  26898  cxp2limlem  26921  jensenlem2  26933  jensen  26934  logdiflbnd  26940  emcllem2  26942  emcllem4  26944  harmonicbnd4  26956  fsumharmonic  26957  lgamgulmlem2  26975  lgamgulm2  26981  lgambdd  26982  lgamucov  26983  lgamcvglem  26985  lgamcvg2  27000  gamcvg  27001  wilthlem3  27015  basellem1  27026  basellem3  27028  basellem4  27029  fsumdvdsdiaglem  27128  dvdsppwf1o  27131  mpodvdsmulf1o  27139  dvdsmulf1o  27141  chteq0  27155  chtub  27158  chpub  27166  logfacubnd  27167  logfaclbnd  27168  logexprlim  27171  perfectlem2  27176  dchrfi  27201  bclbnd  27226  bposlem1  27230  bposlem3  27232  bposlem4  27233  bposlem6  27235  lgslem1  27243  lgsqrlem2  27293  lgsqrlem4  27295  lgseisenlem2  27322  lgsquadlem1  27326  lgsquadlem2  27327  lgsquad2lem1  27330  2sqlem3  27366  2sqlem4  27367  2sqlem8  27372  2sqlem11  27375  2sqcoprm  27381  2sqmod  27382  chebbnd1lem2  27416  chebbnd1lem3  27417  chtppilimlem1  27419  chpchtlim  27425  vmadivsum  27428  vmadivsumb  27429  rpvmasumlem  27433  dchrisumlem2  27436  dchrmusum2  27440  dchrvmasumlem2  27444  dchrvmasumlem3  27445  dchrisum0flblem2  27455  dchrisum0fno1  27457  dchrisum0re  27459  dchrisum0lem1  27462  dchrisum0lem2a  27463  mudivsum  27476  mulogsumlem  27477  mulog2sumlem2  27481  vmalogdivsum2  27484  selberglem2  27492  selbergb  27495  selberg2b  27498  logdivbnd  27502  selberg3lem1  27503  selberg3lem2  27504  selberg4lem1  27506  pntrmax  27510  pntrlog2bndlem2  27524  pntrlog2bndlem3  27525  pntrlog2bndlem5  27527  pntrlog2bndlem6a  27528  pntrlog2bndlem6  27529  pntrlog2bnd  27530  pntpbnd1a  27531  pntpbnd1  27532  pntpbnd2  27533  pntibndlem1  27535  pntibndlem2  27537  pntlemb  27543  pntlemq  27547  pntlemr  27548  pntlemj  27549  pntlemk  27552  qabvle  27571  padicabvcxp  27578  ostth2lem2  27580  ostth2lem3  27581  ostth2lem4  27582  ostth3  27584  addsuniflem  27950  negsid  27989  negsunif  28003  mulsuniflem  28094  sltmul2  28116  precsexlem9  28159  absmuls  28188  zscut  28337  addhalfcut  28384  zs12ge0  28397  legtrid  28573  legov3  28580  krippenlem  28672  mideulem2  28716  midex  28719  opphllem5  28733  opphllem6  28734  opphl  28736  lmieu  28766  lmiisolem  28778  ttgcontlem1  28867  colinearalglem4  28891  axpaschlem  28922  axcontlem7  28952  nbfusgrlevtxm2  29360  clwlksndivn  30067  eucrct2eupth  30226  nvge0  30654  smcnlem  30678  nmoub3i  30754  nmoub2i  30755  nmlno0lem  30774  minvecolem2  30856  htthlem  30898  norm3dif2  31132  bcs2  31163  chscllem2  31619  eigposi  31817  nmopub2tALT  31890  nmfnleub2  31907  nmlnop0iALT  31976  riesz1  32046  cnlnadjlem2  32049  nmopcoadji  32082  leopsq  32110  leopmul  32115  leopnmid  32119  nmopleid  32120  opsqrlem6  32126  0leopj  32167  hstle1  32207  strlem3a  32233  mdslmd4i  32314  cvexchlem  32349  cdj1i  32414  unidifsnel  32516  unidifsnne  32517  le2halvesd  32731  xlt2addrd  32734  fsumub  32805  sgnmulsgp  32820  2exple2exp  32822  oexpled  32824  wrdt2ind  32927  xrge0tsmsd  33047  fzto1st1  33076  cycpmco2lem4  33103  cycpmco2lem6  33105  cyc3conja  33131  archiabllem1a  33162  archiabllem2a  33165  archiabllem2c  33166  rprmdvdsprod  33500  1arithidomlem1  33501  1arithidomlem2  33502  1arithidom  33503  ply1dg3rt0irred  33546  exsslsb  33587  fedgmullem1  33620  fedgmullem2  33621  fldsdrgfldext2  33653  fldextrspundgdvdslem  33670  fldextrspundgdvds  33671  fldext2rspun  33672  algextdeglem8  33709  rtelextdg2lem  33711  constrext2chnlem  33735  cos9thpiminplylem1  33767  cos9thpiminplylem2  33768  metideq  33878  metider  33879  sqsscirc1  33893  esummono  34039  esumpad2  34041  esumle  34043  esumlef  34047  esumcst  34048  esumrnmpt2  34053  esum2d  34078  aean  34229  dya2ub  34256  dya2icoseg  34263  omssubadd  34286  inelcarsg  34297  carsgsigalem  34301  carsggect  34304  carsgclctunlem2  34305  eulerpartlemb  34354  fibp1  34387  signsplypnf  34536  signsply0  34537  fdvposlt  34585  fdvposle  34587  reprgt  34607  logdivsqrle  34636  hgt750lemb  34642  hgt750leme  34644  tgoldbachgtde  34646  subfacval3  35171  sconnpht2  35220  sconnpi1  35221  resconn  35228  snmlff  35311  sinccvglem  35654  faclimlem2  35726  btwnouttr2  36005  weiunpo  36448  dnibndlem5  36465  dnibndlem7  36467  dnibndlem8  36468  dnibndlem9  36469  dnibndlem10  36470  dnibnd  36474  knoppcnlem4  36479  knoppcnlem9  36484  unbdqndv2lem1  36492  unbdqndv2lem2  36493  knoppndvlem11  36505  knoppndvlem12  36506  knoppndvlem14  36508  knoppndvlem15  36509  knoppndvlem17  36511  knoppndvlem18  36512  knoppndvlem19  36513  knoppndvlem21  36515  ltflcei  37597  poimirlem9  37618  poimirlem26  37635  poimirlem27  37636  poimirlem29  37638  heicant  37644  mblfinlem2  37647  mblfinlem3  37648  mblfinlem4  37649  volsupnfl  37654  itg2addnclem  37660  itg2addnclem3  37662  iblmulc2nc  37674  ftc1cnnclem  37680  ftc1anclem6  37687  ftc1anclem7  37688  ftc1anclem8  37689  ftc2nc  37691  dvasin  37693  geomcau  37748  bfplem2  37812  rrncmslem  37821  rrnequiv  37824  lsatcvatlem  39037  islshpcv  39041  atlatmstc  39307  cvlsupr7  39336  cvrval3  39402  cvrval5  39404  cvrexchlem  39408  atcvrj1  39420  cvrat3  39431  cvrat4  39432  atbtwn  39435  1cvratex  39462  hlatexch4  39470  3atlem1  39472  3atlem2  39473  atcvrlln2  39508  atcvrlln  39509  lplnllnneN  39545  llncvrlpln2  39546  4atlem3b  39587  lplncvrlvol2  39604  dalemswapyz  39645  dalemswapyzps  39679  dalem25  39687  dalem39  39700  dalem58  39719  dalem59  39720  lneq2at  39767  lncvrat  39771  dalawlem2  39861  dalawlem3  39862  dalawlem4  39863  dalawlem6  39865  dalawlem9  39868  dalawlem11  39870  dalawlem12  39871  lhpocnle  40005  lhpmcvr3  40014  lhpmcvr5N  40016  lhpmcvr6N  40017  4atexlemunv  40055  4atexlemc  40058  4atexlemex2  40060  lautm  40083  cdlemc2  40181  cdleme5  40229  cdleme11j  40256  cdleme16b  40268  cdlemednpq  40288  cdleme19e  40296  cdleme20i  40306  cdleme22a  40329  cdleme22cN  40331  cdleme22d  40332  cdleme22e  40333  cdleme22eALTN  40334  cdleme22f  40335  cdleme23c  40340  cdleme30a  40367  cdleme35a  40437  cdleme35b  40439  cdleme42h  40471  cdlemeg46rgv  40517  cdlemg8b  40617  cdlemg12e  40636  cdlemg13a  40640  cdlemg17pq  40661  cdlemg18c  40669  cdlemg19  40673  cdlemg21  40675  cdlemg31d  40689  cdlemg33a  40695  tendoid  40762  cdlemk4  40823  cdlemki  40830  cdlemk10  40832  cdlemksv2  40836  cdlemk12  40839  cdlemk14  40843  cdlemk15  40844  cdlemk1u  40848  cdlemk5u  40850  cdlemk12u  40861  cdlemk45  40936  cdlemk48  40939  dia2dimlem1  41053  dia2dimlem2  41054  dia2dimlem3  41055  cdlemm10N  41107  cdlemn2  41184  dihjustlem  41205  dihglbcpreN  41289  dihmeetlem3N  41294  nnproddivdvdsd  41983  lcmineqlem17  42028  lcmineqlem18  42029  3lexlogpow2ineq1  42041  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p5  42058  aks4d1p1  42059  aks4d1p3  42061  aks4d1p8  42070  posbezout  42083  primrootspoweq0  42089  aks6d1c1  42099  hashscontpow1  42104  aks6d1c4  42107  aks6d1c2  42113  aks6d1c5lem1  42119  aks6d1c5lem3  42120  aks6d1c5lem2  42121  deg1gprod  42123  sticksstones7  42135  sticksstones10  42138  sticksstones12  42141  sticksstones22  42151  aks6d1c6lem1  42153  aks6d1c6lem3  42155  aks6d1c6lem4  42156  bcled  42161  bcle2d  42162  aks6d1c7lem1  42163  unitscyglem4  42181  aks5lem7  42183  aks5  42187  explt1d  42306  mulgt0b2d  42461  evlselv  42570  dffltz  42617  fltdvdsabdvdsc  42621  fltaccoprm  42623  fltabcoprm  42625  flt4lem5elem  42634  flt4lem7  42642  fltnlta  42646  irrapxlem1  42805  pell1qrgaplem  42856  pell1qrgap  42857  monotoddzzfi  42926  jm2.24nn  42943  congtr  42949  congmul  42951  congsub  42954  fzmaxdif  42965  acongeq  42967  jm2.20nn  42981  jm2.25  42983  hbtlem4  43110  dgrsub2  43119  mpaaeu  43134  idomsubgmo  43177  iscard4  43517  sqrtcvallem4  43623  leeq2d  44142  int-sqgeq0d  44170  int-ineqmvtd  44175  cvgdvgrat  44297  radcnvrat  44298  hashnzfzclim  44306  dvconstbi  44318  binomcxplemdvbinom  44337  isosctrlem1ALT  44918  mulltgt0  45011  rnmptbd2lem  45237  oddfl  45271  2timesgt  45281  lt3addmuld  45294  lt4addmuld  45299  supxrgere  45324  supxrgelem  45328  supxrge  45329  xadd0ge2  45332  infrpge  45342  xrlexaddrp  45343  xralrple2  45345  infxr  45358  infleinflem1  45361  infleinflem2  45362  infleinf  45363  xralrple4  45364  xralrple3  45365  recnnltrp  45368  rpgtrecnn  45371  xrralrecnnge  45381  rexabslelem  45409  infrnmptle  45414  supminfxr  45455  xrpnf  45476  iccshift  45511  iooshift  45515  ressiocsup  45547  ressioosup  45548  fsumnncl  45565  fmul01  45573  fmul01lt1lem1  45577  fmul01lt1lem2  45578  mccllem  45590  climrec  45596  climexp  45598  climneg  45603  limcrecl  45622  sumnnodd  45623  lptioo2  45624  lptioo1  45625  ltmod  45631  lptre2pt  45633  0ellimcdiv  45642  limclner  45644  fnlimcnv  45660  climinf2lem  45699  limsupubuzlem  45705  limsup10exlem  45765  limsupgtlem  45770  dfxlim2v  45840  xlimliminflimsup  45855  cncficcgt0  45881  cncfioobdlem  45889  ioodvbdlimc1lem1  45924  ioodvbdlimc1lem2  45925  ioodvbdlimc2lem  45927  dvdsn1add  45932  dvnxpaek  45935  dvnmul  45936  dvnprodlem1  45939  itgiccshift  45973  itgperiod  45974  sublevolico  45977  ismbl3  45979  ovolsplit  45981  ismbl4  45986  stoweidlem1  45994  stoweidlem11  46004  stoweidlem13  46006  stoweidlem26  46019  stoweidlem34  46027  stoweidlem38  46031  stoweidlem42  46035  stoweidlem51  46044  stoweidlem59  46052  stirlinglem5  46071  stirlinglem6  46072  stirlinglem7  46073  stirlinglem10  46076  stirlinglem11  46077  stirlinglem13  46079  stirlinglem15  46081  dirkercncflem1  46096  dirkercncflem4  46099  fourierdlem4  46104  fourierdlem10  46110  fourierdlem11  46111  fourierdlem15  46115  fourierdlem20  46120  fourierdlem25  46125  fourierdlem26  46126  fourierdlem30  46130  fourierdlem37  46137  fourierdlem39  46139  fourierdlem40  46140  fourierdlem41  46141  fourierdlem42  46142  fourierdlem44  46144  fourierdlem47  46146  fourierdlem48  46147  fourierdlem49  46148  fourierdlem50  46149  fourierdlem51  46150  fourierdlem52  46151  fourierdlem54  46153  fourierdlem60  46159  fourierdlem61  46160  fourierdlem63  46162  fourierdlem64  46163  fourierdlem65  46164  fourierdlem73  46172  fourierdlem74  46173  fourierdlem75  46174  fourierdlem76  46175  fourierdlem78  46177  fourierdlem79  46178  fourierdlem81  46180  fourierdlem84  46183  fourierdlem87  46186  fourierdlem92  46191  fourierdlem93  46192  fourierdlem101  46200  fourierdlem102  46201  fourierdlem103  46202  fourierdlem104  46203  fourierdlem111  46210  fourierdlem114  46213  sqwvfoura  46221  sqwvfourb  46222  fouriersw  46224  etransclem19  46246  etransclem23  46250  etransclem24  46251  etransclem25  46252  etransclem27  46254  etransclem32  46259  etransclem35  46262  etransclem48  46275  qndenserrnbllem  46287  ioorrnopnlem  46297  ioorrnopnxrlem  46299  fsumlesge0  46370  sge0cl  46374  sge0supre  46382  sge0less  46385  sge0gerp  46388  sge0ltfirp  46393  sge0le  46400  sge0ltfirpmpt  46401  sge0split  46402  sge0rpcpnf  46414  sge0ltfirpmpt2  46419  sge0isum  46420  sge0xaddlem1  46426  sge0pnffigtmpt  46433  sge0pnffsumgt  46435  sge0gtfsumgt  46436  sge0seq  46439  nnfoctbdjlem  46448  meassle  46456  meaiuninclem  46473  meaiininclem  46479  omeiunle  46510  omeiunltfirp  46512  carageniuncllem2  46515  carageniuncl  46516  omess0  46527  hoicvr  46541  ovnlerp  46555  ovnsubaddlem1  46563  hsphoidmvle2  46578  hoidmv1lelem2  46585  hoidmv1le  46587  hoidmvlelem1  46588  hoidmvlelem2  46589  hoidmvlelem3  46590  hoidmvlelem5  46592  ovnhoilem2  46595  ovnhoi  46596  hoidifhspdmvle  46613  hoiqssbllem2  46616  hspmbllem2  46620  hspmbllem3  46621  hspmbl  46622  vonioolem2  46674  vonicclem2  46677  smfaddlem1  46756  smflimlem2  46765  smflimlem4  46767  smfmullem1  46784  smfinflem  46810  smflimsuplem4  46816  smflimsuplem8  46820  perfectALTVlem2  47718  nnpw2blen  48564  itscnhlinecirc02plem1  48766  funcoppc3  49131  oppcuprcl2  49186  isinito3  49484