Theorem breqtrd 5123

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

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

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 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  breqtrrd  5125  breqtrid  5134  domunsn  9057  mapdom2  9078  phplem2  9131  mapfien2  9314  wemaplem2  9454  infdifsn  9568  cantnff  9585  ttrclss  9631  rnttrcl  9633  infxpenlem  9925  infmap2  10129  ssfin4  10222  canthp1lem1  10565  nqereq  10848  ltexnq  10888  ltbtwnnq  10891  add20  11651  mullt0  11658  ltm1  11985  recgt0  11989  prodgt0  11990  ltmul1a  11992  mulge0b  12014  recp1lt1  12042  recreclt  12043  ledivp1  12046  ledivp1i  12069  ltdivp1i  12070  eluzmn  12760  ltaddrp2d  12985  mul2lt0bi  13015  prodge0rd  13016  xleadd1a  13170  xov1plusxeqvd  13416  fz01en  13470  fzonmapblen  13626  fladdz  13747  flhalf  13752  fldiv  13782  modsubdir  13865  fzen2  13894  serle  13982  ltexp2a  14091  leexp2a  14097  exple1  14102  expubnd  14103  bernneq  14154  expmulnbnd  14160  discr1  14164  discr  14165  faclbnd6  14224  hashfz  14352  hashfun  14362  seqcoll  14389  sqeqd  15091  01sqrexlem7  15173  sqrtge0  15182  sqrtneglem  15191  abslt  15240  absle  15241  abstri  15256  rlimge0  15506  reccn2  15522  climaddc2  15561  isercolllem1  15590  caucvgrlem  15598  summolem2a  15640  isumge0  15691  fsumle  15724  fsumlt  15725  o1fsum  15738  supcvg  15781  expcnv  15789  geolim  15795  geolim2  15796  georeclim  15797  geo2lim  15800  mertenslem1  15809  mertens  15811  prodmolem2a  15859  efcllem  16002  ef0lem  16003  efgt0  16030  eftlub  16036  eflt  16044  sinbnd  16107  cosbnd  16108  ef01bndlem  16111  sin01gt0  16117  cos01gt0  16118  sin02gt0  16119  eirrlem  16131  rpnnen2lem11  16151  rpnnen2lem12  16152  ruclem11  16167  dvdssub2  16230  dvdsadd2b  16235  dvdsexp  16257  3dvds  16260  opoe  16292  bitsfzolem  16363  bitsinv1lem  16370  bezoutlem4  16471  dvdsgcd  16473  dvdsmulgcd  16485  bezoutr1  16498  nn0seqcvgd  16499  rpmulgcd2  16585  qredeq  16586  rpdvds  16589  prmind2  16614  divdenle  16678  hashdvds  16704  phimullem  16708  eulerthlem2  16711  prmdiveq  16715  prmdivdiv  16716  pythagtriplem4  16749  pythagtriplem10  16750  pythagtriplem19  16763  iserodd  16765  pcpre1  16772  pcadd2  16820  qexpz  16831  expnprm  16832  oddprmdvds  16833  pockthlem  16835  prmreclem2  16847  prmreclem3  16848  4sqlem7  16874  4sqlem10  16877  4sqlem11  16885  4sqlem12  16886  4sqlem14  16888  4sqlem15  16889  4sqlem16  16890  0ram  16950  ffthiso  17857  latmlej12  18404  qusgrp  19117  pgpfi1  19526  sylow1lem4  19532  sylow1lem5  19533  odcau  19535  pgpfi  19536  pgpssslw  19545  sylow3lem4  19561  sylow3lem6  19563  efgsfo  19670  frgp0  19691  odadd1  19779  odadd2  19780  odadd  19781  gexexlem  19783  lt6abl  19826  gsumzsubmcl  19849  pwsgsum  19913  dprd2dlem1  19974  dprd2d2  19977  ablfacrplem  19998  ablfacrp  19999  ablfacrp2  20000  ablfac1b  20003  ablfac1eu  20006  pgpfac1lem3a  20009  ablfaclem2  20019  dvdsrid  20305  dvdsrtr  20306  dvdsrneg  20308  unitmulcl  20318  unitgrp  20321  unitnegcl  20335  subrguss  20522  subrgunit  20525  isdrng2  20678  fidomndrnglem  20707  abvsubtri  20762  orngsqr  20801  ornglmulle  20802  orngrmulle  20803  orng0le1  20809  gzrngunit  21390  prmirredlem  21429  znidomb  21518  frlmgsum  21729  psrbaglesupp  21880  psdmul  22111  psdmvr  22114  invrvald  22622  psmetsym  24256  psmettri  24257  mettri2  24287  xmetsym  24293  xmettri  24297  prdsxmetlem  24314  xblss2ps  24347  xblss2  24348  blhalf  24351  xmsge0  24409  ngptgp  24582  nrginvrcnlem  24637  nmoeq0  24682  cnmet  24717  blcvx  24744  opnreen  24778  metdcnlem  24783  metdstri  24798  metdsle  24799  metnrmlem1  24806  metnrmlem3  24808  lebnumlem1  24918  pi1inv  25010  cphnmf  25153  ipge0  25156  ipcau2  25192  tcphcphlem1  25193  csbren  25357  minveclem2  25384  minveclem3  25387  ovolssnul  25446  ovolctb  25449  ovolunnul  25459  ovoliunlem1  25461  ovoliun2  25465  ovoliunnul  25466  ioombl1lem4  25520  uniioombllem3  25544  uniioombllem4  25545  uniioombllem5  25546  uniioombl  25548  volcn  25565  vitalilem2  25568  vitalilem5  25571  itg1lea  25671  mbfi1fseqlem6  25679  mbfi1flimlem  25681  itg2eqa  25704  itg2splitlem  25707  itg2split  25708  itg2monolem1  25709  itg2cnlem2  25721  iblabsr  25789  iblmulc2  25790  bddiblnc  25801  dveflem  25941  dvef  25942  dvferm2lem  25948  dvlip  25956  c1liplem1  25959  dveq0  25963  dvlt0  25968  dvivthlem1  25971  lhop1  25977  dvfsumle  25984  dvfsumleOLD  25985  dvfsumlem4  25994  dvfsumrlim3  25998  dvfsum2  25999  ftc1a  26002  ftc1lem4  26004  deg1add  26066  ply1divex  26100  ply1rem  26129  fta1glem2  26132  fta1blem  26134  ig1pdvds  26143  plyeq0lem  26173  dgrcolem2  26238  plydivlem4  26262  plyrem  26271  fta1lem  26273  aalioulem3  26300  aaliou2b  26307  aaliou3lem3  26310  aaliou3lem8  26311  ulmcn  26366  ulmdvlem1  26367  itgulm  26375  pserulm  26389  pserdvlem2  26396  abelthlem2  26400  abelthlem5  26403  abelthlem6  26404  abelthlem7  26406  abelthlem8  26407  abelthlem9  26408  sinq12gt0  26474  sinq34lt0t  26476  cosq14gt0  26477  cosq14ge0  26478  cos02pilt1  26493  efif1olem3  26511  argimgt0  26579  argimlt0  26580  logneg2  26582  logcnlem3  26611  logcnlem4  26612  logtayllem  26626  logtayl2  26629  cxpsqrtlem  26669  cxpsqrt  26670  cxpaddlelem  26719  abscxpbnd  26721  zrtdvds  26727  rtprmirr  26728  loglesqrt  26729  ang180lem2  26778  atanlogaddlem  26881  atanlogsublem  26883  atantan  26891  atans2  26899  atantayl  26905  leibpi  26910  log2tlbnd  26913  birthdaylem2  26920  birthdaylem3  26921  cxp2limlem  26944  jensenlem2  26956  jensen  26957  logdiflbnd  26963  emcllem2  26965  emcllem4  26967  harmonicbnd4  26979  fsumharmonic  26980  lgamgulmlem2  26998  lgamgulm2  27004  lgambdd  27005  lgamucov  27006  lgamcvglem  27008  lgamcvg2  27023  gamcvg  27024  wilthlem3  27038  basellem1  27049  basellem3  27051  basellem4  27052  fsumdvdsdiaglem  27151  dvdsppwf1o  27154  mpodvdsmulf1o  27162  dvdsmulf1o  27164  chteq0  27178  chtub  27181  chpub  27189  logfacubnd  27190  logfaclbnd  27191  logexprlim  27194  perfectlem2  27199  dchrfi  27224  bclbnd  27249  bposlem1  27253  bposlem3  27255  bposlem4  27256  bposlem6  27258  lgslem1  27266  lgsqrlem2  27316  lgsqrlem4  27318  lgseisenlem2  27345  lgsquadlem1  27349  lgsquadlem2  27350  lgsquad2lem1  27353  2sqlem3  27389  2sqlem4  27390  2sqlem8  27395  2sqlem11  27398  2sqcoprm  27404  2sqmod  27405  chebbnd1lem2  27439  chebbnd1lem3  27440  chtppilimlem1  27442  chpchtlim  27448  vmadivsum  27451  vmadivsumb  27452  rpvmasumlem  27456  dchrisumlem2  27459  dchrmusum2  27463  dchrvmasumlem2  27467  dchrvmasumlem3  27468  dchrisum0flblem2  27478  dchrisum0fno1  27480  dchrisum0re  27482  dchrisum0lem1  27485  dchrisum0lem2a  27486  mudivsum  27499  mulogsumlem  27500  mulog2sumlem2  27504  vmalogdivsum2  27507  selberglem2  27515  selbergb  27518  selberg2b  27521  logdivbnd  27525  selberg3lem1  27526  selberg3lem2  27527  selberg4lem1  27529  pntrmax  27533  pntrlog2bndlem2  27547  pntrlog2bndlem3  27548  pntrlog2bndlem5  27550  pntrlog2bndlem6a  27551  pntrlog2bndlem6  27552  pntrlog2bnd  27553  pntpbnd1a  27554  pntpbnd1  27555  pntpbnd2  27556  pntibndlem1  27558  pntibndlem2  27560  pntlemb  27566  pntlemq  27570  pntlemr  27571  pntlemj  27572  pntlemk  27575  qabvle  27594  padicabvcxp  27601  ostth2lem2  27603  ostth2lem3  27604  ostth2lem4  27605  ostth3  27607  addsuniflem  27981  negsid  28021  negsunif  28035  negsright  28039  mulsuniflem  28129  sltmul2  28151  precsexlem9  28194  absmuls  28223  zscut  28384  addhalfcut  28436  pw2cut2  28439  bdayfinbndlem1  28444  zs12ge0  28460  legtrid  28644  legov3  28651  krippenlem  28743  mideulem2  28787  midex  28790  opphllem5  28804  opphllem6  28805  opphl  28807  lmieu  28837  lmiisolem  28849  ttgcontlem1  28938  colinearalglem4  28963  axpaschlem  28994  axcontlem7  29024  nbfusgrlevtxm2  29432  clwlksndivn  30142  eucrct2eupth  30301  nvge0  30729  smcnlem  30753  nmoub3i  30829  nmoub2i  30830  nmlno0lem  30849  minvecolem2  30931  htthlem  30973  norm3dif2  31207  bcs2  31238  chscllem2  31694  eigposi  31892  nmopub2tALT  31965  nmfnleub2  31982  nmlnop0iALT  32051  riesz1  32121  cnlnadjlem2  32124  nmopcoadji  32157  leopsq  32185  leopmul  32190  leopnmid  32194  nmopleid  32195  opsqrlem6  32201  0leopj  32242  hstle1  32282  strlem3a  32308  mdslmd4i  32389  cvexchlem  32424  cdj1i  32489  unidifsnel  32590  unidifsnne  32591  le2halvesd  32815  xlt2addrd  32818  fsumub  32888  sgnmulsgp  32903  2exple2exp  32905  oexpled  32907  wrdt2ind  33014  xrge0tsmsd  33134  fzto1st1  33163  cycpmco2lem4  33190  cycpmco2lem6  33192  cyc3conja  33218  archiabllem1a  33252  archiabllem2a  33255  archiabllem2c  33256  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  ply1dg3rt0irred  33644  mplmulmvr  33683  mplvrpmrhm  33691  exsslsb  33732  fedgmullem1  33765  fedgmullem2  33766  fldsdrgfldext2  33798  fldextrspundgdvdslem  33816  fldextrspundgdvds  33817  fldext2rspun  33818  extdgfialglem2  33829  algextdeglem8  33860  rtelextdg2lem  33862  constrext2chnlem  33886  cos9thpiminplylem1  33918  cos9thpiminplylem2  33919  metideq  34029  metider  34030  sqsscirc1  34044  esummono  34190  esumpad2  34192  esumle  34194  esumlef  34198  esumcst  34199  esumrnmpt2  34204  esum2d  34229  aean  34380  dya2ub  34406  dya2icoseg  34413  omssubadd  34436  inelcarsg  34447  carsgsigalem  34451  carsggect  34454  carsgclctunlem2  34455  eulerpartlemb  34504  fibp1  34537  signsplypnf  34686  signsply0  34687  fdvposlt  34735  fdvposle  34737  reprgt  34757  logdivsqrle  34786  hgt750lemb  34792  hgt750leme  34794  tgoldbachgtde  34796  subfacval3  35362  sconnpht2  35411  sconnpi1  35412  resconn  35419  snmlff  35502  sinccvglem  35845  faclimlem2  35917  btwnouttr2  36195  weiunpo  36638  dnibndlem5  36655  dnibndlem7  36657  dnibndlem8  36658  dnibndlem9  36659  dnibndlem10  36660  dnibnd  36664  knoppcnlem4  36669  knoppcnlem9  36674  unbdqndv2lem1  36682  unbdqndv2lem2  36683  knoppndvlem11  36695  knoppndvlem12  36696  knoppndvlem14  36698  knoppndvlem15  36699  knoppndvlem17  36701  knoppndvlem18  36702  knoppndvlem19  36703  knoppndvlem21  36705  ltflcei  37778  poimirlem9  37799  poimirlem26  37816  poimirlem27  37817  poimirlem29  37819  heicant  37825  mblfinlem2  37828  mblfinlem3  37829  mblfinlem4  37830  volsupnfl  37835  itg2addnclem  37841  itg2addnclem3  37843  iblmulc2nc  37855  ftc1cnnclem  37861  ftc1anclem6  37868  ftc1anclem7  37869  ftc1anclem8  37870  ftc2nc  37872  dvasin  37874  geomcau  37929  bfplem2  37993  rrncmslem  38002  rrnequiv  38005  lsatcvatlem  39344  islshpcv  39348  atlatmstc  39614  cvlsupr7  39643  cvrval3  39708  cvrval5  39710  cvrexchlem  39714  atcvrj1  39726  cvrat3  39737  cvrat4  39738  atbtwn  39741  1cvratex  39768  hlatexch4  39776  3atlem1  39778  3atlem2  39779  atcvrlln2  39814  atcvrlln  39815  lplnllnneN  39851  llncvrlpln2  39852  4atlem3b  39893  lplncvrlvol2  39910  dalemswapyz  39951  dalemswapyzps  39985  dalem25  39993  dalem39  40006  dalem58  40025  dalem59  40026  lneq2at  40073  lncvrat  40077  dalawlem2  40167  dalawlem3  40168  dalawlem4  40169  dalawlem6  40171  dalawlem9  40174  dalawlem11  40176  dalawlem12  40177  lhpocnle  40311  lhpmcvr3  40320  lhpmcvr5N  40322  lhpmcvr6N  40323  4atexlemunv  40361  4atexlemc  40364  4atexlemex2  40366  lautm  40389  cdlemc2  40487  cdleme5  40535  cdleme11j  40562  cdleme16b  40574  cdlemednpq  40594  cdleme19e  40602  cdleme20i  40612  cdleme22a  40635  cdleme22cN  40637  cdleme22d  40638  cdleme22e  40639  cdleme22eALTN  40640  cdleme22f  40641  cdleme23c  40646  cdleme30a  40673  cdleme35a  40743  cdleme35b  40745  cdleme42h  40777  cdlemeg46rgv  40823  cdlemg8b  40923  cdlemg12e  40942  cdlemg13a  40946  cdlemg17pq  40967  cdlemg18c  40975  cdlemg19  40979  cdlemg21  40981  cdlemg31d  40995  cdlemg33a  41001  tendoid  41068  cdlemk4  41129  cdlemki  41136  cdlemk10  41138  cdlemksv2  41142  cdlemk12  41145  cdlemk14  41149  cdlemk15  41150  cdlemk1u  41154  cdlemk5u  41156  cdlemk12u  41167  cdlemk45  41242  cdlemk48  41245  dia2dimlem1  41359  dia2dimlem2  41360  dia2dimlem3  41361  cdlemm10N  41413  cdlemn2  41490  dihjustlem  41511  dihglbcpreN  41595  dihmeetlem3N  41600  nnproddivdvdsd  42289  lcmineqlem17  42334  lcmineqlem18  42335  3lexlogpow2ineq1  42347  3lexlogpow2ineq2  42348  3lexlogpow5ineq5  42349  aks4d1p1p3  42358  aks4d1p1p2  42359  aks4d1p1p4  42360  aks4d1p1p5  42364  aks4d1p1  42365  aks4d1p3  42367  aks4d1p8  42376  posbezout  42389  primrootspoweq0  42395  aks6d1c1  42405  hashscontpow1  42410  aks6d1c4  42413  aks6d1c2  42419  aks6d1c5lem1  42425  aks6d1c5lem3  42426  aks6d1c5lem2  42427  deg1gprod  42429  sticksstones7  42441  sticksstones10  42444  sticksstones12  42447  sticksstones22  42457  aks6d1c6lem1  42459  aks6d1c6lem3  42461  aks6d1c6lem4  42462  bcled  42467  bcle2d  42468  aks6d1c7lem1  42469  unitscyglem4  42487  aks5lem7  42489  aks5  42493  explt1d  42615  mulgt0b2d  42770  evlselv  42867  dffltz  42914  fltdvdsabdvdsc  42918  fltaccoprm  42920  fltabcoprm  42922  flt4lem5elem  42931  flt4lem7  42939  fltnlta  42943  irrapxlem1  43101  pell1qrgaplem  43152  pell1qrgap  43153  monotoddzzfi  43221  jm2.24nn  43238  congtr  43244  congmul  43246  congsub  43249  fzmaxdif  43260  acongeq  43262  jm2.20nn  43276  jm2.25  43278  hbtlem4  43405  dgrsub2  43414  mpaaeu  43429  idomsubgmo  43472  iscard4  43811  sqrtcvallem4  43917  leeq2d  44436  int-sqgeq0d  44464  int-ineqmvtd  44469  cvgdvgrat  44591  radcnvrat  44592  hashnzfzclim  44600  dvconstbi  44612  binomcxplemdvbinom  44631  isosctrlem1ALT  45211  mulltgt0  45304  rnmptbd2lem  45529  oddfl  45563  2timesgt  45573  lt3addmuld  45586  lt4addmuld  45591  supxrgere  45615  supxrgelem  45619  supxrge  45620  xadd0ge2  45623  infrpge  45633  xrlexaddrp  45634  xralrple2  45636  infxr  45648  infleinflem1  45651  infleinflem2  45652  infleinf  45653  xralrple4  45654  xralrple3  45655  recnnltrp  45658  rpgtrecnn  45661  xrralrecnnge  45671  rexabslelem  45699  infrnmptle  45704  supminfxr  45745  xrpnf  45766  iccshift  45801  iooshift  45805  ressiocsup  45837  ressioosup  45838  fsumnncl  45855  fmul01  45863  fmul01lt1lem1  45867  fmul01lt1lem2  45868  mccllem  45880  climrec  45886  climexp  45888  climneg  45893  limcrecl  45912  sumnnodd  45913  lptioo2  45914  lptioo1  45915  ltmod  45919  lptre2pt  45921  0ellimcdiv  45930  limclner  45932  fnlimcnv  45948  climinf2lem  45987  limsupubuzlem  45993  limsup10exlem  46053  limsupgtlem  46058  dfxlim2v  46128  xlimliminflimsup  46143  cncficcgt0  46169  cncfioobdlem  46177  ioodvbdlimc1lem1  46212  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  dvdsn1add  46220  dvnxpaek  46223  dvnmul  46224  dvnprodlem1  46227  itgiccshift  46261  itgperiod  46262  sublevolico  46265  ismbl3  46267  ovolsplit  46269  ismbl4  46274  stoweidlem1  46282  stoweidlem11  46292  stoweidlem13  46294  stoweidlem26  46307  stoweidlem34  46315  stoweidlem38  46319  stoweidlem42  46323  stoweidlem51  46332  stoweidlem59  46340  stirlinglem5  46359  stirlinglem6  46360  stirlinglem7  46361  stirlinglem10  46364  stirlinglem11  46365  stirlinglem13  46367  stirlinglem15  46369  dirkercncflem1  46384  dirkercncflem4  46387  fourierdlem4  46392  fourierdlem10  46398  fourierdlem11  46399  fourierdlem15  46403  fourierdlem20  46408  fourierdlem25  46413  fourierdlem26  46414  fourierdlem30  46418  fourierdlem37  46425  fourierdlem39  46427  fourierdlem40  46428  fourierdlem41  46429  fourierdlem42  46430  fourierdlem44  46432  fourierdlem47  46434  fourierdlem48  46435  fourierdlem49  46436  fourierdlem50  46437  fourierdlem51  46438  fourierdlem52  46439  fourierdlem54  46441  fourierdlem60  46447  fourierdlem61  46448  fourierdlem63  46450  fourierdlem64  46451  fourierdlem65  46452  fourierdlem73  46460  fourierdlem74  46461  fourierdlem75  46462  fourierdlem76  46463  fourierdlem78  46465  fourierdlem79  46466  fourierdlem81  46468  fourierdlem84  46471  fourierdlem87  46474  fourierdlem92  46479  fourierdlem93  46480  fourierdlem101  46488  fourierdlem102  46489  fourierdlem103  46490  fourierdlem104  46491  fourierdlem111  46498  fourierdlem114  46501  sqwvfoura  46509  sqwvfourb  46510  fouriersw  46512  etransclem19  46534  etransclem23  46538  etransclem24  46539  etransclem25  46540  etransclem27  46542  etransclem32  46547  etransclem35  46550  etransclem48  46563  qndenserrnbllem  46575  ioorrnopnlem  46585  ioorrnopnxrlem  46587  fsumlesge0  46658  sge0cl  46662  sge0supre  46670  sge0less  46673  sge0gerp  46676  sge0ltfirp  46681  sge0le  46688  sge0ltfirpmpt  46689  sge0split  46690  sge0rpcpnf  46702  sge0ltfirpmpt2  46707  sge0isum  46708  sge0xaddlem1  46714  sge0pnffigtmpt  46721  sge0pnffsumgt  46723  sge0gtfsumgt  46724  sge0seq  46727  nnfoctbdjlem  46736  meassle  46744  meaiuninclem  46761  meaiininclem  46767  omeiunle  46798  omeiunltfirp  46800  carageniuncllem2  46803  carageniuncl  46804  omess0  46815  hoicvr  46829  ovnlerp  46843  ovnsubaddlem1  46851  hsphoidmvle2  46866  hoidmv1lelem2  46873  hoidmv1le  46875  hoidmvlelem1  46876  hoidmvlelem2  46877  hoidmvlelem3  46878  hoidmvlelem5  46880  ovnhoilem2  46883  ovnhoi  46884  hoidifhspdmvle  46901  hoiqssbllem2  46904  hspmbllem2  46908  hspmbllem3  46909  hspmbl  46910  vonioolem2  46962  vonicclem2  46965  smfaddlem1  47044  smflimlem2  47053  smflimlem4  47055  smfmullem1  47072  smfinflem  47098  smflimsuplem4  47104  smflimsuplem8  47108  chnsubseq  47161  perfectALTVlem2  48005  nnpw2blen  48863  itscnhlinecirc02plem1  49065  funcoppc3  49429  oppcuprcl2  49484  isinito3  49782