Theorem breqtrd 5100

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075

This theorem is referenced by:  breqtrrd  5102  breqtrid  5111  domunsn  9059  mapdom2  9080  phplem2  9133  mapfien2  9316  wemaplem2  9456  infdifsn  9573  cantnff  9590  ttrclss  9636  rnttrcl  9638  infxpenlem  9930  infmap2  10134  ssfin4  10228  canthp1lem1  10571  nqereq  10854  ltexnq  10894  ltbtwnnq  10897  add20  11658  mullt0  11665  ltm1  11992  recgt0  11996  prodgt0  11997  ltmul1a  11999  mulge0b  12021  recp1lt1  12049  recreclt  12050  ledivp1  12053  ledivp1i  12076  ltdivp1i  12077  eluzmn  12790  ltaddrp2d  13015  mul2lt0bi  13045  prodge0rd  13046  xleadd1a  13200  xov1plusxeqvd  13446  fz01en  13501  fzonmapblen  13658  fladdz  13779  flhalf  13784  fldiv  13814  modsubdir  13897  fzen2  13926  serle  14014  ltexp2a  14123  leexp2a  14129  exple1  14134  expubnd  14135  bernneq  14186  expmulnbnd  14192  discr1  14196  discr  14197  faclbnd6  14256  hashfz  14384  hashfun  14394  seqcoll  14421  sqeqd  15123  01sqrexlem7  15205  sqrtge0  15214  sqrtneglem  15223  abslt  15272  absle  15273  abstri  15288  rlimge0  15538  reccn2  15554  climaddc2  15593  isercolllem1  15622  caucvgrlem  15630  summolem2a  15672  isumge0  15723  fsumle  15757  fsumlt  15758  o1fsum  15771  supcvg  15816  expcnv  15824  geolim  15830  geolim2  15831  georeclim  15832  geo2lim  15835  mertenslem1  15844  mertens  15846  prodmolem2a  15894  efcllem  16037  ef0lem  16038  efgt0  16065  eftlub  16071  eflt  16079  sinbnd  16142  cosbnd  16143  ef01bndlem  16146  sin01gt0  16152  cos01gt0  16153  sin02gt0  16154  eirrlem  16166  rpnnen2lem11  16186  rpnnen2lem12  16187  ruclem11  16202  dvdssub2  16265  dvdsadd2b  16270  dvdsexp  16292  3dvds  16295  opoe  16327  bitsfzolem  16398  bitsinv1lem  16405  bezoutlem4  16506  dvdsgcd  16508  dvdsmulgcd  16520  bezoutr1  16533  nn0seqcvgd  16534  rpmulgcd2  16620  qredeq  16621  rpdvds  16624  prmind2  16649  divdenle  16714  hashdvds  16740  phimullem  16744  eulerthlem2  16747  prmdiveq  16751  prmdivdiv  16752  pythagtriplem4  16785  pythagtriplem10  16786  pythagtriplem19  16799  iserodd  16801  pcpre1  16808  pcadd2  16856  qexpz  16867  expnprm  16868  oddprmdvds  16869  pockthlem  16871  prmreclem2  16883  prmreclem3  16884  4sqlem7  16910  4sqlem10  16913  4sqlem11  16921  4sqlem12  16922  4sqlem14  16924  4sqlem15  16925  4sqlem16  16926  0ram  16986  ffthiso  17893  latmlej12  18440  qusgrp  19156  pgpfi1  19564  sylow1lem4  19570  sylow1lem5  19571  odcau  19573  pgpfi  19574  pgpssslw  19583  sylow3lem4  19599  sylow3lem6  19601  efgsfo  19708  frgp0  19729  odadd1  19817  odadd2  19818  odadd  19819  gexexlem  19821  lt6abl  19864  gsumzsubmcl  19887  pwsgsum  19951  dprd2dlem1  20012  dprd2d2  20015  ablfacrplem  20036  ablfacrp  20037  ablfacrp2  20038  ablfac1b  20041  ablfac1eu  20044  pgpfac1lem3a  20047  ablfaclem2  20057  dvdsrid  20341  dvdsrtr  20342  dvdsrneg  20344  unitmulcl  20354  unitgrp  20357  unitnegcl  20371  subrguss  20562  subrgunit  20565  isdrng2  20718  fidomndrnglem  20747  abvsubtri  20802  orngsqr  20841  ornglmulle  20842  orngrmulle  20843  orng0le1  20849  gzrngunit  21411  prmirredlem  21450  znidomb  21539  frlmgsum  21750  psrbaglesupp  21900  psdmul  22157  psdmvr  22160  invrvald  22662  psmetsym  24296  psmettri  24297  mettri2  24327  xmetsym  24333  xmettri  24337  prdsxmetlem  24354  xblss2ps  24387  xblss2  24388  blhalf  24391  xmsge0  24449  ngptgp  24622  nrginvrcnlem  24677  nmoeq0  24722  cnmet  24757  blcvx  24784  opnreen  24818  metdcnlem  24823  metdstri  24838  metdsle  24839  metnrmlem1  24846  metnrmlem3  24848  lebnumlem1  24949  pi1inv  25040  cphnmf  25183  ipge0  25186  ipcau2  25222  tcphcphlem1  25223  csbren  25387  minveclem2  25414  minveclem3  25417  ovolssnul  25475  ovolctb  25478  ovolunnul  25488  ovoliunlem1  25490  ovoliun2  25494  ovoliunnul  25495  ioombl1lem4  25549  uniioombllem3  25573  uniioombllem4  25574  uniioombllem5  25575  uniioombl  25577  volcn  25594  vitalilem2  25597  vitalilem5  25600  itg1lea  25700  mbfi1fseqlem6  25708  mbfi1flimlem  25710  itg2eqa  25733  itg2splitlem  25736  itg2split  25737  itg2monolem1  25738  itg2cnlem2  25750  iblabsr  25818  iblmulc2  25819  bddiblnc  25830  dveflem  25967  dvef  25968  dvferm2lem  25974  dvlip  25981  c1liplem1  25984  dveq0  25988  dvlt0  25993  dvivthlem1  25996  lhop1  26002  dvfsumle  26009  dvfsumlem4  26017  dvfsumrlim3  26021  dvfsum2  26022  ftc1a  26025  ftc1lem4  26027  deg1add  26089  ply1divex  26123  ply1rem  26152  fta1glem2  26155  fta1blem  26157  ig1pdvds  26166  plyeq0lem  26196  dgrcolem2  26260  plydivlem4  26283  plyrem  26292  fta1lem  26294  aalioulem3  26321  aaliou2b  26328  aaliou3lem3  26331  aaliou3lem8  26332  ulmcn  26385  ulmdvlem1  26386  itgulm  26394  pserulm  26408  pserdvlem2  26414  abelthlem2  26418  abelthlem5  26421  abelthlem6  26422  abelthlem7  26424  abelthlem8  26425  abelthlem9  26426  sinq12gt0  26492  sinq34lt0t  26494  cosq14gt0  26495  cosq14ge0  26496  cos02pilt1  26511  efif1olem3  26529  argimgt0  26597  argimlt0  26598  logneg2  26600  logcnlem3  26629  logcnlem4  26630  logtayllem  26644  logtayl2  26647  cxpsqrtlem  26687  cxpsqrt  26688  cxpaddlelem  26736  abscxpbnd  26738  zrtdvds  26744  rtprmirr  26745  loglesqrt  26746  ang180lem2  26795  atanlogaddlem  26898  atanlogsublem  26900  atantan  26908  atans2  26916  atantayl  26922  leibpi  26927  log2tlbnd  26930  birthdaylem2  26937  birthdaylem3  26938  cxp2limlem  26960  jensenlem2  26972  jensen  26973  logdiflbnd  26979  emcllem2  26981  emcllem4  26983  harmonicbnd4  26995  fsumharmonic  26996  lgamgulmlem2  27014  lgamgulm2  27020  lgambdd  27021  lgamucov  27022  lgamcvglem  27024  lgamcvg2  27039  gamcvg  27040  wilthlem3  27054  basellem1  27065  basellem3  27067  basellem4  27068  fsumdvdsdiaglem  27167  dvdsppwf1o  27170  mpodvdsmulf1o  27178  dvdsmulf1o  27180  chteq0  27193  chtub  27196  chpub  27204  logfacubnd  27205  logfaclbnd  27206  logexprlim  27209  perfectlem2  27214  dchrfi  27239  bclbnd  27264  bposlem1  27268  bposlem3  27270  bposlem4  27271  bposlem6  27273  lgslem1  27281  lgsqrlem2  27331  lgsqrlem4  27333  lgseisenlem2  27360  lgsquadlem1  27364  lgsquadlem2  27365  lgsquad2lem1  27368  2sqlem3  27404  2sqlem4  27405  2sqlem8  27410  2sqlem11  27413  2sqcoprm  27419  2sqmod  27420  chebbnd1lem2  27454  chebbnd1lem3  27455  chtppilimlem1  27457  chpchtlim  27463  vmadivsum  27466  vmadivsumb  27467  rpvmasumlem  27471  dchrisumlem2  27474  dchrmusum2  27478  dchrvmasumlem2  27482  dchrvmasumlem3  27483  dchrisum0flblem2  27493  dchrisum0fno1  27495  dchrisum0re  27497  dchrisum0lem1  27500  dchrisum0lem2a  27501  mudivsum  27514  mulogsumlem  27515  mulog2sumlem2  27519  vmalogdivsum2  27522  selberglem2  27530  selbergb  27533  selberg2b  27536  logdivbnd  27540  selberg3lem1  27541  selberg3lem2  27542  selberg4lem1  27544  pntrmax  27548  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem5  27565  pntrlog2bndlem6a  27566  pntrlog2bndlem6  27567  pntrlog2bnd  27568  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem1  27573  pntibndlem2  27575  pntlemb  27581  pntlemq  27585  pntlemr  27586  pntlemj  27587  pntlemk  27590  qabvle  27609  padicabvcxp  27616  ostth2lem2  27618  ostth2lem3  27619  ostth2lem4  27620  ostth3  27622  addsuniflem  28013  negsid  28053  negsunif  28067  negright  28071  mulsuniflem  28161  ltmuls2  28183  precsexlem9  28227  absmuls  28256  zcuts  28419  addhalfcut  28471  pw2cut2  28474  bdayfinbndlem1  28479  z12sge0  28495  legtrid  28679  legov3  28686  krippenlem  28778  mideulem2  28822  midex  28825  opphllem5  28839  opphllem6  28840  opphl  28842  lmieu  28872  lmiisolem  28884  ttgcontlem1  28973  colinearalglem4  28998  axpaschlem  29029  axcontlem7  29059  nbfusgrlevtxm2  29467  clwlksndivn  30176  eucrct2eupth  30335  nvge0  30764  smcnlem  30788  nmoub3i  30864  nmoub2i  30865  nmlno0lem  30884  minvecolem2  30966  htthlem  31008  norm3dif2  31242  bcs2  31273  chscllem2  31729  eigposi  31927  nmopub2tALT  32000  nmfnleub2  32017  nmlnop0iALT  32086  riesz1  32156  cnlnadjlem2  32159  nmopcoadji  32192  leopsq  32220  leopmul  32225  leopnmid  32229  nmopleid  32230  opsqrlem6  32236  0leopj  32277  hstle1  32317  strlem3a  32343  mdslmd4i  32424  cvexchlem  32459  cdj1i  32524  unidifsnel  32625  unidifsnne  32626  le2halvesd  32850  xlt2addrd  32853  fsumub  32922  sgnmulsgp  32937  2exple2exp  32939  oexpled  32941  wrdt2ind  33034  xrge0tsmsd  33156  fzto1st1  33185  cycpmco2lem4  33212  cycpmco2lem6  33214  cyc3conja  33240  archiabllem1a  33274  archiabllem2a  33277  archiabllem2c  33278  rprmdvdsprod  33627  1arithidomlem1  33628  1arithidomlem2  33629  1arithidom  33630  ply1dg3rt0irred  33677  mplmulmvr  33733  mplvrpmrhm  33741  exsslsb  33791  fedgmullem1  33823  fedgmullem2  33824  fldsdrgfldext2  33856  fldextrspundgdvdslem  33874  fldextrspundgdvds  33875  fldext2rspun  33876  extdgfialglem2  33887  algextdeglem8  33918  rtelextdg2lem  33920  constrext2chnlem  33944  cos9thpiminplylem1  33976  cos9thpiminplylem2  33977  metideq  34087  metider  34088  sqsscirc1  34102  esummono  34248  esumpad2  34250  esumle  34252  esumlef  34256  esumcst  34257  esumrnmpt2  34262  esum2d  34287  aean  34438  dya2ub  34464  dya2icoseg  34471  omssubadd  34494  inelcarsg  34505  carsgsigalem  34509  carsggect  34512  carsgclctunlem2  34513  eulerpartlemb  34562  fibp1  34595  signsplypnf  34744  signsply0  34745  fdvposlt  34793  fdvposle  34795  reprgt  34815  logdivsqrle  34844  hgt750lemb  34850  hgt750leme  34852  tgoldbachgtde  34854  subfacval3  35430  sconnpht2  35479  sconnpi1  35480  resconn  35487  snmlff  35570  sinccvglem  35913  faclimlem2  35985  btwnouttr2  36263  weiunpo  36706  dnibndlem5  36801  dnibndlem7  36803  dnibndlem8  36804  dnibndlem9  36805  dnibndlem10  36806  dnibnd  36810  knoppcnlem4  36815  knoppcnlem9  36820  unbdqndv2lem1  36828  unbdqndv2lem2  36829  knoppndvlem11  36841  knoppndvlem12  36842  knoppndvlem14  36844  knoppndvlem15  36845  knoppndvlem17  36847  knoppndvlem18  36848  knoppndvlem19  36849  knoppndvlem21  36851  ltflcei  37988  poimirlem9  38009  poimirlem26  38026  poimirlem27  38027  poimirlem29  38029  heicant  38035  mblfinlem2  38038  mblfinlem3  38039  mblfinlem4  38040  volsupnfl  38045  itg2addnclem  38051  itg2addnclem3  38053  iblmulc2nc  38065  ftc1cnnclem  38071  ftc1anclem6  38078  ftc1anclem7  38079  ftc1anclem8  38080  ftc2nc  38082  dvasin  38084  geomcau  38139  bfplem2  38203  rrncmslem  38212  rrnequiv  38215  lsatcvatlem  39554  islshpcv  39558  atlatmstc  39824  cvlsupr7  39853  cvrval3  39918  cvrval5  39920  cvrexchlem  39924  atcvrj1  39936  cvrat3  39947  cvrat4  39948  atbtwn  39951  1cvratex  39978  hlatexch4  39986  3atlem1  39988  3atlem2  39989  atcvrlln2  40024  atcvrlln  40025  lplnllnneN  40061  llncvrlpln2  40062  4atlem3b  40103  lplncvrlvol2  40120  dalemswapyz  40161  dalemswapyzps  40195  dalem25  40203  dalem39  40216  dalem58  40235  dalem59  40236  lneq2at  40283  lncvrat  40287  dalawlem2  40377  dalawlem3  40378  dalawlem4  40379  dalawlem6  40381  dalawlem9  40384  dalawlem11  40386  dalawlem12  40387  lhpocnle  40521  lhpmcvr3  40530  lhpmcvr5N  40532  lhpmcvr6N  40533  4atexlemunv  40571  4atexlemc  40574  4atexlemex2  40576  lautm  40599  cdlemc2  40697  cdleme5  40745  cdleme11j  40772  cdleme16b  40784  cdlemednpq  40804  cdleme19e  40812  cdleme20i  40822  cdleme22a  40845  cdleme22cN  40847  cdleme22d  40848  cdleme22e  40849  cdleme22eALTN  40850  cdleme22f  40851  cdleme23c  40856  cdleme30a  40883  cdleme35a  40953  cdleme35b  40955  cdleme42h  40987  cdlemeg46rgv  41033  cdlemg8b  41133  cdlemg12e  41152  cdlemg13a  41156  cdlemg17pq  41177  cdlemg18c  41185  cdlemg19  41189  cdlemg21  41191  cdlemg31d  41205  cdlemg33a  41211  tendoid  41278  cdlemk4  41339  cdlemki  41346  cdlemk10  41348  cdlemksv2  41352  cdlemk12  41355  cdlemk14  41359  cdlemk15  41360  cdlemk1u  41364  cdlemk5u  41366  cdlemk12u  41377  cdlemk45  41452  cdlemk48  41455  dia2dimlem1  41569  dia2dimlem2  41570  dia2dimlem3  41571  cdlemm10N  41623  cdlemn2  41700  dihjustlem  41721  dihglbcpreN  41805  dihmeetlem3N  41810  nnproddivdvdsd  42498  lcmineqlem17  42543  lcmineqlem18  42544  3lexlogpow2ineq1  42556  3lexlogpow2ineq2  42557  3lexlogpow5ineq5  42558  aks4d1p1p3  42567  aks4d1p1p2  42568  aks4d1p1p4  42569  aks4d1p1p5  42573  aks4d1p1  42574  aks4d1p3  42576  aks4d1p8  42585  posbezout  42598  primrootspoweq0  42604  aks6d1c1  42614  hashscontpow1  42619  aks6d1c4  42622  aks6d1c2  42628  aks6d1c5lem1  42634  aks6d1c5lem3  42635  aks6d1c5lem2  42636  deg1gprod  42638  sticksstones7  42650  sticksstones10  42653  sticksstones12  42656  sticksstones22  42666  aks6d1c6lem1  42668  aks6d1c6lem3  42670  aks6d1c6lem4  42671  bcled  42676  bcle2d  42677  aks6d1c7lem1  42678  unitscyglem4  42696  aks5lem7  42698  aks5  42702  explt1d  42813  mulgt0b2d  42981  evlselv  43052  dffltz  43097  fltdvdsabdvdsc  43101  fltaccoprm  43103  fltabcoprm  43105  flt4lem5elem  43114  flt4lem7  43122  fltnlta  43126  irrapxlem1  43280  pell1qrgaplem  43331  pell1qrgap  43332  monotoddzzfi  43400  jm2.24nn  43417  congtr  43423  congmul  43425  congsub  43428  fzmaxdif  43439  acongeq  43441  jm2.20nn  43455  jm2.25  43457  hbtlem4  43584  dgrsub2  43593  mpaaeu  43608  idomsubgmo  43651  iscard4  43990  sqrtcvallem4  44096  leeq2d  44615  int-sqgeq0d  44643  int-ineqmvtd  44648  cvgdvgrat  44770  radcnvrat  44771  hashnzfzclim  44779  dvconstbi  44791  binomcxplemdvbinom  44810  isosctrlem1ALT  45390  mulltgt0  45483  rnmptbd2lem  45704  oddfl  45738  2timesgt  45748  lt3addmuld  45761  lt4addmuld  45766  supxrgere  45790  supxrgelem  45794  supxrge  45795  xadd0ge2  45798  infrpge  45808  xrlexaddrp  45809  xralrple2  45811  infxr  45823  infleinflem1  45826  infleinflem2  45827  infleinf  45828  xralrple4  45829  xralrple3  45830  recnnltrp  45833  rpgtrecnn  45836  xrralrecnnge  45846  rexabslelem  45873  infrnmptle  45878  supminfxr  45919  xrpnf  45940  iccshift  45975  iooshift  45979  ressiocsup  46011  ressioosup  46012  fsumnncl  46029  fmul01  46037  fmul01lt1lem1  46041  fmul01lt1lem2  46042  mccllem  46054  climrec  46060  climexp  46062  climneg  46067  limcrecl  46086  sumnnodd  46087  lptioo2  46088  lptioo1  46089  ltmod  46093  lptre2pt  46095  0ellimcdiv  46104  limclner  46106  fnlimcnv  46122  climinf2lem  46161  limsupubuzlem  46167  limsup10exlem  46227  limsupgtlem  46232  dfxlim2v  46302  xlimliminflimsup  46317  cncficcgt0  46343  cncfioobdlem  46351  ioodvbdlimc1lem1  46386  ioodvbdlimc1lem2  46387  ioodvbdlimc2lem  46389  dvdsn1add  46394  dvnxpaek  46397  dvnmul  46398  dvnprodlem1  46401  itgiccshift  46435  itgperiod  46436  sublevolico  46439  ismbl3  46441  ovolsplit  46443  ismbl4  46448  stoweidlem1  46456  stoweidlem11  46466  stoweidlem13  46468  stoweidlem26  46481  stoweidlem34  46489  stoweidlem38  46493  stoweidlem42  46497  stoweidlem51  46506  stoweidlem59  46514  stirlinglem5  46533  stirlinglem6  46534  stirlinglem7  46535  stirlinglem10  46538  stirlinglem11  46539  stirlinglem13  46541  stirlinglem15  46543  dirkercncflem1  46558  dirkercncflem4  46561  fourierdlem4  46566  fourierdlem10  46572  fourierdlem11  46573  fourierdlem15  46577  fourierdlem20  46582  fourierdlem25  46587  fourierdlem26  46588  fourierdlem30  46592  fourierdlem37  46599  fourierdlem39  46601  fourierdlem40  46602  fourierdlem41  46603  fourierdlem42  46604  fourierdlem44  46606  fourierdlem47  46608  fourierdlem48  46609  fourierdlem49  46610  fourierdlem50  46611  fourierdlem51  46612  fourierdlem52  46613  fourierdlem54  46615  fourierdlem60  46621  fourierdlem61  46622  fourierdlem63  46624  fourierdlem64  46625  fourierdlem65  46626  fourierdlem73  46634  fourierdlem74  46635  fourierdlem75  46636  fourierdlem76  46637  fourierdlem78  46639  fourierdlem79  46640  fourierdlem81  46642  fourierdlem84  46645  fourierdlem87  46648  fourierdlem92  46653  fourierdlem93  46654  fourierdlem101  46662  fourierdlem102  46663  fourierdlem103  46664  fourierdlem104  46665  fourierdlem111  46672  fourierdlem114  46675  sqwvfoura  46683  sqwvfourb  46684  fouriersw  46686  etransclem19  46708  etransclem23  46712  etransclem24  46713  etransclem25  46714  etransclem27  46716  etransclem32  46721  etransclem35  46724  etransclem48  46737  qndenserrnbllem  46749  ioorrnopnlem  46759  ioorrnopnxrlem  46761  fsumlesge0  46832  sge0cl  46836  sge0supre  46844  sge0less  46847  sge0gerp  46850  sge0ltfirp  46855  sge0le  46862  sge0ltfirpmpt  46863  sge0split  46864  sge0rpcpnf  46876  sge0ltfirpmpt2  46881  sge0isum  46882  sge0xaddlem1  46888  sge0pnffigtmpt  46895  sge0pnffsumgt  46897  sge0gtfsumgt  46898  sge0seq  46901  nnfoctbdjlem  46910  meassle  46918  meaiuninclem  46935  meaiininclem  46941  omeiunle  46972  omeiunltfirp  46974  carageniuncllem2  46977  carageniuncl  46978  omess0  46989  hoicvr  47003  ovnlerp  47017  ovnsubaddlem1  47025  hsphoidmvle2  47040  hoidmv1lelem2  47047  hoidmv1le  47049  hoidmvlelem1  47050  hoidmvlelem2  47051  hoidmvlelem3  47052  hoidmvlelem5  47054  ovnhoilem2  47057  ovnhoi  47058  hoidifhspdmvle  47075  hoiqssbllem2  47078  hspmbllem2  47082  hspmbllem3  47083  hspmbl  47084  vonioolem2  47136  vonicclem2  47139  smfaddlem1  47218  smflimlem2  47227  smflimlem4  47229  smfmullem1  47246  smfinflem  47272  smflimsuplem4  47278  smflimsuplem8  47282  chnsubseq  47337  perfectALTVlem2  48225  nnpw2blen  49083  itscnhlinecirc02plem1  49285  funcoppc3  49649  oppcuprcl2  49704  isinito3  50002