Theorem breqtrd 5112

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breqtrrd  5114  breqtrid  5123  domunsn  9062  mapdom2  9083  phplem2  9136  mapfien2  9319  wemaplem2  9459  infdifsn  9575  cantnff  9592  ttrclss  9638  rnttrcl  9640  infxpenlem  9932  infmap2  10136  ssfin4  10229  canthp1lem1  10572  nqereq  10855  ltexnq  10895  ltbtwnnq  10898  add20  11659  mullt0  11666  ltm1  11994  recgt0  11998  prodgt0  11999  ltmul1a  12001  mulge0b  12023  recp1lt1  12051  recreclt  12052  ledivp1  12055  ledivp1i  12078  ltdivp1i  12079  eluzmn  12792  ltaddrp2d  13017  mul2lt0bi  13047  prodge0rd  13048  xleadd1a  13202  xov1plusxeqvd  13448  fz01en  13503  fzonmapblen  13660  fladdz  13781  flhalf  13786  fldiv  13816  modsubdir  13899  fzen2  13928  serle  14016  ltexp2a  14125  leexp2a  14131  exple1  14136  expubnd  14137  bernneq  14188  expmulnbnd  14194  discr1  14198  discr  14199  faclbnd6  14258  hashfz  14386  hashfun  14396  seqcoll  14423  sqeqd  15125  01sqrexlem7  15207  sqrtge0  15216  sqrtneglem  15225  abslt  15274  absle  15275  abstri  15290  rlimge0  15540  reccn2  15556  climaddc2  15595  isercolllem1  15624  caucvgrlem  15632  summolem2a  15674  isumge0  15725  fsumle  15759  fsumlt  15760  o1fsum  15773  supcvg  15818  expcnv  15826  geolim  15832  geolim2  15833  georeclim  15834  geo2lim  15837  mertenslem1  15846  mertens  15848  prodmolem2a  15896  efcllem  16039  ef0lem  16040  efgt0  16067  eftlub  16073  eflt  16081  sinbnd  16144  cosbnd  16145  ef01bndlem  16148  sin01gt0  16154  cos01gt0  16155  sin02gt0  16156  eirrlem  16168  rpnnen2lem11  16188  rpnnen2lem12  16189  ruclem11  16204  dvdssub2  16267  dvdsadd2b  16272  dvdsexp  16294  3dvds  16297  opoe  16329  bitsfzolem  16400  bitsinv1lem  16407  bezoutlem4  16508  dvdsgcd  16510  dvdsmulgcd  16522  bezoutr1  16535  nn0seqcvgd  16536  rpmulgcd2  16622  qredeq  16623  rpdvds  16626  prmind2  16651  divdenle  16716  hashdvds  16742  phimullem  16746  eulerthlem2  16749  prmdiveq  16753  prmdivdiv  16754  pythagtriplem4  16787  pythagtriplem10  16788  pythagtriplem19  16801  iserodd  16803  pcpre1  16810  pcadd2  16858  qexpz  16869  expnprm  16870  oddprmdvds  16871  pockthlem  16873  prmreclem2  16885  prmreclem3  16886  4sqlem7  16912  4sqlem10  16915  4sqlem11  16923  4sqlem12  16924  4sqlem14  16926  4sqlem15  16927  4sqlem16  16928  0ram  16988  ffthiso  17895  latmlej12  18442  qusgrp  19158  pgpfi1  19567  sylow1lem4  19573  sylow1lem5  19574  odcau  19576  pgpfi  19577  pgpssslw  19586  sylow3lem4  19602  sylow3lem6  19604  efgsfo  19711  frgp0  19732  odadd1  19820  odadd2  19821  odadd  19822  gexexlem  19824  lt6abl  19867  gsumzsubmcl  19890  pwsgsum  19954  dprd2dlem1  20015  dprd2d2  20018  ablfacrplem  20039  ablfacrp  20040  ablfacrp2  20041  ablfac1b  20044  ablfac1eu  20047  pgpfac1lem3a  20050  ablfaclem2  20060  dvdsrid  20344  dvdsrtr  20345  dvdsrneg  20347  unitmulcl  20357  unitgrp  20360  unitnegcl  20374  subrguss  20561  subrgunit  20564  isdrng2  20717  fidomndrnglem  20746  abvsubtri  20801  orngsqr  20840  ornglmulle  20841  orngrmulle  20842  orng0le1  20848  gzrngunit  21429  prmirredlem  21468  znidomb  21557  frlmgsum  21768  psrbaglesupp  21918  psdmul  22148  psdmvr  22151  invrvald  22657  psmetsym  24291  psmettri  24292  mettri2  24322  xmetsym  24328  xmettri  24332  prdsxmetlem  24349  xblss2ps  24382  xblss2  24383  blhalf  24386  xmsge0  24444  ngptgp  24617  nrginvrcnlem  24672  nmoeq0  24717  cnmet  24752  blcvx  24779  opnreen  24813  metdcnlem  24818  metdstri  24833  metdsle  24834  metnrmlem1  24841  metnrmlem3  24843  lebnumlem1  24944  pi1inv  25035  cphnmf  25178  ipge0  25181  ipcau2  25217  tcphcphlem1  25218  csbren  25382  minveclem2  25409  minveclem3  25412  ovolssnul  25470  ovolctb  25473  ovolunnul  25483  ovoliunlem1  25485  ovoliun2  25489  ovoliunnul  25490  ioombl1lem4  25544  uniioombllem3  25568  uniioombllem4  25569  uniioombllem5  25570  uniioombl  25572  volcn  25589  vitalilem2  25592  vitalilem5  25595  itg1lea  25695  mbfi1fseqlem6  25703  mbfi1flimlem  25705  itg2eqa  25728  itg2splitlem  25731  itg2split  25732  itg2monolem1  25733  itg2cnlem2  25745  iblabsr  25813  iblmulc2  25814  bddiblnc  25825  dveflem  25962  dvef  25963  dvferm2lem  25969  dvlip  25976  c1liplem1  25979  dveq0  25983  dvlt0  25988  dvivthlem1  25991  lhop1  25997  dvfsumle  26004  dvfsumlem4  26012  dvfsumrlim3  26016  dvfsum2  26017  ftc1a  26020  ftc1lem4  26022  deg1add  26084  ply1divex  26118  ply1rem  26147  fta1glem2  26150  fta1blem  26152  ig1pdvds  26161  plyeq0lem  26191  dgrcolem2  26255  plydivlem4  26279  plyrem  26288  fta1lem  26290  aalioulem3  26317  aaliou2b  26324  aaliou3lem3  26327  aaliou3lem8  26328  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  26959  jensenlem2  26971  jensen  26972  logdiflbnd  26978  emcllem2  26980  emcllem4  26982  harmonicbnd4  26994  fsumharmonic  26995  lgamgulmlem2  27013  lgamgulm2  27019  lgambdd  27020  lgamucov  27021  lgamcvglem  27023  lgamcvg2  27038  gamcvg  27039  wilthlem3  27053  basellem1  27064  basellem3  27066  basellem4  27067  fsumdvdsdiaglem  27166  dvdsppwf1o  27169  mpodvdsmulf1o  27177  dvdsmulf1o  27179  chteq0  27192  chtub  27195  chpub  27203  logfacubnd  27204  logfaclbnd  27205  logexprlim  27208  perfectlem2  27213  dchrfi  27238  bclbnd  27263  bposlem1  27267  bposlem3  27269  bposlem4  27270  bposlem6  27272  lgslem1  27280  lgsqrlem2  27330  lgsqrlem4  27332  lgseisenlem2  27359  lgsquadlem1  27363  lgsquadlem2  27364  lgsquad2lem1  27367  2sqlem3  27403  2sqlem4  27404  2sqlem8  27409  2sqlem11  27412  2sqcoprm  27418  2sqmod  27419  chebbnd1lem2  27453  chebbnd1lem3  27454  chtppilimlem1  27456  chpchtlim  27462  vmadivsum  27465  vmadivsumb  27466  rpvmasumlem  27470  dchrisumlem2  27473  dchrmusum2  27477  dchrvmasumlem2  27481  dchrvmasumlem3  27482  dchrisum0flblem2  27492  dchrisum0fno1  27494  dchrisum0re  27496  dchrisum0lem1  27499  dchrisum0lem2a  27500  mudivsum  27513  mulogsumlem  27514  mulog2sumlem2  27518  vmalogdivsum2  27521  selberglem2  27529  selbergb  27532  selberg2b  27535  logdivbnd  27539  selberg3lem1  27540  selberg3lem2  27541  selberg4lem1  27543  pntrmax  27547  pntrlog2bndlem2  27561  pntrlog2bndlem3  27562  pntrlog2bndlem5  27564  pntrlog2bndlem6a  27565  pntrlog2bndlem6  27566  pntrlog2bnd  27567  pntpbnd1a  27568  pntpbnd1  27569  pntpbnd2  27570  pntibndlem1  27572  pntibndlem2  27574  pntlemb  27580  pntlemq  27584  pntlemr  27585  pntlemj  27586  pntlemk  27589  qabvle  27608  padicabvcxp  27615  ostth2lem2  27617  ostth2lem3  27618  ostth2lem4  27619  ostth3  27621  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  30177  eucrct2eupth  30336  nvge0  30765  smcnlem  30789  nmoub3i  30865  nmoub2i  30866  nmlno0lem  30885  minvecolem2  30967  htthlem  31009  norm3dif2  31243  bcs2  31274  chscllem2  31730  eigposi  31928  nmopub2tALT  32001  nmfnleub2  32018  nmlnop0iALT  32087  riesz1  32157  cnlnadjlem2  32160  nmopcoadji  32193  leopsq  32221  leopmul  32226  leopnmid  32230  nmopleid  32231  opsqrlem6  32237  0leopj  32278  hstle1  32318  strlem3a  32344  mdslmd4i  32425  cvexchlem  32460  cdj1i  32525  unidifsnel  32626  unidifsnne  32627  le2halvesd  32850  xlt2addrd  32853  fsumub  32922  sgnmulsgp  32937  2exple2exp  32939  oexpled  32941  wrdt2ind  33034  xrge0tsmsd  33155  fzto1st1  33184  cycpmco2lem4  33211  cycpmco2lem6  33213  cyc3conja  33239  archiabllem1a  33273  archiabllem2a  33276  archiabllem2c  33277  rprmdvdsprod  33615  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  ply1dg3rt0irred  33665  mplmulmvr  33704  mplvrpmrhm  33712  exsslsb  33762  fedgmullem1  33795  fedgmullem2  33796  fldsdrgfldext2  33828  fldextrspundgdvdslem  33846  fldextrspundgdvds  33847  fldext2rspun  33848  extdgfialglem2  33859  algextdeglem8  33890  rtelextdg2lem  33892  constrext2chnlem  33916  cos9thpiminplylem1  33948  cos9thpiminplylem2  33949  metideq  34059  metider  34060  sqsscirc1  34074  esummono  34220  esumpad2  34222  esumle  34224  esumlef  34228  esumcst  34229  esumrnmpt2  34234  esum2d  34259  aean  34410  dya2ub  34436  dya2icoseg  34443  omssubadd  34466  inelcarsg  34477  carsgsigalem  34481  carsggect  34484  carsgclctunlem2  34485  eulerpartlemb  34534  fibp1  34567  signsplypnf  34716  signsply0  34717  fdvposlt  34765  fdvposle  34767  reprgt  34787  logdivsqrle  34816  hgt750lemb  34822  hgt750leme  34824  tgoldbachgtde  34826  subfacval3  35393  sconnpht2  35442  sconnpi1  35443  resconn  35450  snmlff  35533  sinccvglem  35876  faclimlem2  35948  btwnouttr2  36226  weiunpo  36669  dnibndlem5  36764  dnibndlem7  36766  dnibndlem8  36767  dnibndlem9  36768  dnibndlem10  36769  dnibnd  36773  knoppcnlem4  36778  knoppcnlem9  36783  unbdqndv2lem1  36791  unbdqndv2lem2  36792  knoppndvlem11  36804  knoppndvlem12  36805  knoppndvlem14  36807  knoppndvlem15  36808  knoppndvlem17  36810  knoppndvlem18  36811  knoppndvlem19  36812  knoppndvlem21  36814  ltflcei  37951  poimirlem9  37972  poimirlem26  37989  poimirlem27  37990  poimirlem29  37992  heicant  37998  mblfinlem2  38001  mblfinlem3  38002  mblfinlem4  38003  volsupnfl  38008  itg2addnclem  38014  itg2addnclem3  38016  iblmulc2nc  38028  ftc1cnnclem  38034  ftc1anclem6  38041  ftc1anclem7  38042  ftc1anclem8  38043  ftc2nc  38045  dvasin  38047  geomcau  38102  bfplem2  38166  rrncmslem  38175  rrnequiv  38178  lsatcvatlem  39517  islshpcv  39521  atlatmstc  39787  cvlsupr7  39816  cvrval3  39881  cvrval5  39883  cvrexchlem  39887  atcvrj1  39899  cvrat3  39910  cvrat4  39911  atbtwn  39914  1cvratex  39941  hlatexch4  39949  3atlem1  39951  3atlem2  39952  atcvrlln2  39987  atcvrlln  39988  lplnllnneN  40024  llncvrlpln2  40025  4atlem3b  40066  lplncvrlvol2  40083  dalemswapyz  40124  dalemswapyzps  40158  dalem25  40166  dalem39  40179  dalem58  40198  dalem59  40199  lneq2at  40246  lncvrat  40250  dalawlem2  40340  dalawlem3  40341  dalawlem4  40342  dalawlem6  40344  dalawlem9  40347  dalawlem11  40349  dalawlem12  40350  lhpocnle  40484  lhpmcvr3  40493  lhpmcvr5N  40495  lhpmcvr6N  40496  4atexlemunv  40534  4atexlemc  40537  4atexlemex2  40539  lautm  40562  cdlemc2  40660  cdleme5  40708  cdleme11j  40735  cdleme16b  40747  cdlemednpq  40767  cdleme19e  40775  cdleme20i  40785  cdleme22a  40808  cdleme22cN  40810  cdleme22d  40811  cdleme22e  40812  cdleme22eALTN  40813  cdleme22f  40814  cdleme23c  40819  cdleme30a  40846  cdleme35a  40916  cdleme35b  40918  cdleme42h  40950  cdlemeg46rgv  40996  cdlemg8b  41096  cdlemg12e  41115  cdlemg13a  41119  cdlemg17pq  41140  cdlemg18c  41148  cdlemg19  41152  cdlemg21  41154  cdlemg31d  41168  cdlemg33a  41174  tendoid  41241  cdlemk4  41302  cdlemki  41309  cdlemk10  41311  cdlemksv2  41315  cdlemk12  41318  cdlemk14  41322  cdlemk15  41323  cdlemk1u  41327  cdlemk5u  41329  cdlemk12u  41340  cdlemk45  41415  cdlemk48  41418  dia2dimlem1  41532  dia2dimlem2  41533  dia2dimlem3  41534  cdlemm10N  41586  cdlemn2  41663  dihjustlem  41684  dihglbcpreN  41768  dihmeetlem3N  41773  nnproddivdvdsd  42461  lcmineqlem17  42506  lcmineqlem18  42507  3lexlogpow2ineq1  42519  3lexlogpow2ineq2  42520  3lexlogpow5ineq5  42521  aks4d1p1p3  42530  aks4d1p1p2  42531  aks4d1p1p4  42532  aks4d1p1p5  42536  aks4d1p1  42537  aks4d1p3  42539  aks4d1p8  42548  posbezout  42561  primrootspoweq0  42567  aks6d1c1  42577  hashscontpow1  42582  aks6d1c4  42585  aks6d1c2  42591  aks6d1c5lem1  42597  aks6d1c5lem3  42598  aks6d1c5lem2  42599  deg1gprod  42601  sticksstones7  42613  sticksstones10  42616  sticksstones12  42619  sticksstones22  42629  aks6d1c6lem1  42631  aks6d1c6lem3  42633  aks6d1c6lem4  42634  bcled  42639  bcle2d  42640  aks6d1c7lem1  42641  unitscyglem4  42659  aks5lem7  42661  aks5  42665  explt1d  42777  mulgt0b2d  42945  evlselv  43042  dffltz  43089  fltdvdsabdvdsc  43093  fltaccoprm  43095  fltabcoprm  43097  flt4lem5elem  43106  flt4lem7  43114  fltnlta  43118  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  45703  oddfl  45737  2timesgt  45747  lt3addmuld  45760  lt4addmuld  45765  supxrgere  45789  supxrgelem  45793  supxrge  45794  xadd0ge2  45797  infrpge  45807  xrlexaddrp  45808  xralrple2  45810  infxr  45822  infleinflem1  45825  infleinflem2  45826  infleinf  45827  xralrple4  45828  xralrple3  45829  recnnltrp  45832  rpgtrecnn  45835  xrralrecnnge  45845  rexabslelem  45872  infrnmptle  45877  supminfxr  45918  xrpnf  45939  iccshift  45974  iooshift  45978  ressiocsup  46010  ressioosup  46011  fsumnncl  46028  fmul01  46036  fmul01lt1lem1  46040  fmul01lt1lem2  46041  mccllem  46053  climrec  46059  climexp  46061  climneg  46066  limcrecl  46085  sumnnodd  46086  lptioo2  46087  lptioo1  46088  ltmod  46092  lptre2pt  46094  0ellimcdiv  46103  limclner  46105  fnlimcnv  46121  climinf2lem  46160  limsupubuzlem  46166  limsup10exlem  46226  limsupgtlem  46231  dfxlim2v  46301  xlimliminflimsup  46316  cncficcgt0  46342  cncfioobdlem  46350  ioodvbdlimc1lem1  46385  ioodvbdlimc1lem2  46386  ioodvbdlimc2lem  46388  dvdsn1add  46393  dvnxpaek  46396  dvnmul  46397  dvnprodlem1  46400  itgiccshift  46434  itgperiod  46435  sublevolico  46438  ismbl3  46440  ovolsplit  46442  ismbl4  46447  stoweidlem1  46455  stoweidlem11  46465  stoweidlem13  46467  stoweidlem26  46480  stoweidlem34  46488  stoweidlem38  46492  stoweidlem42  46496  stoweidlem51  46505  stoweidlem59  46513  stirlinglem5  46532  stirlinglem6  46533  stirlinglem7  46534  stirlinglem10  46537  stirlinglem11  46538  stirlinglem13  46540  stirlinglem15  46542  dirkercncflem1  46557  dirkercncflem4  46560  fourierdlem4  46565  fourierdlem10  46571  fourierdlem11  46572  fourierdlem15  46576  fourierdlem20  46581  fourierdlem25  46586  fourierdlem26  46587  fourierdlem30  46591  fourierdlem37  46598  fourierdlem39  46600  fourierdlem40  46601  fourierdlem41  46602  fourierdlem42  46603  fourierdlem44  46605  fourierdlem47  46607  fourierdlem48  46608  fourierdlem49  46609  fourierdlem50  46610  fourierdlem51  46611  fourierdlem52  46612  fourierdlem54  46614  fourierdlem60  46620  fourierdlem61  46621  fourierdlem63  46623  fourierdlem64  46624  fourierdlem65  46625  fourierdlem73  46633  fourierdlem74  46634  fourierdlem75  46635  fourierdlem76  46636  fourierdlem78  46638  fourierdlem79  46639  fourierdlem81  46641  fourierdlem84  46644  fourierdlem87  46647  fourierdlem92  46652  fourierdlem93  46653  fourierdlem101  46661  fourierdlem102  46662  fourierdlem103  46663  fourierdlem104  46664  fourierdlem111  46671  fourierdlem114  46674  sqwvfoura  46682  sqwvfourb  46683  fouriersw  46685  etransclem19  46707  etransclem23  46711  etransclem24  46712  etransclem25  46713  etransclem27  46715  etransclem32  46720  etransclem35  46723  etransclem48  46736  qndenserrnbllem  46748  ioorrnopnlem  46758  ioorrnopnxrlem  46760  fsumlesge0  46831  sge0cl  46835  sge0supre  46843  sge0less  46846  sge0gerp  46849  sge0ltfirp  46854  sge0le  46861  sge0ltfirpmpt  46862  sge0split  46863  sge0rpcpnf  46875  sge0ltfirpmpt2  46880  sge0isum  46881  sge0xaddlem1  46887  sge0pnffigtmpt  46894  sge0pnffsumgt  46896  sge0gtfsumgt  46897  sge0seq  46900  nnfoctbdjlem  46909  meassle  46917  meaiuninclem  46934  meaiininclem  46940  omeiunle  46971  omeiunltfirp  46973  carageniuncllem2  46976  carageniuncl  46977  omess0  46988  hoicvr  47002  ovnlerp  47016  ovnsubaddlem1  47024  hsphoidmvle2  47039  hoidmv1lelem2  47046  hoidmv1le  47048  hoidmvlelem1  47049  hoidmvlelem2  47050  hoidmvlelem3  47051  hoidmvlelem5  47053  ovnhoilem2  47056  ovnhoi  47057  hoidifhspdmvle  47074  hoiqssbllem2  47077  hspmbllem2  47081  hspmbllem3  47082  hspmbl  47083  vonioolem2  47135  vonicclem2  47138  smfaddlem1  47217  smflimlem2  47226  smflimlem4  47228  smfmullem1  47245  smfinflem  47271  smflimsuplem4  47277  smflimsuplem8  47281  chnsubseq  47334  perfectALTVlem2  48218  nnpw2blen  49076  itscnhlinecirc02plem1  49278  funcoppc3  49642  oppcuprcl2  49697  isinito3  49995