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 232	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  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  9054  mapdom2  9075  phplem2  9128  mapfien2  9311  wemaplem2  9451  infdifsn  9567  cantnff  9584  ttrclss  9630  rnttrcl  9632  infxpenlem  9924  infmap2  10128  ssfin4  10221  canthp1lem1  10564  nqereq  10847  ltexnq  10887  ltbtwnnq  10890  add20  11651  mullt0  11658  ltm1  11986  recgt0  11990  prodgt0  11991  ltmul1a  11993  mulge0b  12015  recp1lt1  12043  recreclt  12044  ledivp1  12047  ledivp1i  12070  ltdivp1i  12071  eluzmn  12784  ltaddrp2d  13009  mul2lt0bi  13039  prodge0rd  13040  xleadd1a  13194  xov1plusxeqvd  13440  fz01en  13495  fzonmapblen  13652  fladdz  13773  flhalf  13778  fldiv  13808  modsubdir  13891  fzen2  13920  serle  14008  ltexp2a  14117  leexp2a  14123  exple1  14128  expubnd  14129  bernneq  14180  expmulnbnd  14186  discr1  14190  discr  14191  faclbnd6  14250  hashfz  14378  hashfun  14388  seqcoll  14415  sqeqd  15117  01sqrexlem7  15199  sqrtge0  15208  sqrtneglem  15217  abslt  15266  absle  15267  abstri  15282  rlimge0  15532  reccn2  15548  climaddc2  15587  isercolllem1  15616  caucvgrlem  15624  summolem2a  15666  isumge0  15717  fsumle  15751  fsumlt  15752  o1fsum  15765  supcvg  15810  expcnv  15818  geolim  15824  geolim2  15825  georeclim  15826  geo2lim  15829  mertenslem1  15838  mertens  15840  prodmolem2a  15888  efcllem  16031  ef0lem  16032  efgt0  16059  eftlub  16065  eflt  16073  sinbnd  16136  cosbnd  16137  ef01bndlem  16140  sin01gt0  16146  cos01gt0  16147  sin02gt0  16148  eirrlem  16160  rpnnen2lem11  16180  rpnnen2lem12  16181  ruclem11  16196  dvdssub2  16259  dvdsadd2b  16264  dvdsexp  16286  3dvds  16289  opoe  16321  bitsfzolem  16392  bitsinv1lem  16399  bezoutlem4  16500  dvdsgcd  16502  dvdsmulgcd  16514  bezoutr1  16527  nn0seqcvgd  16528  rpmulgcd2  16614  qredeq  16615  rpdvds  16618  prmind2  16643  divdenle  16708  hashdvds  16734  phimullem  16738  eulerthlem2  16741  prmdiveq  16745  prmdivdiv  16746  pythagtriplem4  16779  pythagtriplem10  16780  pythagtriplem19  16793  iserodd  16795  pcpre1  16802  pcadd2  16850  qexpz  16861  expnprm  16862  oddprmdvds  16863  pockthlem  16865  prmreclem2  16877  prmreclem3  16878  4sqlem7  16904  4sqlem10  16907  4sqlem11  16915  4sqlem12  16916  4sqlem14  16918  4sqlem15  16919  4sqlem16  16920  0ram  16980  ffthiso  17887  latmlej12  18434  qusgrp  19150  pgpfi1  19559  sylow1lem4  19565  sylow1lem5  19566  odcau  19568  pgpfi  19569  pgpssslw  19578  sylow3lem4  19594  sylow3lem6  19596  efgsfo  19703  frgp0  19724  odadd1  19812  odadd2  19813  odadd  19814  gexexlem  19816  lt6abl  19859  gsumzsubmcl  19882  pwsgsum  19946  dprd2dlem1  20007  dprd2d2  20010  ablfacrplem  20031  ablfacrp  20032  ablfacrp2  20033  ablfac1b  20036  ablfac1eu  20039  pgpfac1lem3a  20042  ablfaclem2  20052  dvdsrid  20336  dvdsrtr  20337  dvdsrneg  20339  unitmulcl  20349  unitgrp  20352  unitnegcl  20366  subrguss  20553  subrgunit  20556  isdrng2  20709  fidomndrnglem  20738  abvsubtri  20793  orngsqr  20832  ornglmulle  20833  orngrmulle  20834  orng0le1  20840  gzrngunit  21402  prmirredlem  21441  znidomb  21530  frlmgsum  21741  psrbaglesupp  21891  psdmul  22121  psdmvr  22124  invrvald  22629  psmetsym  24263  psmettri  24264  mettri2  24294  xmetsym  24300  xmettri  24304  prdsxmetlem  24321  xblss2ps  24354  xblss2  24355  blhalf  24358  xmsge0  24416  ngptgp  24589  nrginvrcnlem  24644  nmoeq0  24689  cnmet  24724  blcvx  24751  opnreen  24785  metdcnlem  24790  metdstri  24805  metdsle  24806  metnrmlem1  24813  metnrmlem3  24815  lebnumlem1  24916  pi1inv  25007  cphnmf  25150  ipge0  25153  ipcau2  25189  tcphcphlem1  25190  csbren  25354  minveclem2  25381  minveclem3  25384  ovolssnul  25442  ovolctb  25445  ovolunnul  25455  ovoliunlem1  25457  ovoliun2  25461  ovoliunnul  25462  ioombl1lem4  25516  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  uniioombl  25544  volcn  25561  vitalilem2  25564  vitalilem5  25567  itg1lea  25667  mbfi1fseqlem6  25675  mbfi1flimlem  25677  itg2eqa  25700  itg2splitlem  25703  itg2split  25704  itg2monolem1  25705  itg2cnlem2  25717  iblabsr  25785  iblmulc2  25786  bddiblnc  25797  dveflem  25934  dvef  25935  dvferm2lem  25941  dvlip  25948  c1liplem1  25951  dveq0  25955  dvlt0  25960  dvivthlem1  25963  lhop1  25969  dvfsumle  25976  dvfsumlem4  25984  dvfsumrlim3  25988  dvfsum2  25989  ftc1a  25992  ftc1lem4  25994  deg1add  26056  ply1divex  26090  ply1rem  26119  fta1glem2  26122  fta1blem  26124  ig1pdvds  26133  plyeq0lem  26163  dgrcolem2  26227  plydivlem4  26250  plyrem  26259  fta1lem  26261  aalioulem3  26288  aaliou2b  26295  aaliou3lem3  26298  aaliou3lem8  26299  ulmcn  26352  ulmdvlem1  26353  itgulm  26361  pserulm  26375  pserdvlem2  26381  abelthlem2  26385  abelthlem5  26388  abelthlem6  26389  abelthlem7  26391  abelthlem8  26392  abelthlem9  26393  sinq12gt0  26459  sinq34lt0t  26461  cosq14gt0  26462  cosq14ge0  26463  cos02pilt1  26478  efif1olem3  26496  argimgt0  26564  argimlt0  26565  logneg2  26567  logcnlem3  26596  logcnlem4  26597  logtayllem  26611  logtayl2  26614  cxpsqrtlem  26654  cxpsqrt  26655  cxpaddlelem  26703  abscxpbnd  26705  zrtdvds  26711  rtprmirr  26712  loglesqrt  26713  ang180lem2  26762  atanlogaddlem  26865  atanlogsublem  26867  atantan  26875  atans2  26883  atantayl  26889  leibpi  26894  log2tlbnd  26897  birthdaylem2  26904  birthdaylem3  26905  cxp2limlem  26927  jensenlem2  26939  jensen  26940  logdiflbnd  26946  emcllem2  26948  emcllem4  26950  harmonicbnd4  26962  fsumharmonic  26963  lgamgulmlem2  26981  lgamgulm2  26987  lgambdd  26988  lgamucov  26989  lgamcvglem  26991  lgamcvg2  27006  gamcvg  27007  wilthlem3  27021  basellem1  27032  basellem3  27034  basellem4  27035  fsumdvdsdiaglem  27134  dvdsppwf1o  27137  mpodvdsmulf1o  27145  dvdsmulf1o  27147  chteq0  27160  chtub  27163  chpub  27171  logfacubnd  27172  logfaclbnd  27173  logexprlim  27176  perfectlem2  27181  dchrfi  27206  bclbnd  27231  bposlem1  27235  bposlem3  27237  bposlem4  27238  bposlem6  27240  lgslem1  27248  lgsqrlem2  27298  lgsqrlem4  27300  lgseisenlem2  27327  lgsquadlem1  27331  lgsquadlem2  27332  lgsquad2lem1  27335  2sqlem3  27371  2sqlem4  27372  2sqlem8  27377  2sqlem11  27380  2sqcoprm  27386  2sqmod  27387  chebbnd1lem2  27421  chebbnd1lem3  27422  chtppilimlem1  27424  chpchtlim  27430  vmadivsum  27433  vmadivsumb  27434  rpvmasumlem  27438  dchrisumlem2  27441  dchrmusum2  27445  dchrvmasumlem2  27449  dchrvmasumlem3  27450  dchrisum0flblem2  27460  dchrisum0fno1  27462  dchrisum0re  27464  dchrisum0lem1  27467  dchrisum0lem2a  27468  mudivsum  27481  mulogsumlem  27482  mulog2sumlem2  27486  vmalogdivsum2  27489  selberglem2  27497  selbergb  27500  selberg2b  27503  logdivbnd  27507  selberg3lem1  27508  selberg3lem2  27509  selberg4lem1  27511  pntrmax  27515  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem5  27532  pntrlog2bndlem6a  27533  pntrlog2bndlem6  27534  pntrlog2bnd  27535  pntpbnd1a  27536  pntpbnd1  27537  pntpbnd2  27538  pntibndlem1  27540  pntibndlem2  27542  pntlemb  27548  pntlemq  27552  pntlemr  27553  pntlemj  27554  pntlemk  27557  qabvle  27576  padicabvcxp  27583  ostth2lem2  27585  ostth2lem3  27586  ostth2lem4  27587  ostth3  27589  addsuniflem  27981  negsid  28021  negsunif  28035  negright  28039  mulsuniflem  28129  ltmuls2  28151  precsexlem9  28195  absmuls  28224  zcuts  28387  addhalfcut  28439  pw2cut2  28442  bdayfinbndlem1  28447  z12sge0  28463  legtrid  28647  legov3  28654  krippenlem  28746  mideulem2  28790  midex  28793  opphllem5  28807  opphllem6  28808  opphl  28810  lmieu  28840  lmiisolem  28852  ttgcontlem1  28941  colinearalglem4  28966  axpaschlem  28997  axcontlem7  29027  nbfusgrlevtxm2  29435  clwlksndivn  30144  eucrct2eupth  30303  nvge0  30732  smcnlem  30756  nmoub3i  30832  nmoub2i  30833  nmlno0lem  30852  minvecolem2  30934  htthlem  30976  norm3dif2  31210  bcs2  31241  chscllem2  31697  eigposi  31895  nmopub2tALT  31968  nmfnleub2  31985  nmlnop0iALT  32054  riesz1  32124  cnlnadjlem2  32127  nmopcoadji  32160  leopsq  32188  leopmul  32193  leopnmid  32197  nmopleid  32198  opsqrlem6  32204  0leopj  32245  hstle1  32285  strlem3a  32311  mdslmd4i  32392  cvexchlem  32427  cdj1i  32492  unidifsnel  32593  unidifsnne  32594  le2halvesd  32817  xlt2addrd  32820  fsumub  32889  sgnmulsgp  32904  2exple2exp  32906  oexpled  32908  wrdt2ind  33001  xrge0tsmsd  33122  fzto1st1  33151  cycpmco2lem4  33178  cycpmco2lem6  33180  cyc3conja  33206  archiabllem1a  33240  archiabllem2a  33243  archiabllem2c  33244  rprmdvdsprod  33582  1arithidomlem1  33583  1arithidomlem2  33584  1arithidom  33585  ply1dg3rt0irred  33632  mplmulmvr  33671  mplvrpmrhm  33679  exsslsb  33729  fedgmullem1  33761  fedgmullem2  33762  fldsdrgfldext2  33794  fldextrspundgdvdslem  33812  fldextrspundgdvds  33813  fldext2rspun  33814  extdgfialglem2  33825  algextdeglem8  33856  rtelextdg2lem  33858  constrext2chnlem  33882  cos9thpiminplylem1  33914  cos9thpiminplylem2  33915  metideq  34025  metider  34026  sqsscirc1  34040  esummono  34186  esumpad2  34188  esumle  34190  esumlef  34194  esumcst  34195  esumrnmpt2  34200  esum2d  34225  aean  34376  dya2ub  34402  dya2icoseg  34409  omssubadd  34432  inelcarsg  34443  carsgsigalem  34447  carsggect  34450  carsgclctunlem2  34451  eulerpartlemb  34500  fibp1  34533  signsplypnf  34682  signsply0  34683  fdvposlt  34731  fdvposle  34733  reprgt  34753  logdivsqrle  34782  hgt750lemb  34788  hgt750leme  34790  tgoldbachgtde  34792  subfacval3  35359  sconnpht2  35408  sconnpi1  35409  resconn  35416  snmlff  35499  sinccvglem  35842  faclimlem2  35914  btwnouttr2  36192  weiunpo  36635  dnibndlem5  36730  dnibndlem7  36732  dnibndlem8  36733  dnibndlem9  36734  dnibndlem10  36735  dnibnd  36739  knoppcnlem4  36744  knoppcnlem9  36749  unbdqndv2lem1  36757  unbdqndv2lem2  36758  knoppndvlem11  36770  knoppndvlem12  36771  knoppndvlem14  36773  knoppndvlem15  36774  knoppndvlem17  36776  knoppndvlem18  36777  knoppndvlem19  36778  knoppndvlem21  36780  ltflcei  37917  poimirlem9  37938  poimirlem26  37955  poimirlem27  37956  poimirlem29  37958  heicant  37964  mblfinlem2  37967  mblfinlem3  37968  mblfinlem4  37969  volsupnfl  37974  itg2addnclem  37980  itg2addnclem3  37982  iblmulc2nc  37994  ftc1cnnclem  38000  ftc1anclem6  38007  ftc1anclem7  38008  ftc1anclem8  38009  ftc2nc  38011  dvasin  38013  geomcau  38068  bfplem2  38132  rrncmslem  38141  rrnequiv  38144  lsatcvatlem  39483  islshpcv  39487  atlatmstc  39753  cvlsupr7  39782  cvrval3  39847  cvrval5  39849  cvrexchlem  39853  atcvrj1  39865  cvrat3  39876  cvrat4  39877  atbtwn  39880  1cvratex  39907  hlatexch4  39915  3atlem1  39917  3atlem2  39918  atcvrlln2  39953  atcvrlln  39954  lplnllnneN  39990  llncvrlpln2  39991  4atlem3b  40032  lplncvrlvol2  40049  dalemswapyz  40090  dalemswapyzps  40124  dalem25  40132  dalem39  40145  dalem58  40164  dalem59  40165  lneq2at  40212  lncvrat  40216  dalawlem2  40306  dalawlem3  40307  dalawlem4  40308  dalawlem6  40310  dalawlem9  40313  dalawlem11  40315  dalawlem12  40316  lhpocnle  40450  lhpmcvr3  40459  lhpmcvr5N  40461  lhpmcvr6N  40462  4atexlemunv  40500  4atexlemc  40503  4atexlemex2  40505  lautm  40528  cdlemc2  40626  cdleme5  40674  cdleme11j  40701  cdleme16b  40713  cdlemednpq  40733  cdleme19e  40741  cdleme20i  40751  cdleme22a  40774  cdleme22cN  40776  cdleme22d  40777  cdleme22e  40778  cdleme22eALTN  40779  cdleme22f  40780  cdleme23c  40785  cdleme30a  40812  cdleme35a  40882  cdleme35b  40884  cdleme42h  40916  cdlemeg46rgv  40962  cdlemg8b  41062  cdlemg12e  41081  cdlemg13a  41085  cdlemg17pq  41106  cdlemg18c  41114  cdlemg19  41118  cdlemg21  41120  cdlemg31d  41134  cdlemg33a  41140  tendoid  41207  cdlemk4  41268  cdlemki  41275  cdlemk10  41277  cdlemksv2  41281  cdlemk12  41284  cdlemk14  41288  cdlemk15  41289  cdlemk1u  41293  cdlemk5u  41295  cdlemk12u  41306  cdlemk45  41381  cdlemk48  41384  dia2dimlem1  41498  dia2dimlem2  41499  dia2dimlem3  41500  cdlemm10N  41552  cdlemn2  41629  dihjustlem  41650  dihglbcpreN  41734  dihmeetlem3N  41739  nnproddivdvdsd  42427  lcmineqlem17  42472  lcmineqlem18  42473  3lexlogpow2ineq1  42485  3lexlogpow2ineq2  42486  3lexlogpow5ineq5  42487  aks4d1p1p3  42496  aks4d1p1p2  42497  aks4d1p1p4  42498  aks4d1p1p5  42502  aks4d1p1  42503  aks4d1p3  42505  aks4d1p8  42514  posbezout  42527  primrootspoweq0  42533  aks6d1c1  42543  hashscontpow1  42548  aks6d1c4  42551  aks6d1c2  42557  aks6d1c5lem1  42563  aks6d1c5lem3  42564  aks6d1c5lem2  42565  deg1gprod  42567  sticksstones7  42579  sticksstones10  42582  sticksstones12  42585  sticksstones22  42595  aks6d1c6lem1  42597  aks6d1c6lem3  42599  aks6d1c6lem4  42600  bcled  42605  bcle2d  42606  aks6d1c7lem1  42607  unitscyglem4  42625  aks5lem7  42627  aks5  42631  explt1d  42743  mulgt0b2d  42911  evlselv  43008  dffltz  43055  fltdvdsabdvdsc  43059  fltaccoprm  43061  fltabcoprm  43063  flt4lem5elem  43072  flt4lem7  43080  fltnlta  43084  irrapxlem1  43238  pell1qrgaplem  43289  pell1qrgap  43290  monotoddzzfi  43358  jm2.24nn  43375  congtr  43381  congmul  43383  congsub  43386  fzmaxdif  43397  acongeq  43399  jm2.20nn  43413  jm2.25  43415  hbtlem4  43542  dgrsub2  43551  mpaaeu  43566  idomsubgmo  43609  iscard4  43948  sqrtcvallem4  44054  leeq2d  44573  int-sqgeq0d  44601  int-ineqmvtd  44606  cvgdvgrat  44728  radcnvrat  44729  hashnzfzclim  44737  dvconstbi  44749  binomcxplemdvbinom  44768  isosctrlem1ALT  45348  mulltgt0  45441  rnmptbd2lem  45665  oddfl  45699  2timesgt  45709  lt3addmuld  45722  lt4addmuld  45727  supxrgere  45751  supxrgelem  45755  supxrge  45756  xadd0ge2  45759  infrpge  45769  xrlexaddrp  45770  xralrple2  45772  infxr  45784  infleinflem1  45787  infleinflem2  45788  infleinf  45789  xralrple4  45790  xralrple3  45791  recnnltrp  45794  rpgtrecnn  45797  xrralrecnnge  45807  rexabslelem  45834  infrnmptle  45839  supminfxr  45880  xrpnf  45901  iccshift  45936  iooshift  45940  ressiocsup  45972  ressioosup  45973  fsumnncl  45990  fmul01  45998  fmul01lt1lem1  46002  fmul01lt1lem2  46003  mccllem  46015  climrec  46021  climexp  46023  climneg  46028  limcrecl  46047  sumnnodd  46048  lptioo2  46049  lptioo1  46050  ltmod  46054  lptre2pt  46056  0ellimcdiv  46065  limclner  46067  fnlimcnv  46083  climinf2lem  46122  limsupubuzlem  46128  limsup10exlem  46188  limsupgtlem  46193  dfxlim2v  46263  xlimliminflimsup  46278  cncficcgt0  46304  cncfioobdlem  46312  ioodvbdlimc1lem1  46347  ioodvbdlimc1lem2  46348  ioodvbdlimc2lem  46350  dvdsn1add  46355  dvnxpaek  46358  dvnmul  46359  dvnprodlem1  46362  itgiccshift  46396  itgperiod  46397  sublevolico  46400  ismbl3  46402  ovolsplit  46404  ismbl4  46409  stoweidlem1  46417  stoweidlem11  46427  stoweidlem13  46429  stoweidlem26  46442  stoweidlem34  46450  stoweidlem38  46454  stoweidlem42  46458  stoweidlem51  46467  stoweidlem59  46475  stirlinglem5  46494  stirlinglem6  46495  stirlinglem7  46496  stirlinglem10  46499  stirlinglem11  46500  stirlinglem13  46502  stirlinglem15  46504  dirkercncflem1  46519  dirkercncflem4  46522  fourierdlem4  46527  fourierdlem10  46533  fourierdlem11  46534  fourierdlem15  46538  fourierdlem20  46543  fourierdlem25  46548  fourierdlem26  46549  fourierdlem30  46553  fourierdlem37  46560  fourierdlem39  46562  fourierdlem40  46563  fourierdlem41  46564  fourierdlem42  46565  fourierdlem44  46567  fourierdlem47  46569  fourierdlem48  46570  fourierdlem49  46571  fourierdlem50  46572  fourierdlem51  46573  fourierdlem52  46574  fourierdlem54  46576  fourierdlem60  46582  fourierdlem61  46583  fourierdlem63  46585  fourierdlem64  46586  fourierdlem65  46587  fourierdlem73  46595  fourierdlem74  46596  fourierdlem75  46597  fourierdlem76  46598  fourierdlem78  46600  fourierdlem79  46601  fourierdlem81  46603  fourierdlem84  46606  fourierdlem87  46609  fourierdlem92  46614  fourierdlem93  46615  fourierdlem101  46623  fourierdlem102  46624  fourierdlem103  46625  fourierdlem104  46626  fourierdlem111  46633  fourierdlem114  46636  sqwvfoura  46644  sqwvfourb  46645  fouriersw  46647  etransclem19  46669  etransclem23  46673  etransclem24  46674  etransclem25  46675  etransclem27  46677  etransclem32  46682  etransclem35  46685  etransclem48  46698  qndenserrnbllem  46710  ioorrnopnlem  46720  ioorrnopnxrlem  46722  fsumlesge0  46793  sge0cl  46797  sge0supre  46805  sge0less  46808  sge0gerp  46811  sge0ltfirp  46816  sge0le  46823  sge0ltfirpmpt  46824  sge0split  46825  sge0rpcpnf  46837  sge0ltfirpmpt2  46842  sge0isum  46843  sge0xaddlem1  46849  sge0pnffigtmpt  46856  sge0pnffsumgt  46858  sge0gtfsumgt  46859  sge0seq  46862  nnfoctbdjlem  46871  meassle  46879  meaiuninclem  46896  meaiininclem  46902  omeiunle  46933  omeiunltfirp  46935  carageniuncllem2  46938  carageniuncl  46939  omess0  46950  hoicvr  46964  ovnlerp  46978  ovnsubaddlem1  46986  hsphoidmvle2  47001  hoidmv1lelem2  47008  hoidmv1le  47010  hoidmvlelem1  47011  hoidmvlelem2  47012  hoidmvlelem3  47013  hoidmvlelem5  47015  ovnhoilem2  47018  ovnhoi  47019  hoidifhspdmvle  47036  hoiqssbllem2  47039  hspmbllem2  47043  hspmbllem3  47044  hspmbl  47045  vonioolem2  47097  vonicclem2  47100  smfaddlem1  47179  smflimlem2  47188  smflimlem4  47190  smfmullem1  47207  smfinflem  47233  smflimsuplem4  47239  smflimsuplem8  47243  chnsubseq  47298  perfectALTVlem2  48186  nnpw2blen  49044  itscnhlinecirc02plem1  49246  funcoppc3  49610  oppcuprcl2  49665  isinito3  49963