Theorem breqtrd 5133

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breqtrrd  5135  breqtrid  5144  domunsn  9091  mapdom2  9112  phplem2  9169  mapfien2  9360  wemaplem2  9500  infdifsn  9610  cantnff  9627  ttrclss  9673  rnttrcl  9675  infxpenlem  9966  infmap2  10170  ssfin4  10263  canthp1lem1  10605  nqereq  10888  ltexnq  10928  ltbtwnnq  10931  add20  11690  mullt0  11697  ltm1  12024  recgt0  12028  prodgt0  12029  ltmul1a  12031  mulge0b  12053  recp1lt1  12081  recreclt  12082  ledivp1  12085  ledivp1i  12108  ltdivp1i  12109  eluzmn  12800  ltaddrp2d  13029  mul2lt0bi  13059  prodge0rd  13060  xleadd1a  13213  xov1plusxeqvd  13459  fz01en  13513  fzonmapblen  13669  fladdz  13787  flhalf  13792  fldiv  13822  modsubdir  13905  fzen2  13934  serle  14022  ltexp2a  14131  leexp2a  14137  exple1  14142  expubnd  14143  bernneq  14194  expmulnbnd  14200  discr1  14204  discr  14205  faclbnd6  14264  hashfz  14392  hashfun  14402  seqcoll  14429  sqeqd  15132  01sqrexlem7  15214  sqrtge0  15223  sqrtneglem  15232  abslt  15281  absle  15282  abstri  15297  rlimge0  15547  reccn2  15563  climaddc2  15602  isercolllem1  15631  caucvgrlem  15639  summolem2a  15681  isumge0  15732  fsumle  15765  fsumlt  15766  o1fsum  15779  supcvg  15822  expcnv  15830  geolim  15836  geolim2  15837  georeclim  15838  geo2lim  15841  mertenslem1  15850  mertens  15852  prodmolem2a  15900  efcllem  16043  ef0lem  16044  efgt0  16071  eftlub  16077  eflt  16085  sinbnd  16148  cosbnd  16149  ef01bndlem  16152  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  eirrlem  16172  rpnnen2lem11  16192  rpnnen2lem12  16193  ruclem11  16208  dvdssub2  16271  dvdsadd2b  16276  dvdsexp  16298  3dvds  16301  opoe  16333  bitsfzolem  16404  bitsinv1lem  16411  bezoutlem4  16512  dvdsgcd  16514  dvdsmulgcd  16526  bezoutr1  16539  nn0seqcvgd  16540  rpmulgcd2  16626  qredeq  16627  rpdvds  16630  prmind2  16655  divdenle  16719  hashdvds  16745  phimullem  16749  eulerthlem2  16752  prmdiveq  16756  prmdivdiv  16757  pythagtriplem4  16790  pythagtriplem10  16791  pythagtriplem19  16804  iserodd  16806  pcpre1  16813  pcadd2  16861  qexpz  16872  expnprm  16873  oddprmdvds  16874  pockthlem  16876  prmreclem2  16888  prmreclem3  16889  4sqlem7  16915  4sqlem10  16918  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  4sqlem15  16930  4sqlem16  16931  0ram  16991  ffthiso  17893  latmlej12  18438  qusgrp  19118  pgpfi1  19525  sylow1lem4  19531  sylow1lem5  19532  odcau  19534  pgpfi  19535  pgpssslw  19544  sylow3lem4  19560  sylow3lem6  19562  efgsfo  19669  frgp0  19690  odadd1  19778  odadd2  19779  odadd  19780  gexexlem  19782  lt6abl  19825  gsumzsubmcl  19848  pwsgsum  19912  dprd2dlem1  19973  dprd2d2  19976  ablfacrplem  19997  ablfacrp  19998  ablfacrp2  19999  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem3a  20008  ablfaclem2  20018  dvdsrid  20276  dvdsrtr  20277  dvdsrneg  20279  unitmulcl  20289  unitgrp  20292  unitnegcl  20306  subrguss  20496  subrgunit  20499  isdrng2  20652  fidomndrnglem  20681  abvsubtri  20736  gzrngunit  21350  prmirredlem  21382  znidomb  21471  frlmgsum  21681  psrbaglesupp  21831  psdmul  22053  psdmvr  22056  invrvald  22563  psmetsym  24198  psmettri  24199  mettri2  24229  xmetsym  24235  xmettri  24239  prdsxmetlem  24256  xblss2ps  24289  xblss2  24290  blhalf  24293  xmsge0  24351  ngptgp  24524  nrginvrcnlem  24579  nmoeq0  24624  cnmet  24659  blcvx  24686  opnreen  24720  metdcnlem  24725  metdstri  24740  metdsle  24741  metnrmlem1  24748  metnrmlem3  24750  lebnumlem1  24860  pi1inv  24952  cphnmf  25095  ipge0  25098  ipcau2  25134  tcphcphlem1  25135  csbren  25299  minveclem2  25326  minveclem3  25329  ovolssnul  25388  ovolctb  25391  ovolunnul  25401  ovoliunlem1  25403  ovoliun2  25407  ovoliunnul  25408  ioombl1lem4  25462  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  volcn  25507  vitalilem2  25510  vitalilem5  25513  itg1lea  25613  mbfi1fseqlem6  25621  mbfi1flimlem  25623  itg2eqa  25646  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2cnlem2  25663  iblabsr  25731  iblmulc2  25732  bddiblnc  25743  dveflem  25883  dvef  25884  dvferm2lem  25890  dvlip  25898  c1liplem1  25901  dveq0  25905  dvlt0  25910  dvivthlem1  25913  lhop1  25919  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem4  25936  dvfsumrlim3  25940  dvfsum2  25941  ftc1a  25944  ftc1lem4  25946  deg1add  26008  ply1divex  26042  ply1rem  26071  fta1glem2  26074  fta1blem  26076  ig1pdvds  26085  plyeq0lem  26115  dgrcolem2  26180  plydivlem4  26204  plyrem  26213  fta1lem  26215  aalioulem3  26242  aaliou2b  26249  aaliou3lem3  26252  aaliou3lem8  26253  ulmcn  26308  ulmdvlem1  26309  itgulm  26317  pserulm  26331  pserdvlem2  26338  abelthlem2  26342  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  abelthlem8  26349  abelthlem9  26350  sinq12gt0  26416  sinq34lt0t  26418  cosq14gt0  26419  cosq14ge0  26420  cos02pilt1  26435  efif1olem3  26453  argimgt0  26521  argimlt0  26522  logneg2  26524  logcnlem3  26553  logcnlem4  26554  logtayllem  26568  logtayl2  26571  cxpsqrtlem  26611  cxpsqrt  26612  cxpaddlelem  26661  abscxpbnd  26663  zrtdvds  26669  rtprmirr  26670  loglesqrt  26671  ang180lem2  26720  atanlogaddlem  26823  atanlogsublem  26825  atantan  26833  atans2  26841  atantayl  26847  leibpi  26852  log2tlbnd  26855  birthdaylem2  26862  birthdaylem3  26863  cxp2limlem  26886  jensenlem2  26898  jensen  26899  logdiflbnd  26905  emcllem2  26907  emcllem4  26909  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulm2  26946  lgambdd  26947  lgamucov  26948  lgamcvglem  26950  lgamcvg2  26965  gamcvg  26966  wilthlem3  26980  basellem1  26991  basellem3  26993  basellem4  26994  fsumdvdsdiaglem  27093  dvdsppwf1o  27096  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chteq0  27120  chtub  27123  chpub  27131  logfacubnd  27132  logfaclbnd  27133  logexprlim  27136  perfectlem2  27141  dchrfi  27166  bclbnd  27191  bposlem1  27195  bposlem3  27197  bposlem4  27198  bposlem6  27200  lgslem1  27208  lgsqrlem2  27258  lgsqrlem4  27260  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem1  27295  2sqlem3  27331  2sqlem4  27332  2sqlem8  27337  2sqlem11  27340  2sqcoprm  27346  2sqmod  27347  chebbnd1lem2  27381  chebbnd1lem3  27382  chtppilimlem1  27384  chpchtlim  27390  vmadivsum  27393  vmadivsumb  27394  rpvmasumlem  27398  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0re  27424  dchrisum0lem1  27427  dchrisum0lem2a  27428  mudivsum  27441  mulogsumlem  27442  mulog2sumlem2  27446  vmalogdivsum2  27449  selberglem2  27457  selbergb  27460  selberg2b  27463  logdivbnd  27467  selberg3lem1  27468  selberg3lem2  27469  selberg4lem1  27471  pntrmax  27475  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6a  27493  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem1  27500  pntibndlem2  27502  pntlemb  27508  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemk  27517  qabvle  27536  padicabvcxp  27543  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth3  27549  addsuniflem  27908  negsid  27947  negsunif  27961  mulsuniflem  28052  sltmul2  28074  precsexlem9  28117  absmuls  28146  zscut  28295  addhalfcut  28334  zs12ge0  28342  legtrid  28518  legov3  28525  krippenlem  28617  mideulem2  28661  midex  28664  opphllem5  28678  opphllem6  28679  opphl  28681  lmieu  28711  lmiisolem  28723  ttgcontlem1  28812  colinearalglem4  28836  axpaschlem  28867  axcontlem7  28897  nbfusgrlevtxm2  29305  clwlksndivn  30015  eucrct2eupth  30174  nvge0  30602  smcnlem  30626  nmoub3i  30702  nmoub2i  30703  nmlno0lem  30722  minvecolem2  30804  htthlem  30846  norm3dif2  31080  bcs2  31111  chscllem2  31567  eigposi  31765  nmopub2tALT  31838  nmfnleub2  31855  nmlnop0iALT  31924  riesz1  31994  cnlnadjlem2  31997  nmopcoadji  32030  leopsq  32058  leopmul  32063  leopnmid  32067  nmopleid  32068  opsqrlem6  32074  0leopj  32115  hstle1  32155  strlem3a  32181  mdslmd4i  32262  cvexchlem  32297  cdj1i  32362  unidifsnel  32464  unidifsnne  32465  le2halvesd  32679  xlt2addrd  32682  fsumub  32753  sgnmulsgp  32768  2exple2exp  32770  oexpled  32772  wrdt2ind  32875  xrge0tsmsd  33002  fzto1st1  33059  cycpmco2lem4  33086  cycpmco2lem6  33088  cyc3conja  33114  archiabllem1a  33145  archiabllem2a  33148  archiabllem2c  33149  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  orng0le1  33290  rprmdvdsprod  33505  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  ply1dg3rt0irred  33551  exsslsb  33592  fedgmullem1  33625  fedgmullem2  33626  fldsdrgfldext2  33658  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  fldext2rspun  33677  algextdeglem8  33714  rtelextdg2lem  33716  constrext2chnlem  33740  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  metideq  33883  metider  33884  sqsscirc1  33898  esummono  34044  esumpad2  34046  esumle  34048  esumlef  34052  esumcst  34053  esumrnmpt2  34058  esum2d  34083  aean  34234  dya2ub  34261  dya2icoseg  34268  omssubadd  34291  inelcarsg  34302  carsgsigalem  34306  carsggect  34309  carsgclctunlem2  34310  eulerpartlemb  34359  fibp1  34392  signsplypnf  34541  signsply0  34542  fdvposlt  34590  fdvposle  34592  reprgt  34612  logdivsqrle  34641  hgt750lemb  34647  hgt750leme  34649  tgoldbachgtde  34651  subfacval3  35176  sconnpht2  35225  sconnpi1  35226  resconn  35233  snmlff  35316  sinccvglem  35659  faclimlem2  35731  btwnouttr2  36010  weiunpo  36453  dnibndlem5  36470  dnibndlem7  36472  dnibndlem8  36473  dnibndlem9  36474  dnibndlem10  36475  dnibnd  36479  knoppcnlem4  36484  knoppcnlem9  36489  unbdqndv2lem1  36497  unbdqndv2lem2  36498  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem21  36520  ltflcei  37602  poimirlem9  37623  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  volsupnfl  37659  itg2addnclem  37665  itg2addnclem3  37667  iblmulc2nc  37679  ftc1cnnclem  37685  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc2nc  37696  dvasin  37698  geomcau  37753  bfplem2  37817  rrncmslem  37826  rrnequiv  37829  lsatcvatlem  39042  islshpcv  39046  atlatmstc  39312  cvlsupr7  39341  cvrval3  39407  cvrval5  39409  cvrexchlem  39413  atcvrj1  39425  cvrat3  39436  cvrat4  39437  atbtwn  39440  1cvratex  39467  hlatexch4  39475  3atlem1  39477  3atlem2  39478  atcvrlln2  39513  atcvrlln  39514  lplnllnneN  39550  llncvrlpln2  39551  4atlem3b  39592  lplncvrlvol2  39609  dalemswapyz  39650  dalemswapyzps  39684  dalem25  39692  dalem39  39705  dalem58  39724  dalem59  39725  lneq2at  39772  lncvrat  39776  dalawlem2  39866  dalawlem3  39867  dalawlem4  39868  dalawlem6  39870  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  lhpocnle  40010  lhpmcvr3  40019  lhpmcvr5N  40021  lhpmcvr6N  40022  4atexlemunv  40060  4atexlemc  40063  4atexlemex2  40065  lautm  40088  cdlemc2  40186  cdleme5  40234  cdleme11j  40261  cdleme16b  40273  cdlemednpq  40293  cdleme19e  40301  cdleme20i  40311  cdleme22a  40334  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme23c  40345  cdleme30a  40372  cdleme35a  40442  cdleme35b  40444  cdleme42h  40476  cdlemeg46rgv  40522  cdlemg8b  40622  cdlemg12e  40641  cdlemg13a  40645  cdlemg17pq  40666  cdlemg18c  40674  cdlemg19  40678  cdlemg21  40680  cdlemg31d  40694  cdlemg33a  40700  tendoid  40767  cdlemk4  40828  cdlemki  40835  cdlemk10  40837  cdlemksv2  40841  cdlemk12  40844  cdlemk14  40848  cdlemk15  40849  cdlemk1u  40853  cdlemk5u  40855  cdlemk12u  40866  cdlemk45  40941  cdlemk48  40944  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  cdlemm10N  41112  cdlemn2  41189  dihjustlem  41210  dihglbcpreN  41294  dihmeetlem3N  41299  nnproddivdvdsd  41988  lcmineqlem17  42033  lcmineqlem18  42034  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p8  42075  posbezout  42088  primrootspoweq0  42094  aks6d1c1  42104  hashscontpow1  42109  aks6d1c4  42112  aks6d1c2  42118  aks6d1c5lem1  42124  aks6d1c5lem3  42125  aks6d1c5lem2  42126  deg1gprod  42128  sticksstones7  42140  sticksstones10  42143  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem1  42158  aks6d1c6lem3  42160  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  unitscyglem4  42186  aks5lem7  42188  aks5  42192  explt1d  42311  mulgt0b2d  42466  evlselv  42575  dffltz  42622  fltdvdsabdvdsc  42626  fltaccoprm  42628  fltabcoprm  42630  flt4lem5elem  42639  flt4lem7  42647  fltnlta  42651  irrapxlem1  42810  pell1qrgaplem  42861  pell1qrgap  42862  monotoddzzfi  42931  jm2.24nn  42948  congtr  42954  congmul  42956  congsub  42959  fzmaxdif  42970  acongeq  42972  jm2.20nn  42986  jm2.25  42988  hbtlem4  43115  dgrsub2  43124  mpaaeu  43139  idomsubgmo  43182  iscard4  43522  sqrtcvallem4  43628  leeq2d  44147  int-sqgeq0d  44175  int-ineqmvtd  44180  cvgdvgrat  44302  radcnvrat  44303  hashnzfzclim  44311  dvconstbi  44323  binomcxplemdvbinom  44342  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  45363  infleinflem1  45366  infleinflem2  45367  infleinf  45368  xralrple4  45369  xralrple3  45370  recnnltrp  45373  rpgtrecnn  45376  xrralrecnnge  45386  rexabslelem  45414  infrnmptle  45419  supminfxr  45460  xrpnf  45481  iccshift  45516  iooshift  45520  ressiocsup  45552  ressioosup  45553  fsumnncl  45570  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  mccllem  45595  climrec  45601  climexp  45603  climneg  45608  limcrecl  45627  sumnnodd  45628  lptioo2  45629  lptioo1  45630  ltmod  45636  lptre2pt  45638  0ellimcdiv  45647  limclner  45649  fnlimcnv  45665  climinf2lem  45704  limsupubuzlem  45710  limsup10exlem  45770  limsupgtlem  45775  dfxlim2v  45845  xlimliminflimsup  45860  cncficcgt0  45886  cncfioobdlem  45894  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvdsn1add  45937  dvnxpaek  45940  dvnmul  45941  dvnprodlem1  45944  itgiccshift  45978  itgperiod  45979  sublevolico  45982  ismbl3  45984  ovolsplit  45986  ismbl4  45991  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweidlem38  46036  stoweidlem42  46040  stoweidlem51  46049  stoweidlem59  46057  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem13  46084  stirlinglem15  46086  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem10  46115  fourierdlem11  46116  fourierdlem15  46120  fourierdlem20  46125  fourierdlem25  46130  fourierdlem26  46131  fourierdlem30  46135  fourierdlem37  46142  fourierdlem39  46144  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem44  46149  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem52  46156  fourierdlem54  46158  fourierdlem60  46164  fourierdlem61  46165  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem81  46185  fourierdlem84  46188  fourierdlem87  46191  fourierdlem92  46196  fourierdlem93  46197  fourierdlem101  46205  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  etransclem19  46251  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem32  46264  etransclem35  46267  etransclem48  46280  qndenserrnbllem  46292  ioorrnopnlem  46302  ioorrnopnxrlem  46304  fsumlesge0  46375  sge0cl  46379  sge0supre  46387  sge0less  46390  sge0gerp  46393  sge0ltfirp  46398  sge0le  46405  sge0ltfirpmpt  46406  sge0split  46407  sge0rpcpnf  46419  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xaddlem1  46431  sge0pnffigtmpt  46438  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0seq  46444  nnfoctbdjlem  46453  meassle  46461  meaiuninclem  46478  meaiininclem  46484  omeiunle  46515  omeiunltfirp  46517  carageniuncllem2  46520  carageniuncl  46521  omess0  46532  hoicvr  46546  ovnlerp  46560  ovnsubaddlem1  46568  hsphoidmvle2  46583  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem5  46597  ovnhoilem2  46600  ovnhoi  46601  hoidifhspdmvle  46618  hoiqssbllem2  46621  hspmbllem2  46625  hspmbllem3  46626  hspmbl  46627  vonioolem2  46679  vonicclem2  46682  smfaddlem1  46761  smflimlem2  46770  smflimlem4  46772  smfmullem1  46789  smfinflem  46815  smflimsuplem4  46821  smflimsuplem8  46825  perfectALTVlem2  47723  nnpw2blen  48569  itscnhlinecirc02plem1  48771  funcoppc3  49136  oppcuprcl2  49191  isinito3  49489