Theorem breqtrd 5099

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-br 5074

This theorem is referenced by:  breqtrrd  5101  breqtrid  5110  domunsn  9056  mapdom2  9077  phplem2  9130  mapfien2  9313  wemaplem2  9453  infdifsn  9570  cantnff  9587  ttrclss  9633  rnttrcl  9635  infxpenlem  9927  infmap2  10131  ssfin4  10224  canthp1lem1  10567  nqereq  10850  ltexnq  10890  ltbtwnnq  10893  add20  11654  mullt0  11661  ltm1  11989  recgt0  11993  prodgt0  11994  ltmul1a  11996  mulge0b  12018  recp1lt1  12046  recreclt  12047  ledivp1  12050  ledivp1i  12073  ltdivp1i  12074  eluzmn  12787  ltaddrp2d  13012  mul2lt0bi  13042  prodge0rd  13043  xleadd1a  13197  xov1plusxeqvd  13443  fz01en  13498  fzonmapblen  13655  fladdz  13776  flhalf  13781  fldiv  13811  modsubdir  13894  fzen2  13923  serle  14011  ltexp2a  14120  leexp2a  14126  exple1  14131  expubnd  14132  bernneq  14183  expmulnbnd  14189  discr1  14193  discr  14194  faclbnd6  14253  hashfz  14381  hashfun  14391  seqcoll  14418  sqeqd  15120  01sqrexlem7  15202  sqrtge0  15211  sqrtneglem  15220  abslt  15269  absle  15270  abstri  15285  rlimge0  15535  reccn2  15551  climaddc2  15590  isercolllem1  15619  caucvgrlem  15627  summolem2a  15669  isumge0  15720  fsumle  15754  fsumlt  15755  o1fsum  15768  supcvg  15813  expcnv  15821  geolim  15827  geolim2  15828  georeclim  15829  geo2lim  15832  mertenslem1  15841  mertens  15843  prodmolem2a  15891  efcllem  16034  ef0lem  16035  efgt0  16062  eftlub  16068  eflt  16076  sinbnd  16139  cosbnd  16140  ef01bndlem  16143  sin01gt0  16149  cos01gt0  16150  sin02gt0  16151  eirrlem  16163  rpnnen2lem11  16183  rpnnen2lem12  16184  ruclem11  16199  dvdssub2  16262  dvdsadd2b  16267  dvdsexp  16289  3dvds  16292  opoe  16324  bitsfzolem  16395  bitsinv1lem  16402  bezoutlem4  16503  dvdsgcd  16505  dvdsmulgcd  16517  bezoutr1  16530  nn0seqcvgd  16531  rpmulgcd2  16617  qredeq  16618  rpdvds  16621  prmind2  16646  divdenle  16711  hashdvds  16737  phimullem  16741  eulerthlem2  16744  prmdiveq  16748  prmdivdiv  16749  pythagtriplem4  16782  pythagtriplem10  16783  pythagtriplem19  16796  iserodd  16798  pcpre1  16805  pcadd2  16853  qexpz  16864  expnprm  16865  oddprmdvds  16866  pockthlem  16868  prmreclem2  16880  prmreclem3  16881  4sqlem7  16907  4sqlem10  16910  4sqlem11  16918  4sqlem12  16919  4sqlem14  16921  4sqlem15  16922  4sqlem16  16923  0ram  16983  ffthiso  17890  latmlej12  18437  qusgrp  19153  pgpfi1  19562  sylow1lem4  19568  sylow1lem5  19569  odcau  19571  pgpfi  19572  pgpssslw  19581  sylow3lem4  19597  sylow3lem6  19599  efgsfo  19706  frgp0  19727  odadd1  19815  odadd2  19816  odadd  19817  gexexlem  19819  lt6abl  19862  gsumzsubmcl  19885  pwsgsum  19949  dprd2dlem1  20010  dprd2d2  20013  ablfacrplem  20034  ablfacrp  20035  ablfacrp2  20036  ablfac1b  20039  ablfac1eu  20042  pgpfac1lem3a  20045  ablfaclem2  20055  dvdsrid  20339  dvdsrtr  20340  dvdsrneg  20342  unitmulcl  20352  unitgrp  20355  unitnegcl  20369  subrguss  20560  subrgunit  20563  isdrng2  20716  fidomndrnglem  20745  abvsubtri  20800  orngsqr  20839  ornglmulle  20840  orngrmulle  20841  orng0le1  20847  gzrngunit  21409  prmirredlem  21448  znidomb  21537  frlmgsum  21748  psrbaglesupp  21898  psdmul  22155  psdmvr  22158  invrvald  22660  psmetsym  24294  psmettri  24295  mettri2  24325  xmetsym  24331  xmettri  24335  prdsxmetlem  24352  xblss2ps  24385  xblss2  24386  blhalf  24389  xmsge0  24447  ngptgp  24620  nrginvrcnlem  24675  nmoeq0  24720  cnmet  24755  blcvx  24782  opnreen  24816  metdcnlem  24821  metdstri  24836  metdsle  24837  metnrmlem1  24844  metnrmlem3  24846  lebnumlem1  24947  pi1inv  25038  cphnmf  25181  ipge0  25184  ipcau2  25220  tcphcphlem1  25221  csbren  25385  minveclem2  25412  minveclem3  25415  ovolssnul  25473  ovolctb  25476  ovolunnul  25486  ovoliunlem1  25488  ovoliun2  25492  ovoliunnul  25493  ioombl1lem4  25547  uniioombllem3  25571  uniioombllem4  25572  uniioombllem5  25573  uniioombl  25575  volcn  25592  vitalilem2  25595  vitalilem5  25598  itg1lea  25698  mbfi1fseqlem6  25706  mbfi1flimlem  25708  itg2eqa  25731  itg2splitlem  25734  itg2split  25735  itg2monolem1  25736  itg2cnlem2  25748  iblabsr  25816  iblmulc2  25817  bddiblnc  25828  dveflem  25965  dvef  25966  dvferm2lem  25972  dvlip  25979  c1liplem1  25982  dveq0  25986  dvlt0  25991  dvivthlem1  25994  lhop1  26000  dvfsumle  26007  dvfsumlem4  26015  dvfsumrlim3  26019  dvfsum2  26020  ftc1a  26023  ftc1lem4  26025  deg1add  26087  ply1divex  26121  ply1rem  26150  fta1glem2  26153  fta1blem  26155  ig1pdvds  26164  plyeq0lem  26194  dgrcolem2  26258  plydivlem4  26281  plyrem  26290  fta1lem  26292  aalioulem3  26319  aaliou2b  26326  aaliou3lem3  26329  aaliou3lem8  26330  ulmcn  26383  ulmdvlem1  26384  itgulm  26392  pserulm  26406  pserdvlem2  26412  abelthlem2  26416  abelthlem5  26419  abelthlem6  26420  abelthlem7  26422  abelthlem8  26423  abelthlem9  26424  sinq12gt0  26490  sinq34lt0t  26492  cosq14gt0  26493  cosq14ge0  26494  cos02pilt1  26509  efif1olem3  26527  argimgt0  26595  argimlt0  26596  logneg2  26598  logcnlem3  26627  logcnlem4  26628  logtayllem  26642  logtayl2  26645  cxpsqrtlem  26685  cxpsqrt  26686  cxpaddlelem  26734  abscxpbnd  26736  zrtdvds  26742  rtprmirr  26743  loglesqrt  26744  ang180lem2  26793  atanlogaddlem  26896  atanlogsublem  26898  atantan  26906  atans2  26914  atantayl  26920  leibpi  26925  log2tlbnd  26928  birthdaylem2  26935  birthdaylem3  26936  cxp2limlem  26958  jensenlem2  26970  jensen  26971  logdiflbnd  26977  emcllem2  26979  emcllem4  26981  harmonicbnd4  26993  fsumharmonic  26994  lgamgulmlem2  27012  lgamgulm2  27018  lgambdd  27019  lgamucov  27020  lgamcvglem  27022  lgamcvg2  27037  gamcvg  27038  wilthlem3  27052  basellem1  27063  basellem3  27065  basellem4  27066  fsumdvdsdiaglem  27165  dvdsppwf1o  27168  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chteq0  27191  chtub  27194  chpub  27202  logfacubnd  27203  logfaclbnd  27204  logexprlim  27207  perfectlem2  27212  dchrfi  27237  bclbnd  27262  bposlem1  27266  bposlem3  27268  bposlem4  27269  bposlem6  27271  lgslem1  27279  lgsqrlem2  27329  lgsqrlem4  27331  lgseisenlem2  27358  lgsquadlem1  27362  lgsquadlem2  27363  lgsquad2lem1  27366  2sqlem3  27402  2sqlem4  27403  2sqlem8  27408  2sqlem11  27411  2sqcoprm  27417  2sqmod  27418  chebbnd1lem2  27452  chebbnd1lem3  27453  chtppilimlem1  27455  chpchtlim  27461  vmadivsum  27464  vmadivsumb  27465  rpvmasumlem  27469  dchrisumlem2  27472  dchrmusum2  27476  dchrvmasumlem2  27480  dchrvmasumlem3  27481  dchrisum0flblem2  27491  dchrisum0fno1  27493  dchrisum0re  27495  dchrisum0lem1  27498  dchrisum0lem2a  27499  mudivsum  27512  mulogsumlem  27513  mulog2sumlem2  27517  vmalogdivsum2  27520  selberglem2  27528  selbergb  27531  selberg2b  27534  logdivbnd  27538  selberg3lem1  27539  selberg3lem2  27540  selberg4lem1  27542  pntrmax  27546  pntrlog2bndlem2  27560  pntrlog2bndlem3  27561  pntrlog2bndlem5  27563  pntrlog2bndlem6a  27564  pntrlog2bndlem6  27565  pntrlog2bnd  27566  pntpbnd1a  27567  pntpbnd1  27568  pntpbnd2  27569  pntibndlem1  27571  pntibndlem2  27573  pntlemb  27579  pntlemq  27583  pntlemr  27584  pntlemj  27585  pntlemk  27588  qabvle  27607  padicabvcxp  27614  ostth2lem2  27616  ostth2lem3  27617  ostth2lem4  27618  ostth3  27620  addsuniflem  28012  negsid  28052  negsunif  28066  negright  28070  mulsuniflem  28160  ltmuls2  28182  precsexlem9  28226  absmuls  28255  zcuts  28418  addhalfcut  28470  pw2cut2  28473  bdayfinbndlem1  28478  z12sge0  28494  legtrid  28678  legov3  28685  krippenlem  28777  mideulem2  28821  midex  28824  opphllem5  28838  opphllem6  28839  opphl  28841  lmieu  28871  lmiisolem  28883  ttgcontlem1  28972  colinearalglem4  28997  axpaschlem  29028  axcontlem7  29058  nbfusgrlevtxm2  29466  clwlksndivn  30175  eucrct2eupth  30334  nvge0  30763  smcnlem  30787  nmoub3i  30863  nmoub2i  30864  nmlno0lem  30883  minvecolem2  30965  htthlem  31007  norm3dif2  31241  bcs2  31272  chscllem2  31728  eigposi  31926  nmopub2tALT  31999  nmfnleub2  32016  nmlnop0iALT  32085  riesz1  32155  cnlnadjlem2  32158  nmopcoadji  32191  leopsq  32219  leopmul  32224  leopnmid  32228  nmopleid  32229  opsqrlem6  32235  0leopj  32276  hstle1  32316  strlem3a  32342  mdslmd4i  32423  cvexchlem  32458  cdj1i  32523  unidifsnel  32624  unidifsnne  32625  le2halvesd  32849  xlt2addrd  32852  fsumub  32921  sgnmulsgp  32936  2exple2exp  32938  oexpled  32940  wrdt2ind  33033  xrge0tsmsd  33155  fzto1st1  33184  cycpmco2lem4  33211  cycpmco2lem6  33213  cyc3conja  33239  archiabllem1a  33273  archiabllem2a  33276  archiabllem2c  33277  rprmdvdsprod  33626  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  ply1dg3rt0irred  33676  mplmulmvr  33732  mplvrpmrhm  33740  exsslsb  33790  fedgmullem1  33822  fedgmullem2  33823  fldsdrgfldext2  33855  fldextrspundgdvdslem  33873  fldextrspundgdvds  33874  fldext2rspun  33875  extdgfialglem2  33886  algextdeglem8  33917  rtelextdg2lem  33919  constrext2chnlem  33943  cos9thpiminplylem1  33975  cos9thpiminplylem2  33976  metideq  34086  metider  34087  sqsscirc1  34101  esummono  34247  esumpad2  34249  esumle  34251  esumlef  34255  esumcst  34256  esumrnmpt2  34261  esum2d  34286  aean  34437  dya2ub  34463  dya2icoseg  34470  omssubadd  34493  inelcarsg  34504  carsgsigalem  34508  carsggect  34511  carsgclctunlem2  34512  eulerpartlemb  34561  fibp1  34594  signsplypnf  34743  signsply0  34744  fdvposlt  34792  fdvposle  34794  reprgt  34814  logdivsqrle  34843  hgt750lemb  34849  hgt750leme  34851  tgoldbachgtde  34853  subfacval3  35426  sconnpht2  35475  sconnpi1  35476  resconn  35483  snmlff  35566  sinccvglem  35909  faclimlem2  35981  btwnouttr2  36259  weiunpo  36702  dnibndlem5  36797  dnibndlem7  36799  dnibndlem8  36800  dnibndlem9  36801  dnibndlem10  36802  dnibnd  36806  knoppcnlem4  36811  knoppcnlem9  36816  unbdqndv2lem1  36824  unbdqndv2lem2  36825  knoppndvlem11  36837  knoppndvlem12  36838  knoppndvlem14  36840  knoppndvlem15  36841  knoppndvlem17  36843  knoppndvlem18  36844  knoppndvlem19  36845  knoppndvlem21  36847  ltflcei  37984  poimirlem9  38005  poimirlem26  38022  poimirlem27  38023  poimirlem29  38025  heicant  38031  mblfinlem2  38034  mblfinlem3  38035  mblfinlem4  38036  volsupnfl  38041  itg2addnclem  38047  itg2addnclem3  38049  iblmulc2nc  38061  ftc1cnnclem  38067  ftc1anclem6  38074  ftc1anclem7  38075  ftc1anclem8  38076  ftc2nc  38078  dvasin  38080  geomcau  38135  bfplem2  38199  rrncmslem  38208  rrnequiv  38211  lsatcvatlem  39550  islshpcv  39554  atlatmstc  39820  cvlsupr7  39849  cvrval3  39914  cvrval5  39916  cvrexchlem  39920  atcvrj1  39932  cvrat3  39943  cvrat4  39944  atbtwn  39947  1cvratex  39974  hlatexch4  39982  3atlem1  39984  3atlem2  39985  atcvrlln2  40020  atcvrlln  40021  lplnllnneN  40057  llncvrlpln2  40058  4atlem3b  40099  lplncvrlvol2  40116  dalemswapyz  40157  dalemswapyzps  40191  dalem25  40199  dalem39  40212  dalem58  40231  dalem59  40232  lneq2at  40279  lncvrat  40283  dalawlem2  40373  dalawlem3  40374  dalawlem4  40375  dalawlem6  40377  dalawlem9  40380  dalawlem11  40382  dalawlem12  40383  lhpocnle  40517  lhpmcvr3  40526  lhpmcvr5N  40528  lhpmcvr6N  40529  4atexlemunv  40567  4atexlemc  40570  4atexlemex2  40572  lautm  40595  cdlemc2  40693  cdleme5  40741  cdleme11j  40768  cdleme16b  40780  cdlemednpq  40800  cdleme19e  40808  cdleme20i  40818  cdleme22a  40841  cdleme22cN  40843  cdleme22d  40844  cdleme22e  40845  cdleme22eALTN  40846  cdleme22f  40847  cdleme23c  40852  cdleme30a  40879  cdleme35a  40949  cdleme35b  40951  cdleme42h  40983  cdlemeg46rgv  41029  cdlemg8b  41129  cdlemg12e  41148  cdlemg13a  41152  cdlemg17pq  41173  cdlemg18c  41181  cdlemg19  41185  cdlemg21  41187  cdlemg31d  41201  cdlemg33a  41207  tendoid  41274  cdlemk4  41335  cdlemki  41342  cdlemk10  41344  cdlemksv2  41348  cdlemk12  41351  cdlemk14  41355  cdlemk15  41356  cdlemk1u  41360  cdlemk5u  41362  cdlemk12u  41373  cdlemk45  41448  cdlemk48  41451  dia2dimlem1  41565  dia2dimlem2  41566  dia2dimlem3  41567  cdlemm10N  41619  cdlemn2  41696  dihjustlem  41717  dihglbcpreN  41801  dihmeetlem3N  41806  nnproddivdvdsd  42494  lcmineqlem17  42539  lcmineqlem18  42540  3lexlogpow2ineq1  42552  3lexlogpow2ineq2  42553  3lexlogpow5ineq5  42554  aks4d1p1p3  42563  aks4d1p1p2  42564  aks4d1p1p4  42565  aks4d1p1p5  42569  aks4d1p1  42570  aks4d1p3  42572  aks4d1p8  42581  posbezout  42594  primrootspoweq0  42600  aks6d1c1  42610  hashscontpow1  42615  aks6d1c4  42618  aks6d1c2  42624  aks6d1c5lem1  42630  aks6d1c5lem3  42631  aks6d1c5lem2  42632  deg1gprod  42634  sticksstones7  42646  sticksstones10  42649  sticksstones12  42652  sticksstones22  42662  aks6d1c6lem1  42664  aks6d1c6lem3  42666  aks6d1c6lem4  42667  bcled  42672  bcle2d  42673  aks6d1c7lem1  42674  unitscyglem4  42692  aks5lem7  42694  aks5  42698  explt1d  42809  mulgt0b2d  42977  evlselv  43048  dffltz  43093  fltdvdsabdvdsc  43097  fltaccoprm  43099  fltabcoprm  43101  flt4lem5elem  43110  flt4lem7  43118  fltnlta  43122  irrapxlem1  43276  pell1qrgaplem  43327  pell1qrgap  43328  monotoddzzfi  43396  jm2.24nn  43413  congtr  43419  congmul  43421  congsub  43424  fzmaxdif  43435  acongeq  43437  jm2.20nn  43451  jm2.25  43453  hbtlem4  43580  dgrsub2  43589  mpaaeu  43604  idomsubgmo  43647  iscard4  43986  sqrtcvallem4  44092  leeq2d  44611  int-sqgeq0d  44639  int-ineqmvtd  44644  cvgdvgrat  44766  radcnvrat  44767  hashnzfzclim  44775  dvconstbi  44787  binomcxplemdvbinom  44806  isosctrlem1ALT  45386  mulltgt0  45479  rnmptbd2lem  45700  oddfl  45734  2timesgt  45744  lt3addmuld  45757  lt4addmuld  45762  supxrgere  45786  supxrgelem  45790  supxrge  45791  xadd0ge2  45794  infrpge  45804  xrlexaddrp  45805  xralrple2  45807  infxr  45819  infleinflem1  45822  infleinflem2  45823  infleinf  45824  xralrple4  45825  xralrple3  45826  recnnltrp  45829  rpgtrecnn  45832  xrralrecnnge  45842  rexabslelem  45869  infrnmptle  45874  supminfxr  45915  xrpnf  45936  iccshift  45971  iooshift  45975  ressiocsup  46007  ressioosup  46008  fsumnncl  46025  fmul01  46033  fmul01lt1lem1  46037  fmul01lt1lem2  46038  mccllem  46050  climrec  46056  climexp  46058  climneg  46063  limcrecl  46082  sumnnodd  46083  lptioo2  46084  lptioo1  46085  ltmod  46089  lptre2pt  46091  0ellimcdiv  46100  limclner  46102  fnlimcnv  46118  climinf2lem  46157  limsupubuzlem  46163  limsup10exlem  46223  limsupgtlem  46228  dfxlim2v  46298  xlimliminflimsup  46313  cncficcgt0  46339  cncfioobdlem  46347  ioodvbdlimc1lem1  46382  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvdsn1add  46390  dvnxpaek  46393  dvnmul  46394  dvnprodlem1  46397  itgiccshift  46431  itgperiod  46432  sublevolico  46435  ismbl3  46437  ovolsplit  46439  ismbl4  46444  stoweidlem1  46452  stoweidlem11  46462  stoweidlem13  46464  stoweidlem26  46477  stoweidlem34  46485  stoweidlem38  46489  stoweidlem42  46493  stoweidlem51  46502  stoweidlem59  46510  stirlinglem5  46529  stirlinglem6  46530  stirlinglem7  46531  stirlinglem10  46534  stirlinglem11  46535  stirlinglem13  46537  stirlinglem15  46539  dirkercncflem1  46554  dirkercncflem4  46557  fourierdlem4  46562  fourierdlem10  46568  fourierdlem11  46569  fourierdlem15  46573  fourierdlem20  46578  fourierdlem25  46583  fourierdlem26  46584  fourierdlem30  46588  fourierdlem37  46595  fourierdlem39  46597  fourierdlem40  46598  fourierdlem41  46599  fourierdlem42  46600  fourierdlem44  46602  fourierdlem47  46604  fourierdlem48  46605  fourierdlem49  46606  fourierdlem50  46607  fourierdlem51  46608  fourierdlem52  46609  fourierdlem54  46611  fourierdlem60  46617  fourierdlem61  46618  fourierdlem63  46620  fourierdlem64  46621  fourierdlem65  46622  fourierdlem73  46630  fourierdlem74  46631  fourierdlem75  46632  fourierdlem76  46633  fourierdlem78  46635  fourierdlem79  46636  fourierdlem81  46638  fourierdlem84  46641  fourierdlem87  46644  fourierdlem92  46649  fourierdlem93  46650  fourierdlem101  46658  fourierdlem102  46659  fourierdlem103  46660  fourierdlem104  46661  fourierdlem111  46668  fourierdlem114  46671  sqwvfoura  46679  sqwvfourb  46680  fouriersw  46682  etransclem19  46704  etransclem23  46708  etransclem24  46709  etransclem25  46710  etransclem27  46712  etransclem32  46717  etransclem35  46720  etransclem48  46733  qndenserrnbllem  46745  ioorrnopnlem  46755  ioorrnopnxrlem  46757  fsumlesge0  46828  sge0cl  46832  sge0supre  46840  sge0less  46843  sge0gerp  46846  sge0ltfirp  46851  sge0le  46858  sge0ltfirpmpt  46859  sge0split  46860  sge0rpcpnf  46872  sge0ltfirpmpt2  46877  sge0isum  46878  sge0xaddlem1  46884  sge0pnffigtmpt  46891  sge0pnffsumgt  46893  sge0gtfsumgt  46894  sge0seq  46897  nnfoctbdjlem  46906  meassle  46914  meaiuninclem  46931  meaiininclem  46937  omeiunle  46968  omeiunltfirp  46970  carageniuncllem2  46973  carageniuncl  46974  omess0  46985  hoicvr  46999  ovnlerp  47013  ovnsubaddlem1  47021  hsphoidmvle2  47036  hoidmv1lelem2  47043  hoidmv1le  47045  hoidmvlelem1  47046  hoidmvlelem2  47047  hoidmvlelem3  47048  hoidmvlelem5  47050  ovnhoilem2  47053  ovnhoi  47054  hoidifhspdmvle  47071  hoiqssbllem2  47074  hspmbllem2  47078  hspmbllem3  47079  hspmbl  47080  vonioolem2  47132  vonicclem2  47135  smfaddlem1  47214  smflimlem2  47223  smflimlem4  47225  smfmullem1  47242  smfinflem  47268  smflimsuplem4  47274  smflimsuplem8  47278  chnsubseq  47333  perfectALTVlem2  48221  nnpw2blen  49079  itscnhlinecirc02plem1  49281  funcoppc3  49645  oppcuprcl2  49700  isinito3  49998