Theorem breqtrd 5169

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  breqtrrd  5171  breqtrid  5180  domunsn  9167  mapdom2  9188  phplem2  9245  phplem4OLD  9257  mapfien2  9449  wemaplem2  9587  infdifsn  9697  cantnff  9714  ttrclss  9760  rnttrcl  9762  infxpenlem  10053  infmap2  10257  ssfin4  10350  canthp1lem1  10692  nqereq  10975  ltexnq  11015  ltbtwnnq  11018  add20  11775  mullt0  11782  ltm1  12109  recgt0  12113  prodgt0  12114  ltmul1a  12116  mulge0b  12138  recp1lt1  12166  recreclt  12167  ledivp1  12170  ledivp1i  12193  ltdivp1i  12194  eluzmn  12885  ltaddrp2d  13111  mul2lt0bi  13141  prodge0rd  13142  xleadd1a  13295  xov1plusxeqvd  13538  fz01en  13592  fzonmapblen  13748  fladdz  13865  flhalf  13870  fldiv  13900  modsubdir  13981  fzen2  14010  serle  14098  ltexp2a  14206  leexp2a  14212  exple1  14216  expubnd  14217  bernneq  14268  expmulnbnd  14274  discr1  14278  discr  14279  faclbnd6  14338  hashfz  14466  hashfun  14476  seqcoll  14503  sqeqd  15205  01sqrexlem7  15287  sqrtge0  15296  sqrtneglem  15305  abslt  15353  absle  15354  abstri  15369  rlimge0  15617  reccn2  15633  climaddc2  15672  isercolllem1  15701  caucvgrlem  15709  summolem2a  15751  isumge0  15802  fsumle  15835  fsumlt  15836  o1fsum  15849  supcvg  15892  expcnv  15900  geolim  15906  geolim2  15907  georeclim  15908  geo2lim  15911  mertenslem1  15920  mertens  15922  prodmolem2a  15970  efcllem  16113  ef0lem  16114  efgt0  16139  eftlub  16145  eflt  16153  sinbnd  16216  cosbnd  16217  ef01bndlem  16220  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  eirrlem  16240  rpnnen2lem11  16260  rpnnen2lem12  16261  ruclem11  16276  dvdssub2  16338  dvdsadd2b  16343  dvdsexp  16365  3dvds  16368  opoe  16400  bitsfzolem  16471  bitsinv1lem  16478  bezoutlem4  16579  dvdsgcd  16581  dvdsmulgcd  16593  bezoutr1  16606  nn0seqcvgd  16607  rpmulgcd2  16693  qredeq  16694  rpdvds  16697  prmind2  16722  divdenle  16786  hashdvds  16812  phimullem  16816  eulerthlem2  16819  prmdiveq  16823  prmdivdiv  16824  pythagtriplem4  16857  pythagtriplem10  16858  pythagtriplem19  16871  iserodd  16873  pcpre1  16880  pcadd2  16928  qexpz  16939  expnprm  16940  oddprmdvds  16941  pockthlem  16943  prmreclem2  16955  prmreclem3  16956  4sqlem7  16982  4sqlem10  16985  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  4sqlem15  16997  4sqlem16  16998  0ram  17058  ffthiso  17976  latmlej12  18524  qusgrp  19204  pgpfi1  19613  sylow1lem4  19619  sylow1lem5  19620  odcau  19622  pgpfi  19623  pgpssslw  19632  sylow3lem4  19648  sylow3lem6  19650  efgsfo  19757  frgp0  19778  odadd1  19866  odadd2  19867  odadd  19868  gexexlem  19870  lt6abl  19913  gsumzsubmcl  19936  pwsgsum  20000  dprd2dlem1  20061  dprd2d2  20064  ablfacrplem  20085  ablfacrp  20086  ablfacrp2  20087  ablfac1b  20090  ablfac1eu  20093  pgpfac1lem3a  20096  ablfaclem2  20106  dvdsrid  20367  dvdsrtr  20368  dvdsrneg  20370  unitmulcl  20380  unitgrp  20383  unitnegcl  20397  subrguss  20587  subrgunit  20590  isdrng2  20743  fidomndrnglem  20773  abvsubtri  20828  gzrngunit  21451  prmirredlem  21483  znidomb  21580  frlmgsum  21792  psrbaglesupp  21942  psdmul  22170  psdmvr  22173  invrvald  22682  psmetsym  24320  psmettri  24321  mettri2  24351  xmetsym  24357  xmettri  24361  prdsxmetlem  24378  xblss2ps  24411  xblss2  24412  blhalf  24415  xmsge0  24473  ngptgp  24649  nrginvrcnlem  24712  nmoeq0  24757  cnmet  24792  blcvx  24819  opnreen  24853  metdcnlem  24858  metdstri  24873  metdsle  24874  metnrmlem1  24881  metnrmlem3  24883  lebnumlem1  24993  pi1inv  25085  cphnmf  25229  ipge0  25232  ipcau2  25268  tcphcphlem1  25269  csbren  25433  minveclem2  25460  minveclem3  25463  ovolssnul  25522  ovolctb  25525  ovolunnul  25535  ovoliunlem1  25537  ovoliun2  25541  ovoliunnul  25542  ioombl1lem4  25596  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  volcn  25641  vitalilem2  25644  vitalilem5  25647  itg1lea  25747  mbfi1fseqlem6  25755  mbfi1flimlem  25757  itg2eqa  25780  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2cnlem2  25797  iblabsr  25865  iblmulc2  25866  bddiblnc  25877  dveflem  26017  dvef  26018  dvferm2lem  26024  dvlip  26032  c1liplem1  26035  dveq0  26039  dvlt0  26044  dvivthlem1  26047  lhop1  26053  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem4  26070  dvfsumrlim3  26074  dvfsum2  26075  ftc1a  26078  ftc1lem4  26080  deg1add  26142  ply1divex  26176  ply1rem  26205  fta1glem2  26208  fta1blem  26210  ig1pdvds  26219  plyeq0lem  26249  dgrcolem2  26314  plydivlem4  26338  plyrem  26347  fta1lem  26349  aalioulem3  26376  aaliou2b  26383  aaliou3lem3  26386  aaliou3lem8  26387  ulmcn  26442  ulmdvlem1  26443  itgulm  26451  pserulm  26465  pserdvlem2  26472  abelthlem2  26476  abelthlem5  26479  abelthlem6  26480  abelthlem7  26482  abelthlem8  26483  abelthlem9  26484  sinq12gt0  26549  sinq34lt0t  26551  cosq14gt0  26552  cosq14ge0  26553  cos02pilt1  26568  efif1olem3  26586  argimgt0  26654  argimlt0  26655  logneg2  26657  logcnlem3  26686  logcnlem4  26687  logtayllem  26701  logtayl2  26704  cxpsqrtlem  26744  cxpsqrt  26745  cxpaddlelem  26794  abscxpbnd  26796  zrtdvds  26802  rtprmirr  26803  loglesqrt  26804  ang180lem2  26853  atanlogaddlem  26956  atanlogsublem  26958  atantan  26966  atans2  26974  atantayl  26980  leibpi  26985  log2tlbnd  26988  birthdaylem2  26995  birthdaylem3  26996  cxp2limlem  27019  jensenlem2  27031  jensen  27032  logdiflbnd  27038  emcllem2  27040  emcllem4  27042  harmonicbnd4  27054  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulm2  27079  lgambdd  27080  lgamucov  27081  lgamcvglem  27083  lgamcvg2  27098  gamcvg  27099  wilthlem3  27113  basellem1  27124  basellem3  27126  basellem4  27127  fsumdvdsdiaglem  27226  dvdsppwf1o  27229  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chteq0  27253  chtub  27256  chpub  27264  logfacubnd  27265  logfaclbnd  27266  logexprlim  27269  perfectlem2  27274  dchrfi  27299  bclbnd  27324  bposlem1  27328  bposlem3  27330  bposlem4  27331  bposlem6  27333  lgslem1  27341  lgsqrlem2  27391  lgsqrlem4  27393  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem1  27428  2sqlem3  27464  2sqlem4  27465  2sqlem8  27470  2sqlem11  27473  2sqcoprm  27479  2sqmod  27480  chebbnd1lem2  27514  chebbnd1lem3  27515  chtppilimlem1  27517  chpchtlim  27523  vmadivsum  27526  vmadivsumb  27527  rpvmasumlem  27531  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lem1  27560  dchrisum0lem2a  27561  mudivsum  27574  mulogsumlem  27575  mulog2sumlem2  27579  vmalogdivsum2  27582  selberglem2  27590  selbergb  27593  selberg2b  27596  logdivbnd  27600  selberg3lem1  27601  selberg3lem2  27602  selberg4lem1  27604  pntrmax  27608  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntrlog2bndlem6a  27626  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem1  27633  pntibndlem2  27635  pntlemb  27641  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemk  27650  qabvle  27669  padicabvcxp  27676  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth3  27682  addsuniflem  28034  negsid  28073  negsunif  28087  mulsuniflem  28175  sltmul2  28197  precsexlem9  28239  absmuls  28268  zscut  28393  addhalfcut  28419  legtrid  28599  legov3  28606  krippenlem  28698  mideulem2  28742  midex  28745  opphllem5  28759  opphllem6  28760  opphl  28762  lmieu  28792  lmiisolem  28804  ttgcontlem1  28899  colinearalglem4  28924  axpaschlem  28955  axcontlem7  28985  nbfusgrlevtxm2  29395  clwlksndivn  30105  eucrct2eupth  30264  nvge0  30692  smcnlem  30716  nmoub3i  30792  nmoub2i  30793  nmlno0lem  30812  minvecolem2  30894  htthlem  30936  norm3dif2  31170  bcs2  31201  chscllem2  31657  eigposi  31855  nmopub2tALT  31928  nmfnleub2  31945  nmlnop0iALT  32014  riesz1  32084  cnlnadjlem2  32087  nmopcoadji  32120  leopsq  32148  leopmul  32153  leopnmid  32157  nmopleid  32158  opsqrlem6  32164  0leopj  32205  hstle1  32245  strlem3a  32271  mdslmd4i  32352  cvexchlem  32387  cdj1i  32452  unidifsnel  32553  unidifsnne  32554  le2halvesd  32759  xlt2addrd  32762  fsumub  32830  2exple2exp  32834  wrdt2ind  32938  xrge0tsmsd  33065  fzto1st1  33122  cycpmco2lem4  33149  cycpmco2lem6  33151  cyc3conja  33177  archiabllem1a  33198  archiabllem2a  33201  archiabllem2c  33202  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  orng0le1  33342  rprmdvdsprod  33562  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  ply1dg3rt0irred  33607  exsslsb  33647  fedgmullem1  33680  fedgmullem2  33681  fldsdrgfldext2  33713  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  fldext2rspun  33732  algextdeglem8  33765  rtelextdg2lem  33767  metideq  33892  metider  33893  sqsscirc1  33907  esummono  34055  esumpad2  34057  esumle  34059  esumlef  34063  esumcst  34064  esumrnmpt2  34069  esum2d  34094  aean  34245  dya2ub  34272  dya2icoseg  34279  omssubadd  34302  inelcarsg  34313  carsgsigalem  34317  carsggect  34320  carsgclctunlem2  34321  eulerpartlemb  34370  fibp1  34403  sgnmulsgp  34553  signsplypnf  34565  signsply0  34566  fdvposlt  34614  fdvposle  34616  reprgt  34636  logdivsqrle  34665  hgt750lemb  34671  hgt750leme  34673  tgoldbachgtde  34675  subfacval3  35194  sconnpht2  35243  sconnpi1  35244  resconn  35251  snmlff  35334  sinccvglem  35677  faclimlem2  35744  btwnouttr2  36023  weiunpo  36466  dnibndlem5  36483  dnibndlem7  36485  dnibndlem8  36486  dnibndlem9  36487  dnibndlem10  36488  dnibnd  36492  knoppcnlem4  36497  knoppcnlem9  36502  unbdqndv2lem1  36510  unbdqndv2lem2  36511  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem18  36530  knoppndvlem19  36531  knoppndvlem21  36533  ltflcei  37615  poimirlem9  37636  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  volsupnfl  37672  itg2addnclem  37678  itg2addnclem3  37680  iblmulc2nc  37692  ftc1cnnclem  37698  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc2nc  37709  dvasin  37711  geomcau  37766  bfplem2  37830  rrncmslem  37839  rrnequiv  37842  lsatcvatlem  39050  islshpcv  39054  atlatmstc  39320  cvlsupr7  39349  cvrval3  39415  cvrval5  39417  cvrexchlem  39421  atcvrj1  39433  cvrat3  39444  cvrat4  39445  atbtwn  39448  1cvratex  39475  hlatexch4  39483  3atlem1  39485  3atlem2  39486  atcvrlln2  39521  atcvrlln  39522  lplnllnneN  39558  llncvrlpln2  39559  4atlem3b  39600  lplncvrlvol2  39617  dalemswapyz  39658  dalemswapyzps  39692  dalem25  39700  dalem39  39713  dalem58  39732  dalem59  39733  lneq2at  39780  lncvrat  39784  dalawlem2  39874  dalawlem3  39875  dalawlem4  39876  dalawlem6  39878  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  lhpocnle  40018  lhpmcvr3  40027  lhpmcvr5N  40029  lhpmcvr6N  40030  4atexlemunv  40068  4atexlemc  40071  4atexlemex2  40073  lautm  40096  cdlemc2  40194  cdleme5  40242  cdleme11j  40269  cdleme16b  40281  cdlemednpq  40301  cdleme19e  40309  cdleme20i  40319  cdleme22a  40342  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme23c  40353  cdleme30a  40380  cdleme35a  40450  cdleme35b  40452  cdleme42h  40484  cdlemeg46rgv  40530  cdlemg8b  40630  cdlemg12e  40649  cdlemg13a  40653  cdlemg17pq  40674  cdlemg18c  40682  cdlemg19  40686  cdlemg21  40688  cdlemg31d  40702  cdlemg33a  40708  tendoid  40775  cdlemk4  40836  cdlemki  40843  cdlemk10  40845  cdlemksv2  40849  cdlemk12  40852  cdlemk14  40856  cdlemk15  40857  cdlemk1u  40861  cdlemk5u  40863  cdlemk12u  40874  cdlemk45  40949  cdlemk48  40952  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  cdlemm10N  41120  cdlemn2  41197  dihjustlem  41218  dihglbcpreN  41302  dihmeetlem3N  41307  nnproddivdvdsd  42001  lcmineqlem17  42046  lcmineqlem18  42047  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p3  42079  aks4d1p8  42088  posbezout  42101  primrootspoweq0  42107  aks6d1c1  42117  hashscontpow1  42122  aks6d1c4  42125  aks6d1c2  42131  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c5lem2  42139  deg1gprod  42141  sticksstones7  42153  sticksstones10  42156  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem1  42171  aks6d1c6lem3  42173  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  unitscyglem4  42199  aks5lem7  42201  aks5  42205  2xp3dxp2ge1d  42242  factwoffsmonot  42243  explt1d  42358  evlselv  42597  dffltz  42644  fltdvdsabdvdsc  42648  fltaccoprm  42650  fltabcoprm  42652  flt4lem5elem  42661  flt4lem7  42669  fltnlta  42673  irrapxlem1  42833  pell1qrgaplem  42884  pell1qrgap  42885  monotoddzzfi  42954  jm2.24nn  42971  congtr  42977  congmul  42979  congsub  42982  fzmaxdif  42993  acongeq  42995  jm2.20nn  43009  jm2.25  43011  hbtlem4  43138  dgrsub2  43147  mpaaeu  43162  idomsubgmo  43205  iscard4  43546  sqrtcvallem4  43652  leeq2d  44171  int-sqgeq0d  44199  int-ineqmvtd  44204  cvgdvgrat  44332  radcnvrat  44333  hashnzfzclim  44341  dvconstbi  44353  binomcxplemdvbinom  44372  isosctrlem1ALT  44954  mulltgt0  45027  rnmptbd2lem  45255  oddfl  45289  2timesgt  45300  lt3addmuld  45313  lt4addmuld  45318  supxrgere  45344  supxrgelem  45348  supxrge  45349  xadd0ge2  45352  infrpge  45362  xrlexaddrp  45363  xralrple2  45365  infxr  45378  infleinflem1  45381  infleinflem2  45382  infleinf  45383  xralrple4  45384  xralrple3  45385  recnnltrp  45388  rpgtrecnn  45391  xrralrecnnge  45401  rexabslelem  45429  infrnmptle  45434  supminfxr  45475  xrpnf  45496  iccshift  45531  iooshift  45535  ressiocsup  45567  ressioosup  45568  fsumnncl  45587  fmul01  45595  fmul01lt1lem1  45599  fmul01lt1lem2  45600  mccllem  45612  climrec  45618  climexp  45620  climneg  45625  limcrecl  45644  sumnnodd  45645  lptioo2  45646  lptioo1  45647  ltmod  45653  lptre2pt  45655  0ellimcdiv  45664  limclner  45666  fnlimcnv  45682  climinf2lem  45721  limsupubuzlem  45727  limsup10exlem  45787  limsupgtlem  45792  dfxlim2v  45862  xlimliminflimsup  45877  cncficcgt0  45903  cncfioobdlem  45911  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvdsn1add  45954  dvnxpaek  45957  dvnmul  45958  dvnprodlem1  45961  itgiccshift  45995  itgperiod  45996  sublevolico  45999  ismbl3  46001  ovolsplit  46003  ismbl4  46008  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  stoweidlem38  46053  stoweidlem42  46057  stoweidlem51  46066  stoweidlem59  46074  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem13  46101  stirlinglem15  46103  dirkercncflem1  46118  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem10  46132  fourierdlem11  46133  fourierdlem15  46137  fourierdlem20  46142  fourierdlem25  46147  fourierdlem26  46148  fourierdlem30  46152  fourierdlem37  46159  fourierdlem39  46161  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem44  46166  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem54  46175  fourierdlem60  46181  fourierdlem61  46182  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem81  46202  fourierdlem84  46205  fourierdlem87  46208  fourierdlem92  46213  fourierdlem93  46214  fourierdlem101  46222  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  etransclem19  46268  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem27  46276  etransclem32  46281  etransclem35  46284  etransclem48  46297  qndenserrnbllem  46309  ioorrnopnlem  46319  ioorrnopnxrlem  46321  fsumlesge0  46392  sge0cl  46396  sge0supre  46404  sge0less  46407  sge0gerp  46410  sge0ltfirp  46415  sge0le  46422  sge0ltfirpmpt  46423  sge0split  46424  sge0rpcpnf  46436  sge0ltfirpmpt2  46441  sge0isum  46442  sge0xaddlem1  46448  sge0pnffigtmpt  46455  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0seq  46461  nnfoctbdjlem  46470  meassle  46478  meaiuninclem  46495  meaiininclem  46501  omeiunle  46532  omeiunltfirp  46534  carageniuncllem2  46537  carageniuncl  46538  omess0  46549  hoicvr  46563  ovnlerp  46577  ovnsubaddlem1  46585  hsphoidmvle2  46600  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem5  46614  ovnhoilem2  46617  ovnhoi  46618  hoidifhspdmvle  46635  hoiqssbllem2  46638  hspmbllem2  46642  hspmbllem3  46643  hspmbl  46644  vonioolem2  46696  vonicclem2  46699  smfaddlem1  46778  smflimlem2  46787  smflimlem4  46789  smfmullem1  46806  smfinflem  46832  smflimsuplem4  46838  smflimsuplem8  46842  perfectALTVlem2  47709  nnpw2blen  48501  itscnhlinecirc02plem1  48703