Theorem breqtrd 5118

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breqtrrd  5120  breqtrid  5129  domunsn  9044  mapdom2  9065  phplem2  9119  mapfien2  9299  wemaplem2  9439  infdifsn  9553  cantnff  9570  ttrclss  9616  rnttrcl  9618  infxpenlem  9907  infmap2  10111  ssfin4  10204  canthp1lem1  10546  nqereq  10829  ltexnq  10869  ltbtwnnq  10872  add20  11632  mullt0  11639  ltm1  11966  recgt0  11970  prodgt0  11971  ltmul1a  11973  mulge0b  11995  recp1lt1  12023  recreclt  12024  ledivp1  12027  ledivp1i  12050  ltdivp1i  12051  eluzmn  12742  ltaddrp2d  12971  mul2lt0bi  13001  prodge0rd  13002  xleadd1a  13155  xov1plusxeqvd  13401  fz01en  13455  fzonmapblen  13611  fladdz  13729  flhalf  13734  fldiv  13764  modsubdir  13847  fzen2  13876  serle  13964  ltexp2a  14073  leexp2a  14079  exple1  14084  expubnd  14085  bernneq  14136  expmulnbnd  14142  discr1  14146  discr  14147  faclbnd6  14206  hashfz  14334  hashfun  14344  seqcoll  14371  sqeqd  15073  01sqrexlem7  15155  sqrtge0  15164  sqrtneglem  15173  abslt  15222  absle  15223  abstri  15238  rlimge0  15488  reccn2  15504  climaddc2  15543  isercolllem1  15572  caucvgrlem  15580  summolem2a  15622  isumge0  15673  fsumle  15706  fsumlt  15707  o1fsum  15720  supcvg  15763  expcnv  15771  geolim  15777  geolim2  15778  georeclim  15779  geo2lim  15782  mertenslem1  15791  mertens  15793  prodmolem2a  15841  efcllem  15984  ef0lem  15985  efgt0  16012  eftlub  16018  eflt  16026  sinbnd  16089  cosbnd  16090  ef01bndlem  16093  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  eirrlem  16113  rpnnen2lem11  16133  rpnnen2lem12  16134  ruclem11  16149  dvdssub2  16212  dvdsadd2b  16217  dvdsexp  16239  3dvds  16242  opoe  16274  bitsfzolem  16345  bitsinv1lem  16352  bezoutlem4  16453  dvdsgcd  16455  dvdsmulgcd  16467  bezoutr1  16480  nn0seqcvgd  16481  rpmulgcd2  16567  qredeq  16568  rpdvds  16571  prmind2  16596  divdenle  16660  hashdvds  16686  phimullem  16690  eulerthlem2  16693  prmdiveq  16697  prmdivdiv  16698  pythagtriplem4  16731  pythagtriplem10  16732  pythagtriplem19  16745  iserodd  16747  pcpre1  16754  pcadd2  16802  qexpz  16813  expnprm  16814  oddprmdvds  16815  pockthlem  16817  prmreclem2  16829  prmreclem3  16830  4sqlem7  16856  4sqlem10  16859  4sqlem11  16867  4sqlem12  16868  4sqlem14  16870  4sqlem15  16871  4sqlem16  16872  0ram  16932  ffthiso  17838  latmlej12  18385  qusgrp  19065  pgpfi1  19474  sylow1lem4  19480  sylow1lem5  19481  odcau  19483  pgpfi  19484  pgpssslw  19493  sylow3lem4  19509  sylow3lem6  19511  efgsfo  19618  frgp0  19639  odadd1  19727  odadd2  19728  odadd  19729  gexexlem  19731  lt6abl  19774  gsumzsubmcl  19797  pwsgsum  19861  dprd2dlem1  19922  dprd2d2  19925  ablfacrplem  19946  ablfacrp  19947  ablfacrp2  19948  ablfac1b  19951  ablfac1eu  19954  pgpfac1lem3a  19957  ablfaclem2  19967  dvdsrid  20252  dvdsrtr  20253  dvdsrneg  20255  unitmulcl  20265  unitgrp  20268  unitnegcl  20282  subrguss  20472  subrgunit  20475  isdrng2  20628  fidomndrnglem  20657  abvsubtri  20712  orngsqr  20751  ornglmulle  20752  orngrmulle  20753  orng0le1  20759  gzrngunit  21340  prmirredlem  21379  znidomb  21468  frlmgsum  21679  psrbaglesupp  21829  psdmul  22051  psdmvr  22054  invrvald  22561  psmetsym  24196  psmettri  24197  mettri2  24227  xmetsym  24233  xmettri  24237  prdsxmetlem  24254  xblss2ps  24287  xblss2  24288  blhalf  24291  xmsge0  24349  ngptgp  24522  nrginvrcnlem  24577  nmoeq0  24622  cnmet  24657  blcvx  24684  opnreen  24718  metdcnlem  24723  metdstri  24738  metdsle  24739  metnrmlem1  24746  metnrmlem3  24748  lebnumlem1  24858  pi1inv  24950  cphnmf  25093  ipge0  25096  ipcau2  25132  tcphcphlem1  25133  csbren  25297  minveclem2  25324  minveclem3  25327  ovolssnul  25386  ovolctb  25389  ovolunnul  25399  ovoliunlem1  25401  ovoliun2  25405  ovoliunnul  25406  ioombl1lem4  25460  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  uniioombl  25488  volcn  25505  vitalilem2  25508  vitalilem5  25511  itg1lea  25611  mbfi1fseqlem6  25619  mbfi1flimlem  25621  itg2eqa  25644  itg2splitlem  25647  itg2split  25648  itg2monolem1  25649  itg2cnlem2  25661  iblabsr  25729  iblmulc2  25730  bddiblnc  25741  dveflem  25881  dvef  25882  dvferm2lem  25888  dvlip  25896  c1liplem1  25899  dveq0  25903  dvlt0  25908  dvivthlem1  25911  lhop1  25917  dvfsumle  25924  dvfsumleOLD  25925  dvfsumlem4  25934  dvfsumrlim3  25938  dvfsum2  25939  ftc1a  25942  ftc1lem4  25944  deg1add  26006  ply1divex  26040  ply1rem  26069  fta1glem2  26072  fta1blem  26074  ig1pdvds  26083  plyeq0lem  26113  dgrcolem2  26178  plydivlem4  26202  plyrem  26211  fta1lem  26213  aalioulem3  26240  aaliou2b  26247  aaliou3lem3  26250  aaliou3lem8  26251  ulmcn  26306  ulmdvlem1  26307  itgulm  26315  pserulm  26329  pserdvlem2  26336  abelthlem2  26340  abelthlem5  26343  abelthlem6  26344  abelthlem7  26346  abelthlem8  26347  abelthlem9  26348  sinq12gt0  26414  sinq34lt0t  26416  cosq14gt0  26417  cosq14ge0  26418  cos02pilt1  26433  efif1olem3  26451  argimgt0  26519  argimlt0  26520  logneg2  26522  logcnlem3  26551  logcnlem4  26552  logtayllem  26566  logtayl2  26569  cxpsqrtlem  26609  cxpsqrt  26610  cxpaddlelem  26659  abscxpbnd  26661  zrtdvds  26667  rtprmirr  26668  loglesqrt  26669  ang180lem2  26718  atanlogaddlem  26821  atanlogsublem  26823  atantan  26831  atans2  26839  atantayl  26845  leibpi  26850  log2tlbnd  26853  birthdaylem2  26860  birthdaylem3  26861  cxp2limlem  26884  jensenlem2  26896  jensen  26897  logdiflbnd  26903  emcllem2  26905  emcllem4  26907  harmonicbnd4  26919  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulm2  26944  lgambdd  26945  lgamucov  26946  lgamcvglem  26948  lgamcvg2  26963  gamcvg  26964  wilthlem3  26978  basellem1  26989  basellem3  26991  basellem4  26992  fsumdvdsdiaglem  27091  dvdsppwf1o  27094  mpodvdsmulf1o  27102  dvdsmulf1o  27104  chteq0  27118  chtub  27121  chpub  27129  logfacubnd  27130  logfaclbnd  27131  logexprlim  27134  perfectlem2  27139  dchrfi  27164  bclbnd  27189  bposlem1  27193  bposlem3  27195  bposlem4  27196  bposlem6  27198  lgslem1  27206  lgsqrlem2  27256  lgsqrlem4  27258  lgseisenlem2  27285  lgsquadlem1  27289  lgsquadlem2  27290  lgsquad2lem1  27293  2sqlem3  27329  2sqlem4  27330  2sqlem8  27335  2sqlem11  27338  2sqcoprm  27344  2sqmod  27345  chebbnd1lem2  27379  chebbnd1lem3  27380  chtppilimlem1  27382  chpchtlim  27388  vmadivsum  27391  vmadivsumb  27392  rpvmasumlem  27396  dchrisumlem2  27399  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlem3  27408  dchrisum0flblem2  27418  dchrisum0fno1  27420  dchrisum0re  27422  dchrisum0lem1  27425  dchrisum0lem2a  27426  mudivsum  27439  mulogsumlem  27440  mulog2sumlem2  27444  vmalogdivsum2  27447  selberglem2  27455  selbergb  27458  selberg2b  27461  logdivbnd  27465  selberg3lem1  27466  selberg3lem2  27467  selberg4lem1  27469  pntrmax  27473  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem5  27490  pntrlog2bndlem6a  27491  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem1  27498  pntibndlem2  27500  pntlemb  27506  pntlemq  27510  pntlemr  27511  pntlemj  27512  pntlemk  27515  qabvle  27534  padicabvcxp  27541  ostth2lem2  27543  ostth2lem3  27544  ostth2lem4  27545  ostth3  27547  addsuniflem  27915  negsid  27954  negsunif  27968  mulsuniflem  28059  sltmul2  28081  precsexlem9  28124  absmuls  28153  zscut  28302  addhalfcut  28350  pw2cut2  28353  zs12ge0  28364  legtrid  28540  legov3  28547  krippenlem  28639  mideulem2  28683  midex  28686  opphllem5  28700  opphllem6  28701  opphl  28703  lmieu  28733  lmiisolem  28745  ttgcontlem1  28834  colinearalglem4  28858  axpaschlem  28889  axcontlem7  28919  nbfusgrlevtxm2  29327  clwlksndivn  30034  eucrct2eupth  30193  nvge0  30621  smcnlem  30645  nmoub3i  30721  nmoub2i  30722  nmlno0lem  30741  minvecolem2  30823  htthlem  30865  norm3dif2  31099  bcs2  31130  chscllem2  31586  eigposi  31784  nmopub2tALT  31857  nmfnleub2  31874  nmlnop0iALT  31943  riesz1  32013  cnlnadjlem2  32016  nmopcoadji  32049  leopsq  32077  leopmul  32082  leopnmid  32086  nmopleid  32087  opsqrlem6  32093  0leopj  32134  hstle1  32174  strlem3a  32200  mdslmd4i  32281  cvexchlem  32316  cdj1i  32381  unidifsnel  32484  unidifsnne  32485  le2halvesd  32708  xlt2addrd  32711  fsumub  32782  sgnmulsgp  32797  2exple2exp  32799  oexpled  32801  wrdt2ind  32904  xrge0tsmsd  33024  fzto1st1  33053  cycpmco2lem4  33080  cycpmco2lem6  33082  cyc3conja  33108  archiabllem1a  33142  archiabllem2a  33145  archiabllem2c  33146  rprmdvdsprod  33480  1arithidomlem1  33481  1arithidomlem2  33482  1arithidom  33483  ply1dg3rt0irred  33527  mplvrpmrhm  33558  exsslsb  33579  fedgmullem1  33612  fedgmullem2  33613  fldsdrgfldext2  33645  fldextrspundgdvdslem  33663  fldextrspundgdvds  33664  fldext2rspun  33665  extdgfialglem2  33676  algextdeglem8  33707  rtelextdg2lem  33709  constrext2chnlem  33733  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  metideq  33876  metider  33877  sqsscirc1  33891  esummono  34037  esumpad2  34039  esumle  34041  esumlef  34045  esumcst  34046  esumrnmpt2  34051  esum2d  34076  aean  34227  dya2ub  34254  dya2icoseg  34261  omssubadd  34284  inelcarsg  34295  carsgsigalem  34299  carsggect  34302  carsgclctunlem2  34303  eulerpartlemb  34352  fibp1  34385  signsplypnf  34534  signsply0  34535  fdvposlt  34583  fdvposle  34585  reprgt  34605  logdivsqrle  34634  hgt750lemb  34640  hgt750leme  34642  tgoldbachgtde  34644  subfacval3  35182  sconnpht2  35231  sconnpi1  35232  resconn  35239  snmlff  35322  sinccvglem  35665  faclimlem2  35737  btwnouttr2  36016  weiunpo  36459  dnibndlem5  36476  dnibndlem7  36478  dnibndlem8  36479  dnibndlem9  36480  dnibndlem10  36481  dnibnd  36485  knoppcnlem4  36490  knoppcnlem9  36495  unbdqndv2lem1  36503  unbdqndv2lem2  36504  knoppndvlem11  36516  knoppndvlem12  36517  knoppndvlem14  36519  knoppndvlem15  36520  knoppndvlem17  36522  knoppndvlem18  36523  knoppndvlem19  36524  knoppndvlem21  36526  ltflcei  37608  poimirlem9  37629  poimirlem26  37646  poimirlem27  37647  poimirlem29  37649  heicant  37655  mblfinlem2  37658  mblfinlem3  37659  mblfinlem4  37660  volsupnfl  37665  itg2addnclem  37671  itg2addnclem3  37673  iblmulc2nc  37685  ftc1cnnclem  37691  ftc1anclem6  37698  ftc1anclem7  37699  ftc1anclem8  37700  ftc2nc  37702  dvasin  37704  geomcau  37759  bfplem2  37823  rrncmslem  37832  rrnequiv  37835  lsatcvatlem  39048  islshpcv  39052  atlatmstc  39318  cvlsupr7  39347  cvrval3  39412  cvrval5  39414  cvrexchlem  39418  atcvrj1  39430  cvrat3  39441  cvrat4  39442  atbtwn  39445  1cvratex  39472  hlatexch4  39480  3atlem1  39482  3atlem2  39483  atcvrlln2  39518  atcvrlln  39519  lplnllnneN  39555  llncvrlpln2  39556  4atlem3b  39597  lplncvrlvol2  39614  dalemswapyz  39655  dalemswapyzps  39689  dalem25  39697  dalem39  39710  dalem58  39729  dalem59  39730  lneq2at  39777  lncvrat  39781  dalawlem2  39871  dalawlem3  39872  dalawlem4  39873  dalawlem6  39875  dalawlem9  39878  dalawlem11  39880  dalawlem12  39881  lhpocnle  40015  lhpmcvr3  40024  lhpmcvr5N  40026  lhpmcvr6N  40027  4atexlemunv  40065  4atexlemc  40068  4atexlemex2  40070  lautm  40093  cdlemc2  40191  cdleme5  40239  cdleme11j  40266  cdleme16b  40278  cdlemednpq  40298  cdleme19e  40306  cdleme20i  40316  cdleme22a  40339  cdleme22cN  40341  cdleme22d  40342  cdleme22e  40343  cdleme22eALTN  40344  cdleme22f  40345  cdleme23c  40350  cdleme30a  40377  cdleme35a  40447  cdleme35b  40449  cdleme42h  40481  cdlemeg46rgv  40527  cdlemg8b  40627  cdlemg12e  40646  cdlemg13a  40650  cdlemg17pq  40671  cdlemg18c  40679  cdlemg19  40683  cdlemg21  40685  cdlemg31d  40699  cdlemg33a  40705  tendoid  40772  cdlemk4  40833  cdlemki  40840  cdlemk10  40842  cdlemksv2  40846  cdlemk12  40849  cdlemk14  40853  cdlemk15  40854  cdlemk1u  40858  cdlemk5u  40860  cdlemk12u  40871  cdlemk45  40946  cdlemk48  40949  dia2dimlem1  41063  dia2dimlem2  41064  dia2dimlem3  41065  cdlemm10N  41117  cdlemn2  41194  dihjustlem  41215  dihglbcpreN  41299  dihmeetlem3N  41304  nnproddivdvdsd  41993  lcmineqlem17  42038  lcmineqlem18  42039  3lexlogpow2ineq1  42051  3lexlogpow2ineq2  42052  3lexlogpow5ineq5  42053  aks4d1p1p3  42062  aks4d1p1p2  42063  aks4d1p1p4  42064  aks4d1p1p5  42068  aks4d1p1  42069  aks4d1p3  42071  aks4d1p8  42080  posbezout  42093  primrootspoweq0  42099  aks6d1c1  42109  hashscontpow1  42114  aks6d1c4  42117  aks6d1c2  42123  aks6d1c5lem1  42129  aks6d1c5lem3  42130  aks6d1c5lem2  42131  deg1gprod  42133  sticksstones7  42145  sticksstones10  42148  sticksstones12  42151  sticksstones22  42161  aks6d1c6lem1  42163  aks6d1c6lem3  42165  aks6d1c6lem4  42166  bcled  42171  bcle2d  42172  aks6d1c7lem1  42173  unitscyglem4  42191  aks5lem7  42193  aks5  42197  explt1d  42316  mulgt0b2d  42471  evlselv  42580  dffltz  42627  fltdvdsabdvdsc  42631  fltaccoprm  42633  fltabcoprm  42635  flt4lem5elem  42644  flt4lem7  42652  fltnlta  42656  irrapxlem1  42815  pell1qrgaplem  42866  pell1qrgap  42867  monotoddzzfi  42935  jm2.24nn  42952  congtr  42958  congmul  42960  congsub  42963  fzmaxdif  42974  acongeq  42976  jm2.20nn  42990  jm2.25  42992  hbtlem4  43119  dgrsub2  43128  mpaaeu  43143  idomsubgmo  43186  iscard4  43526  sqrtcvallem4  43632  leeq2d  44151  int-sqgeq0d  44179  int-ineqmvtd  44184  cvgdvgrat  44306  radcnvrat  44307  hashnzfzclim  44315  dvconstbi  44327  binomcxplemdvbinom  44346  isosctrlem1ALT  44927  mulltgt0  45020  rnmptbd2lem  45246  oddfl  45280  2timesgt  45290  lt3addmuld  45303  lt4addmuld  45308  supxrgere  45333  supxrgelem  45337  supxrge  45338  xadd0ge2  45341  infrpge  45351  xrlexaddrp  45352  xralrple2  45354  infxr  45366  infleinflem1  45369  infleinflem2  45370  infleinf  45371  xralrple4  45372  xralrple3  45373  recnnltrp  45376  rpgtrecnn  45379  xrralrecnnge  45389  rexabslelem  45417  infrnmptle  45422  supminfxr  45463  xrpnf  45484  iccshift  45519  iooshift  45523  ressiocsup  45555  ressioosup  45556  fsumnncl  45573  fmul01  45581  fmul01lt1lem1  45585  fmul01lt1lem2  45586  mccllem  45598  climrec  45604  climexp  45606  climneg  45611  limcrecl  45630  sumnnodd  45631  lptioo2  45632  lptioo1  45633  ltmod  45639  lptre2pt  45641  0ellimcdiv  45650  limclner  45652  fnlimcnv  45668  climinf2lem  45707  limsupubuzlem  45713  limsup10exlem  45773  limsupgtlem  45778  dfxlim2v  45848  xlimliminflimsup  45863  cncficcgt0  45889  cncfioobdlem  45897  ioodvbdlimc1lem1  45932  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvdsn1add  45940  dvnxpaek  45943  dvnmul  45944  dvnprodlem1  45947  itgiccshift  45981  itgperiod  45982  sublevolico  45985  ismbl3  45987  ovolsplit  45989  ismbl4  45994  stoweidlem1  46002  stoweidlem11  46012  stoweidlem13  46014  stoweidlem26  46027  stoweidlem34  46035  stoweidlem38  46039  stoweidlem42  46043  stoweidlem51  46052  stoweidlem59  46060  stirlinglem5  46079  stirlinglem6  46080  stirlinglem7  46081  stirlinglem10  46084  stirlinglem11  46085  stirlinglem13  46087  stirlinglem15  46089  dirkercncflem1  46104  dirkercncflem4  46107  fourierdlem4  46112  fourierdlem10  46118  fourierdlem11  46119  fourierdlem15  46123  fourierdlem20  46128  fourierdlem25  46133  fourierdlem26  46134  fourierdlem30  46138  fourierdlem37  46145  fourierdlem39  46147  fourierdlem40  46148  fourierdlem41  46149  fourierdlem42  46150  fourierdlem44  46152  fourierdlem47  46154  fourierdlem48  46155  fourierdlem49  46156  fourierdlem50  46157  fourierdlem51  46158  fourierdlem52  46159  fourierdlem54  46161  fourierdlem60  46167  fourierdlem61  46168  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem73  46180  fourierdlem74  46181  fourierdlem75  46182  fourierdlem76  46183  fourierdlem78  46185  fourierdlem79  46186  fourierdlem81  46188  fourierdlem84  46191  fourierdlem87  46194  fourierdlem92  46199  fourierdlem93  46200  fourierdlem101  46208  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fourierdlem114  46221  sqwvfoura  46229  sqwvfourb  46230  fouriersw  46232  etransclem19  46254  etransclem23  46258  etransclem24  46259  etransclem25  46260  etransclem27  46262  etransclem32  46267  etransclem35  46270  etransclem48  46283  qndenserrnbllem  46295  ioorrnopnlem  46305  ioorrnopnxrlem  46307  fsumlesge0  46378  sge0cl  46382  sge0supre  46390  sge0less  46393  sge0gerp  46396  sge0ltfirp  46401  sge0le  46408  sge0ltfirpmpt  46409  sge0split  46410  sge0rpcpnf  46422  sge0ltfirpmpt2  46427  sge0isum  46428  sge0xaddlem1  46434  sge0pnffigtmpt  46441  sge0pnffsumgt  46443  sge0gtfsumgt  46444  sge0seq  46447  nnfoctbdjlem  46456  meassle  46464  meaiuninclem  46481  meaiininclem  46487  omeiunle  46518  omeiunltfirp  46520  carageniuncllem2  46523  carageniuncl  46524  omess0  46535  hoicvr  46549  ovnlerp  46563  ovnsubaddlem1  46571  hsphoidmvle2  46586  hoidmv1lelem2  46593  hoidmv1le  46595  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem5  46600  ovnhoilem2  46603  ovnhoi  46604  hoidifhspdmvle  46621  hoiqssbllem2  46624  hspmbllem2  46628  hspmbllem3  46629  hspmbl  46630  vonioolem2  46682  vonicclem2  46685  smfaddlem1  46764  smflimlem2  46773  smflimlem4  46775  smfmullem1  46792  smfinflem  46818  smflimsuplem4  46824  smflimsuplem8  46828  perfectALTVlem2  47726  nnpw2blen  48585  itscnhlinecirc02plem1  48787  funcoppc3  49152  oppcuprcl2  49207  isinito3  49505