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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  breqtrrd  5138  breqtrid  5147  domunsn  9097  mapdom2  9118  phplem2  9175  mapfien2  9367  wemaplem2  9507  infdifsn  9617  cantnff  9634  ttrclss  9680  rnttrcl  9682  infxpenlem  9973  infmap2  10177  ssfin4  10270  canthp1lem1  10612  nqereq  10895  ltexnq  10935  ltbtwnnq  10938  add20  11697  mullt0  11704  ltm1  12031  recgt0  12035  prodgt0  12036  ltmul1a  12038  mulge0b  12060  recp1lt1  12088  recreclt  12089  ledivp1  12092  ledivp1i  12115  ltdivp1i  12116  eluzmn  12807  ltaddrp2d  13036  mul2lt0bi  13066  prodge0rd  13067  xleadd1a  13220  xov1plusxeqvd  13466  fz01en  13520  fzonmapblen  13676  fladdz  13794  flhalf  13799  fldiv  13829  modsubdir  13912  fzen2  13941  serle  14029  ltexp2a  14138  leexp2a  14144  exple1  14149  expubnd  14150  bernneq  14201  expmulnbnd  14207  discr1  14211  discr  14212  faclbnd6  14271  hashfz  14399  hashfun  14409  seqcoll  14436  sqeqd  15139  01sqrexlem7  15221  sqrtge0  15230  sqrtneglem  15239  abslt  15288  absle  15289  abstri  15304  rlimge0  15554  reccn2  15570  climaddc2  15609  isercolllem1  15638  caucvgrlem  15646  summolem2a  15688  isumge0  15739  fsumle  15772  fsumlt  15773  o1fsum  15786  supcvg  15829  expcnv  15837  geolim  15843  geolim2  15844  georeclim  15845  geo2lim  15848  mertenslem1  15857  mertens  15859  prodmolem2a  15907  efcllem  16050  ef0lem  16051  efgt0  16078  eftlub  16084  eflt  16092  sinbnd  16155  cosbnd  16156  ef01bndlem  16159  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  eirrlem  16179  rpnnen2lem11  16199  rpnnen2lem12  16200  ruclem11  16215  dvdssub2  16278  dvdsadd2b  16283  dvdsexp  16305  3dvds  16308  opoe  16340  bitsfzolem  16411  bitsinv1lem  16418  bezoutlem4  16519  dvdsgcd  16521  dvdsmulgcd  16533  bezoutr1  16546  nn0seqcvgd  16547  rpmulgcd2  16633  qredeq  16634  rpdvds  16637  prmind2  16662  divdenle  16726  hashdvds  16752  phimullem  16756  eulerthlem2  16759  prmdiveq  16763  prmdivdiv  16764  pythagtriplem4  16797  pythagtriplem10  16798  pythagtriplem19  16811  iserodd  16813  pcpre1  16820  pcadd2  16868  qexpz  16879  expnprm  16880  oddprmdvds  16881  pockthlem  16883  prmreclem2  16895  prmreclem3  16896  4sqlem7  16922  4sqlem10  16925  4sqlem11  16933  4sqlem12  16934  4sqlem14  16936  4sqlem15  16937  4sqlem16  16938  0ram  16998  ffthiso  17900  latmlej12  18445  qusgrp  19125  pgpfi1  19532  sylow1lem4  19538  sylow1lem5  19539  odcau  19541  pgpfi  19542  pgpssslw  19551  sylow3lem4  19567  sylow3lem6  19569  efgsfo  19676  frgp0  19697  odadd1  19785  odadd2  19786  odadd  19787  gexexlem  19789  lt6abl  19832  gsumzsubmcl  19855  pwsgsum  19919  dprd2dlem1  19980  dprd2d2  19983  ablfacrplem  20004  ablfacrp  20005  ablfacrp2  20006  ablfac1b  20009  ablfac1eu  20012  pgpfac1lem3a  20015  ablfaclem2  20025  dvdsrid  20283  dvdsrtr  20284  dvdsrneg  20286  unitmulcl  20296  unitgrp  20299  unitnegcl  20313  subrguss  20503  subrgunit  20506  isdrng2  20659  fidomndrnglem  20688  abvsubtri  20743  gzrngunit  21357  prmirredlem  21389  znidomb  21478  frlmgsum  21688  psrbaglesupp  21838  psdmul  22060  psdmvr  22063  invrvald  22570  psmetsym  24205  psmettri  24206  mettri2  24236  xmetsym  24242  xmettri  24246  prdsxmetlem  24263  xblss2ps  24296  xblss2  24297  blhalf  24300  xmsge0  24358  ngptgp  24531  nrginvrcnlem  24586  nmoeq0  24631  cnmet  24666  blcvx  24693  opnreen  24727  metdcnlem  24732  metdstri  24747  metdsle  24748  metnrmlem1  24755  metnrmlem3  24757  lebnumlem1  24867  pi1inv  24959  cphnmf  25102  ipge0  25105  ipcau2  25141  tcphcphlem1  25142  csbren  25306  minveclem2  25333  minveclem3  25336  ovolssnul  25395  ovolctb  25398  ovolunnul  25408  ovoliunlem1  25410  ovoliun2  25414  ovoliunnul  25415  ioombl1lem4  25469  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  volcn  25514  vitalilem2  25517  vitalilem5  25520  itg1lea  25620  mbfi1fseqlem6  25628  mbfi1flimlem  25630  itg2eqa  25653  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2cnlem2  25670  iblabsr  25738  iblmulc2  25739  bddiblnc  25750  dveflem  25890  dvef  25891  dvferm2lem  25897  dvlip  25905  c1liplem1  25908  dveq0  25912  dvlt0  25917  dvivthlem1  25920  lhop1  25926  dvfsumle  25933  dvfsumleOLD  25934  dvfsumlem4  25943  dvfsumrlim3  25947  dvfsum2  25948  ftc1a  25951  ftc1lem4  25953  deg1add  26015  ply1divex  26049  ply1rem  26078  fta1glem2  26081  fta1blem  26083  ig1pdvds  26092  plyeq0lem  26122  dgrcolem2  26187  plydivlem4  26211  plyrem  26220  fta1lem  26222  aalioulem3  26249  aaliou2b  26256  aaliou3lem3  26259  aaliou3lem8  26260  ulmcn  26315  ulmdvlem1  26316  itgulm  26324  pserulm  26338  pserdvlem2  26345  abelthlem2  26349  abelthlem5  26352  abelthlem6  26353  abelthlem7  26355  abelthlem8  26356  abelthlem9  26357  sinq12gt0  26423  sinq34lt0t  26425  cosq14gt0  26426  cosq14ge0  26427  cos02pilt1  26442  efif1olem3  26460  argimgt0  26528  argimlt0  26529  logneg2  26531  logcnlem3  26560  logcnlem4  26561  logtayllem  26575  logtayl2  26578  cxpsqrtlem  26618  cxpsqrt  26619  cxpaddlelem  26668  abscxpbnd  26670  zrtdvds  26676  rtprmirr  26677  loglesqrt  26678  ang180lem2  26727  atanlogaddlem  26830  atanlogsublem  26832  atantan  26840  atans2  26848  atantayl  26854  leibpi  26859  log2tlbnd  26862  birthdaylem2  26869  birthdaylem3  26870  cxp2limlem  26893  jensenlem2  26905  jensen  26906  logdiflbnd  26912  emcllem2  26914  emcllem4  26916  harmonicbnd4  26928  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulm2  26953  lgambdd  26954  lgamucov  26955  lgamcvglem  26957  lgamcvg2  26972  gamcvg  26973  wilthlem3  26987  basellem1  26998  basellem3  27000  basellem4  27001  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chteq0  27127  chtub  27130  chpub  27138  logfacubnd  27139  logfaclbnd  27140  logexprlim  27143  perfectlem2  27148  dchrfi  27173  bclbnd  27198  bposlem1  27202  bposlem3  27204  bposlem4  27205  bposlem6  27207  lgslem1  27215  lgsqrlem2  27265  lgsqrlem4  27267  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem1  27302  2sqlem3  27338  2sqlem4  27339  2sqlem8  27344  2sqlem11  27347  2sqcoprm  27353  2sqmod  27354  chebbnd1lem2  27388  chebbnd1lem3  27389  chtppilimlem1  27391  chpchtlim  27397  vmadivsum  27400  vmadivsumb  27401  rpvmasumlem  27405  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrisum0flblem2  27427  dchrisum0fno1  27429  dchrisum0re  27431  dchrisum0lem1  27434  dchrisum0lem2a  27435  mudivsum  27448  mulogsumlem  27449  mulog2sumlem2  27453  vmalogdivsum2  27456  selberglem2  27464  selbergb  27467  selberg2b  27470  logdivbnd  27474  selberg3lem1  27475  selberg3lem2  27476  selberg4lem1  27478  pntrmax  27482  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6a  27500  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem1  27507  pntibndlem2  27509  pntlemb  27515  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemk  27524  qabvle  27543  padicabvcxp  27550  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth3  27556  addsuniflem  27915  negsid  27954  negsunif  27968  mulsuniflem  28059  sltmul2  28081  precsexlem9  28124  absmuls  28153  zscut  28302  addhalfcut  28341  zs12ge0  28349  legtrid  28525  legov3  28532  krippenlem  28624  mideulem2  28668  midex  28671  opphllem5  28685  opphllem6  28686  opphl  28688  lmieu  28718  lmiisolem  28730  ttgcontlem1  28819  colinearalglem4  28843  axpaschlem  28874  axcontlem7  28904  nbfusgrlevtxm2  29312  clwlksndivn  30022  eucrct2eupth  30181  nvge0  30609  smcnlem  30633  nmoub3i  30709  nmoub2i  30710  nmlno0lem  30729  minvecolem2  30811  htthlem  30853  norm3dif2  31087  bcs2  31118  chscllem2  31574  eigposi  31772  nmopub2tALT  31845  nmfnleub2  31862  nmlnop0iALT  31931  riesz1  32001  cnlnadjlem2  32004  nmopcoadji  32037  leopsq  32065  leopmul  32070  leopnmid  32074  nmopleid  32075  opsqrlem6  32081  0leopj  32122  hstle1  32162  strlem3a  32188  mdslmd4i  32269  cvexchlem  32304  cdj1i  32369  unidifsnel  32471  unidifsnne  32472  le2halvesd  32686  xlt2addrd  32689  fsumub  32760  sgnmulsgp  32775  2exple2exp  32777  oexpled  32779  wrdt2ind  32882  xrge0tsmsd  33009  fzto1st1  33066  cycpmco2lem4  33093  cycpmco2lem6  33095  cyc3conja  33121  archiabllem1a  33152  archiabllem2a  33155  archiabllem2c  33156  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  orng0le1  33297  rprmdvdsprod  33512  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  ply1dg3rt0irred  33558  exsslsb  33599  fedgmullem1  33632  fedgmullem2  33633  fldsdrgfldext2  33665  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  fldext2rspun  33684  algextdeglem8  33721  rtelextdg2lem  33723  constrext2chnlem  33747  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  metideq  33890  metider  33891  sqsscirc1  33905  esummono  34051  esumpad2  34053  esumle  34055  esumlef  34059  esumcst  34060  esumrnmpt2  34065  esum2d  34090  aean  34241  dya2ub  34268  dya2icoseg  34275  omssubadd  34298  inelcarsg  34309  carsgsigalem  34313  carsggect  34316  carsgclctunlem2  34317  eulerpartlemb  34366  fibp1  34399  signsplypnf  34548  signsply0  34549  fdvposlt  34597  fdvposle  34599  reprgt  34619  logdivsqrle  34648  hgt750lemb  34654  hgt750leme  34656  tgoldbachgtde  34658  subfacval3  35183  sconnpht2  35232  sconnpi1  35233  resconn  35240  snmlff  35323  sinccvglem  35666  faclimlem2  35738  btwnouttr2  36017  weiunpo  36460  dnibndlem5  36477  dnibndlem7  36479  dnibndlem8  36480  dnibndlem9  36481  dnibndlem10  36482  dnibnd  36486  knoppcnlem4  36491  knoppcnlem9  36496  unbdqndv2lem1  36504  unbdqndv2lem2  36505  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem21  36527  ltflcei  37609  poimirlem9  37630  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  volsupnfl  37666  itg2addnclem  37672  itg2addnclem3  37674  iblmulc2nc  37686  ftc1cnnclem  37692  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc2nc  37703  dvasin  37705  geomcau  37760  bfplem2  37824  rrncmslem  37833  rrnequiv  37836  lsatcvatlem  39049  islshpcv  39053  atlatmstc  39319  cvlsupr7  39348  cvrval3  39414  cvrval5  39416  cvrexchlem  39420  atcvrj1  39432  cvrat3  39443  cvrat4  39444  atbtwn  39447  1cvratex  39474  hlatexch4  39482  3atlem1  39484  3atlem2  39485  atcvrlln2  39520  atcvrlln  39521  lplnllnneN  39557  llncvrlpln2  39558  4atlem3b  39599  lplncvrlvol2  39616  dalemswapyz  39657  dalemswapyzps  39691  dalem25  39699  dalem39  39712  dalem58  39731  dalem59  39732  lneq2at  39779  lncvrat  39783  dalawlem2  39873  dalawlem3  39874  dalawlem4  39875  dalawlem6  39877  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  lhpocnle  40017  lhpmcvr3  40026  lhpmcvr5N  40028  lhpmcvr6N  40029  4atexlemunv  40067  4atexlemc  40070  4atexlemex2  40072  lautm  40095  cdlemc2  40193  cdleme5  40241  cdleme11j  40268  cdleme16b  40280  cdlemednpq  40300  cdleme19e  40308  cdleme20i  40318  cdleme22a  40341  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme23c  40352  cdleme30a  40379  cdleme35a  40449  cdleme35b  40451  cdleme42h  40483  cdlemeg46rgv  40529  cdlemg8b  40629  cdlemg12e  40648  cdlemg13a  40652  cdlemg17pq  40673  cdlemg18c  40681  cdlemg19  40685  cdlemg21  40687  cdlemg31d  40701  cdlemg33a  40707  tendoid  40774  cdlemk4  40835  cdlemki  40842  cdlemk10  40844  cdlemksv2  40848  cdlemk12  40851  cdlemk14  40855  cdlemk15  40856  cdlemk1u  40860  cdlemk5u  40862  cdlemk12u  40873  cdlemk45  40948  cdlemk48  40951  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  cdlemm10N  41119  cdlemn2  41196  dihjustlem  41217  dihglbcpreN  41301  dihmeetlem3N  41306  nnproddivdvdsd  41995  lcmineqlem17  42040  lcmineqlem18  42041  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p8  42082  posbezout  42095  primrootspoweq0  42101  aks6d1c1  42111  hashscontpow1  42116  aks6d1c4  42119  aks6d1c2  42125  aks6d1c5lem1  42131  aks6d1c5lem3  42132  aks6d1c5lem2  42133  deg1gprod  42135  sticksstones7  42147  sticksstones10  42150  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem1  42165  aks6d1c6lem3  42167  aks6d1c6lem4  42168  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  unitscyglem4  42193  aks5lem7  42195  aks5  42199  explt1d  42318  mulgt0b2d  42473  evlselv  42582  dffltz  42629  fltdvdsabdvdsc  42633  fltaccoprm  42635  fltabcoprm  42637  flt4lem5elem  42646  flt4lem7  42654  fltnlta  42658  irrapxlem1  42817  pell1qrgaplem  42868  pell1qrgap  42869  monotoddzzfi  42938  jm2.24nn  42955  congtr  42961  congmul  42963  congsub  42966  fzmaxdif  42977  acongeq  42979  jm2.20nn  42993  jm2.25  42995  hbtlem4  43122  dgrsub2  43131  mpaaeu  43146  idomsubgmo  43189  iscard4  43529  sqrtcvallem4  43635  leeq2d  44154  int-sqgeq0d  44182  int-ineqmvtd  44187  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  dvconstbi  44330  binomcxplemdvbinom  44349  isosctrlem1ALT  44930  mulltgt0  45023  rnmptbd2lem  45249  oddfl  45283  2timesgt  45293  lt3addmuld  45306  lt4addmuld  45311  supxrgere  45336  supxrgelem  45340  supxrge  45341  xadd0ge2  45344  infrpge  45354  xrlexaddrp  45355  xralrple2  45357  infxr  45370  infleinflem1  45373  infleinflem2  45374  infleinf  45375  xralrple4  45376  xralrple3  45377  recnnltrp  45380  rpgtrecnn  45383  xrralrecnnge  45393  rexabslelem  45421  infrnmptle  45426  supminfxr  45467  xrpnf  45488  iccshift  45523  iooshift  45527  ressiocsup  45559  ressioosup  45560  fsumnncl  45577  fmul01  45585  fmul01lt1lem1  45589  fmul01lt1lem2  45590  mccllem  45602  climrec  45608  climexp  45610  climneg  45615  limcrecl  45634  sumnnodd  45635  lptioo2  45636  lptioo1  45637  ltmod  45643  lptre2pt  45645  0ellimcdiv  45654  limclner  45656  fnlimcnv  45672  climinf2lem  45711  limsupubuzlem  45717  limsup10exlem  45777  limsupgtlem  45782  dfxlim2v  45852  xlimliminflimsup  45867  cncficcgt0  45893  cncfioobdlem  45901  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvdsn1add  45944  dvnxpaek  45947  dvnmul  45948  dvnprodlem1  45951  itgiccshift  45985  itgperiod  45986  sublevolico  45989  ismbl3  45991  ovolsplit  45993  ismbl4  45998  stoweidlem1  46006  stoweidlem11  46016  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  stoweidlem38  46043  stoweidlem42  46047  stoweidlem51  46056  stoweidlem59  46064  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem13  46091  stirlinglem15  46093  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem4  46116  fourierdlem10  46122  fourierdlem11  46123  fourierdlem15  46127  fourierdlem20  46132  fourierdlem25  46137  fourierdlem26  46138  fourierdlem30  46142  fourierdlem37  46149  fourierdlem39  46151  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem44  46156  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem52  46163  fourierdlem54  46165  fourierdlem60  46171  fourierdlem61  46172  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem81  46192  fourierdlem84  46195  fourierdlem87  46198  fourierdlem92  46203  fourierdlem93  46204  fourierdlem101  46212  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  etransclem19  46258  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem27  46266  etransclem32  46271  etransclem35  46274  etransclem48  46287  qndenserrnbllem  46299  ioorrnopnlem  46309  ioorrnopnxrlem  46311  fsumlesge0  46382  sge0cl  46386  sge0supre  46394  sge0less  46397  sge0gerp  46400  sge0ltfirp  46405  sge0le  46412  sge0ltfirpmpt  46413  sge0split  46414  sge0rpcpnf  46426  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xaddlem1  46438  sge0pnffigtmpt  46445  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0seq  46451  nnfoctbdjlem  46460  meassle  46468  meaiuninclem  46485  meaiininclem  46491  omeiunle  46522  omeiunltfirp  46524  carageniuncllem2  46527  carageniuncl  46528  omess0  46539  hoicvr  46553  ovnlerp  46567  ovnsubaddlem1  46575  hsphoidmvle2  46590  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem5  46604  ovnhoilem2  46607  ovnhoi  46608  hoidifhspdmvle  46625  hoiqssbllem2  46628  hspmbllem2  46632  hspmbllem3  46633  hspmbl  46634  vonioolem2  46686  vonicclem2  46689  smfaddlem1  46768  smflimlem2  46777  smflimlem4  46779  smfmullem1  46796  smfinflem  46822  smflimsuplem4  46828  smflimsuplem8  46832  perfectALTVlem2  47727  nnpw2blen  48573  itscnhlinecirc02plem1  48775  funcoppc3  49140  oppcuprcl2  49195  isinito3  49493