Theorem breqtrd 5145

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

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

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 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  breqtrrd  5147  breqtrid  5156  domunsn  9139  mapdom2  9160  phplem2  9217  mapfien2  9419  wemaplem2  9559  infdifsn  9669  cantnff  9686  ttrclss  9732  rnttrcl  9734  infxpenlem  10025  infmap2  10229  ssfin4  10322  canthp1lem1  10664  nqereq  10947  ltexnq  10987  ltbtwnnq  10990  add20  11747  mullt0  11754  ltm1  12081  recgt0  12085  prodgt0  12086  ltmul1a  12088  mulge0b  12110  recp1lt1  12138  recreclt  12139  ledivp1  12142  ledivp1i  12165  ltdivp1i  12166  eluzmn  12857  ltaddrp2d  13083  mul2lt0bi  13113  prodge0rd  13114  xleadd1a  13267  xov1plusxeqvd  13513  fz01en  13567  fzonmapblen  13723  fladdz  13840  flhalf  13845  fldiv  13875  modsubdir  13956  fzen2  13985  serle  14073  ltexp2a  14182  leexp2a  14188  exple1  14193  expubnd  14194  bernneq  14245  expmulnbnd  14251  discr1  14255  discr  14256  faclbnd6  14315  hashfz  14443  hashfun  14453  seqcoll  14480  sqeqd  15183  01sqrexlem7  15265  sqrtge0  15274  sqrtneglem  15283  abslt  15331  absle  15332  abstri  15347  rlimge0  15595  reccn2  15611  climaddc2  15650  isercolllem1  15679  caucvgrlem  15687  summolem2a  15729  isumge0  15780  fsumle  15813  fsumlt  15814  o1fsum  15827  supcvg  15870  expcnv  15878  geolim  15884  geolim2  15885  georeclim  15886  geo2lim  15889  mertenslem1  15898  mertens  15900  prodmolem2a  15948  efcllem  16091  ef0lem  16092  efgt0  16119  eftlub  16125  eflt  16133  sinbnd  16196  cosbnd  16197  ef01bndlem  16200  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  eirrlem  16220  rpnnen2lem11  16240  rpnnen2lem12  16241  ruclem11  16256  dvdssub2  16318  dvdsadd2b  16323  dvdsexp  16345  3dvds  16348  opoe  16380  bitsfzolem  16451  bitsinv1lem  16458  bezoutlem4  16559  dvdsgcd  16561  dvdsmulgcd  16573  bezoutr1  16586  nn0seqcvgd  16587  rpmulgcd2  16673  qredeq  16674  rpdvds  16677  prmind2  16702  divdenle  16766  hashdvds  16792  phimullem  16796  eulerthlem2  16799  prmdiveq  16803  prmdivdiv  16804  pythagtriplem4  16837  pythagtriplem10  16838  pythagtriplem19  16851  iserodd  16853  pcpre1  16860  pcadd2  16908  qexpz  16919  expnprm  16920  oddprmdvds  16921  pockthlem  16923  prmreclem2  16935  prmreclem3  16936  4sqlem7  16962  4sqlem10  16965  4sqlem11  16973  4sqlem12  16974  4sqlem14  16976  4sqlem15  16977  4sqlem16  16978  0ram  17038  ffthiso  17942  latmlej12  18487  qusgrp  19167  pgpfi1  19574  sylow1lem4  19580  sylow1lem5  19581  odcau  19583  pgpfi  19584  pgpssslw  19593  sylow3lem4  19609  sylow3lem6  19611  efgsfo  19718  frgp0  19739  odadd1  19827  odadd2  19828  odadd  19829  gexexlem  19831  lt6abl  19874  gsumzsubmcl  19897  pwsgsum  19961  dprd2dlem1  20022  dprd2d2  20025  ablfacrplem  20046  ablfacrp  20047  ablfacrp2  20048  ablfac1b  20051  ablfac1eu  20054  pgpfac1lem3a  20057  ablfaclem2  20067  dvdsrid  20325  dvdsrtr  20326  dvdsrneg  20328  unitmulcl  20338  unitgrp  20341  unitnegcl  20355  subrguss  20545  subrgunit  20548  isdrng2  20701  fidomndrnglem  20730  abvsubtri  20785  gzrngunit  21399  prmirredlem  21431  znidomb  21520  frlmgsum  21730  psrbaglesupp  21880  psdmul  22102  psdmvr  22105  invrvald  22612  psmetsym  24247  psmettri  24248  mettri2  24278  xmetsym  24284  xmettri  24288  prdsxmetlem  24305  xblss2ps  24338  xblss2  24339  blhalf  24342  xmsge0  24400  ngptgp  24573  nrginvrcnlem  24628  nmoeq0  24673  cnmet  24708  blcvx  24735  opnreen  24769  metdcnlem  24774  metdstri  24789  metdsle  24790  metnrmlem1  24797  metnrmlem3  24799  lebnumlem1  24909  pi1inv  25001  cphnmf  25145  ipge0  25148  ipcau2  25184  tcphcphlem1  25185  csbren  25349  minveclem2  25376  minveclem3  25379  ovolssnul  25438  ovolctb  25441  ovolunnul  25451  ovoliunlem1  25453  ovoliun2  25457  ovoliunnul  25458  ioombl1lem4  25512  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombl  25540  volcn  25557  vitalilem2  25560  vitalilem5  25563  itg1lea  25663  mbfi1fseqlem6  25671  mbfi1flimlem  25673  itg2eqa  25696  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2cnlem2  25713  iblabsr  25781  iblmulc2  25782  bddiblnc  25793  dveflem  25933  dvef  25934  dvferm2lem  25940  dvlip  25948  c1liplem1  25951  dveq0  25955  dvlt0  25960  dvivthlem1  25963  lhop1  25969  dvfsumle  25976  dvfsumleOLD  25977  dvfsumlem4  25986  dvfsumrlim3  25990  dvfsum2  25991  ftc1a  25994  ftc1lem4  25996  deg1add  26058  ply1divex  26092  ply1rem  26121  fta1glem2  26124  fta1blem  26126  ig1pdvds  26135  plyeq0lem  26165  dgrcolem2  26230  plydivlem4  26254  plyrem  26263  fta1lem  26265  aalioulem3  26292  aaliou2b  26299  aaliou3lem3  26302  aaliou3lem8  26303  ulmcn  26358  ulmdvlem1  26359  itgulm  26367  pserulm  26381  pserdvlem2  26388  abelthlem2  26392  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem8  26399  abelthlem9  26400  sinq12gt0  26466  sinq34lt0t  26468  cosq14gt0  26469  cosq14ge0  26470  cos02pilt1  26485  efif1olem3  26503  argimgt0  26571  argimlt0  26572  logneg2  26574  logcnlem3  26603  logcnlem4  26604  logtayllem  26618  logtayl2  26621  cxpsqrtlem  26661  cxpsqrt  26662  cxpaddlelem  26711  abscxpbnd  26713  zrtdvds  26719  rtprmirr  26720  loglesqrt  26721  ang180lem2  26770  atanlogaddlem  26873  atanlogsublem  26875  atantan  26883  atans2  26891  atantayl  26897  leibpi  26902  log2tlbnd  26905  birthdaylem2  26912  birthdaylem3  26913  cxp2limlem  26936  jensenlem2  26948  jensen  26949  logdiflbnd  26955  emcllem2  26957  emcllem4  26959  harmonicbnd4  26971  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulm2  26996  lgambdd  26997  lgamucov  26998  lgamcvglem  27000  lgamcvg2  27015  gamcvg  27016  wilthlem3  27030  basellem1  27041  basellem3  27043  basellem4  27044  fsumdvdsdiaglem  27143  dvdsppwf1o  27146  mpodvdsmulf1o  27154  dvdsmulf1o  27156  chteq0  27170  chtub  27173  chpub  27181  logfacubnd  27182  logfaclbnd  27183  logexprlim  27186  perfectlem2  27191  dchrfi  27216  bclbnd  27241  bposlem1  27245  bposlem3  27247  bposlem4  27248  bposlem6  27250  lgslem1  27258  lgsqrlem2  27308  lgsqrlem4  27310  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem1  27345  2sqlem3  27381  2sqlem4  27382  2sqlem8  27387  2sqlem11  27390  2sqcoprm  27396  2sqmod  27397  chebbnd1lem2  27431  chebbnd1lem3  27432  chtppilimlem1  27434  chpchtlim  27440  vmadivsum  27443  vmadivsumb  27444  rpvmasumlem  27448  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrisum0flblem2  27470  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lem1  27477  dchrisum0lem2a  27478  mudivsum  27491  mulogsumlem  27492  mulog2sumlem2  27496  vmalogdivsum2  27499  selberglem2  27507  selbergb  27510  selberg2b  27513  logdivbnd  27517  selberg3lem1  27518  selberg3lem2  27519  selberg4lem1  27521  pntrmax  27525  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntrlog2bndlem6a  27543  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem1  27550  pntibndlem2  27552  pntlemb  27558  pntlemq  27562  pntlemr  27563  pntlemj  27564  pntlemk  27567  qabvle  27586  padicabvcxp  27593  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth3  27599  addsuniflem  27951  negsid  27990  negsunif  28004  mulsuniflem  28092  sltmul2  28114  precsexlem9  28156  absmuls  28185  zscut  28310  addhalfcut  28336  legtrid  28516  legov3  28523  krippenlem  28615  mideulem2  28659  midex  28662  opphllem5  28676  opphllem6  28677  opphl  28679  lmieu  28709  lmiisolem  28721  ttgcontlem1  28810  colinearalglem4  28834  axpaschlem  28865  axcontlem7  28895  nbfusgrlevtxm2  29303  clwlksndivn  30013  eucrct2eupth  30172  nvge0  30600  smcnlem  30624  nmoub3i  30700  nmoub2i  30701  nmlno0lem  30720  minvecolem2  30802  htthlem  30844  norm3dif2  31078  bcs2  31109  chscllem2  31565  eigposi  31763  nmopub2tALT  31836  nmfnleub2  31853  nmlnop0iALT  31922  riesz1  31992  cnlnadjlem2  31995  nmopcoadji  32028  leopsq  32056  leopmul  32061  leopnmid  32065  nmopleid  32066  opsqrlem6  32072  0leopj  32113  hstle1  32153  strlem3a  32179  mdslmd4i  32260  cvexchlem  32295  cdj1i  32360  unidifsnel  32462  unidifsnne  32463  le2halvesd  32679  xlt2addrd  32682  fsumub  32753  sgnmulsgp  32768  2exple2exp  32770  oexpled  32772  wrdt2ind  32875  xrge0tsmsd  33002  fzto1st1  33059  cycpmco2lem4  33086  cycpmco2lem6  33088  cyc3conja  33114  archiabllem1a  33135  archiabllem2a  33138  archiabllem2c  33139  orngsqr  33272  ornglmulle  33273  orngrmulle  33274  orng0le1  33280  rprmdvdsprod  33495  1arithidomlem1  33496  1arithidomlem2  33497  1arithidom  33498  ply1dg3rt0irred  33541  exsslsb  33582  fedgmullem1  33615  fedgmullem2  33616  fldsdrgfldext2  33650  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  fldext2rspun  33669  algextdeglem8  33704  rtelextdg2lem  33706  constrext2chnlem  33730  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  metideq  33870  metider  33871  sqsscirc1  33885  esummono  34031  esumpad2  34033  esumle  34035  esumlef  34039  esumcst  34040  esumrnmpt2  34045  esum2d  34070  aean  34221  dya2ub  34248  dya2icoseg  34255  omssubadd  34278  inelcarsg  34289  carsgsigalem  34293  carsggect  34296  carsgclctunlem2  34297  eulerpartlemb  34346  fibp1  34379  signsplypnf  34528  signsply0  34529  fdvposlt  34577  fdvposle  34579  reprgt  34599  logdivsqrle  34628  hgt750lemb  34634  hgt750leme  34636  tgoldbachgtde  34638  subfacval3  35157  sconnpht2  35206  sconnpi1  35207  resconn  35214  snmlff  35297  sinccvglem  35640  faclimlem2  35707  btwnouttr2  35986  weiunpo  36429  dnibndlem5  36446  dnibndlem7  36448  dnibndlem8  36449  dnibndlem9  36450  dnibndlem10  36451  dnibnd  36455  knoppcnlem4  36460  knoppcnlem9  36465  unbdqndv2lem1  36473  unbdqndv2lem2  36474  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem19  36494  knoppndvlem21  36496  ltflcei  37578  poimirlem9  37599  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  volsupnfl  37635  itg2addnclem  37641  itg2addnclem3  37643  iblmulc2nc  37655  ftc1cnnclem  37661  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc2nc  37672  dvasin  37674  geomcau  37729  bfplem2  37793  rrncmslem  37802  rrnequiv  37805  lsatcvatlem  39013  islshpcv  39017  atlatmstc  39283  cvlsupr7  39312  cvrval3  39378  cvrval5  39380  cvrexchlem  39384  atcvrj1  39396  cvrat3  39407  cvrat4  39408  atbtwn  39411  1cvratex  39438  hlatexch4  39446  3atlem1  39448  3atlem2  39449  atcvrlln2  39484  atcvrlln  39485  lplnllnneN  39521  llncvrlpln2  39522  4atlem3b  39563  lplncvrlvol2  39580  dalemswapyz  39621  dalemswapyzps  39655  dalem25  39663  dalem39  39676  dalem58  39695  dalem59  39696  lneq2at  39743  lncvrat  39747  dalawlem2  39837  dalawlem3  39838  dalawlem4  39839  dalawlem6  39841  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  lhpocnle  39981  lhpmcvr3  39990  lhpmcvr5N  39992  lhpmcvr6N  39993  4atexlemunv  40031  4atexlemc  40034  4atexlemex2  40036  lautm  40059  cdlemc2  40157  cdleme5  40205  cdleme11j  40232  cdleme16b  40244  cdlemednpq  40264  cdleme19e  40272  cdleme20i  40282  cdleme22a  40305  cdleme22cN  40307  cdleme22d  40308  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme23c  40316  cdleme30a  40343  cdleme35a  40413  cdleme35b  40415  cdleme42h  40447  cdlemeg46rgv  40493  cdlemg8b  40593  cdlemg12e  40612  cdlemg13a  40616  cdlemg17pq  40637  cdlemg18c  40645  cdlemg19  40649  cdlemg21  40651  cdlemg31d  40665  cdlemg33a  40671  tendoid  40738  cdlemk4  40799  cdlemki  40806  cdlemk10  40808  cdlemksv2  40812  cdlemk12  40815  cdlemk14  40819  cdlemk15  40820  cdlemk1u  40824  cdlemk5u  40826  cdlemk12u  40837  cdlemk45  40912  cdlemk48  40915  dia2dimlem1  41029  dia2dimlem2  41030  dia2dimlem3  41031  cdlemm10N  41083  cdlemn2  41160  dihjustlem  41181  dihglbcpreN  41265  dihmeetlem3N  41270  nnproddivdvdsd  41959  lcmineqlem17  42004  lcmineqlem18  42005  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p3  42037  aks4d1p8  42046  posbezout  42059  primrootspoweq0  42065  aks6d1c1  42075  hashscontpow1  42080  aks6d1c4  42083  aks6d1c2  42089  aks6d1c5lem1  42095  aks6d1c5lem3  42096  aks6d1c5lem2  42097  deg1gprod  42099  sticksstones7  42111  sticksstones10  42114  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem1  42129  aks6d1c6lem3  42131  aks6d1c6lem4  42132  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  unitscyglem4  42157  aks5lem7  42159  aks5  42163  2xp3dxp2ge1d  42200  factwoffsmonot  42201  explt1d  42319  evlselv  42557  dffltz  42604  fltdvdsabdvdsc  42608  fltaccoprm  42610  fltabcoprm  42612  flt4lem5elem  42621  flt4lem7  42629  fltnlta  42633  irrapxlem1  42792  pell1qrgaplem  42843  pell1qrgap  42844  monotoddzzfi  42913  jm2.24nn  42930  congtr  42936  congmul  42938  congsub  42941  fzmaxdif  42952  acongeq  42954  jm2.20nn  42968  jm2.25  42970  hbtlem4  43097  dgrsub2  43106  mpaaeu  43121  idomsubgmo  43164  iscard4  43504  sqrtcvallem4  43610  leeq2d  44129  int-sqgeq0d  44157  int-ineqmvtd  44162  cvgdvgrat  44285  radcnvrat  44286  hashnzfzclim  44294  dvconstbi  44306  binomcxplemdvbinom  44325  isosctrlem1ALT  44906  mulltgt0  44994  rnmptbd2lem  45220  oddfl  45254  2timesgt  45265  lt3addmuld  45278  lt4addmuld  45283  supxrgere  45308  supxrgelem  45312  supxrge  45313  xadd0ge2  45316  infrpge  45326  xrlexaddrp  45327  xralrple2  45329  infxr  45342  infleinflem1  45345  infleinflem2  45346  infleinf  45347  xralrple4  45348  xralrple3  45349  recnnltrp  45352  rpgtrecnn  45355  xrralrecnnge  45365  rexabslelem  45393  infrnmptle  45398  supminfxr  45439  xrpnf  45460  iccshift  45495  iooshift  45499  ressiocsup  45531  ressioosup  45532  fsumnncl  45549  fmul01  45557  fmul01lt1lem1  45561  fmul01lt1lem2  45562  mccllem  45574  climrec  45580  climexp  45582  climneg  45587  limcrecl  45606  sumnnodd  45607  lptioo2  45608  lptioo1  45609  ltmod  45615  lptre2pt  45617  0ellimcdiv  45626  limclner  45628  fnlimcnv  45644  climinf2lem  45683  limsupubuzlem  45689  limsup10exlem  45749  limsupgtlem  45754  dfxlim2v  45824  xlimliminflimsup  45839  cncficcgt0  45865  cncfioobdlem  45873  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvdsn1add  45916  dvnxpaek  45919  dvnmul  45920  dvnprodlem1  45923  itgiccshift  45957  itgperiod  45958  sublevolico  45961  ismbl3  45963  ovolsplit  45965  ismbl4  45970  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  stoweidlem26  46003  stoweidlem34  46011  stoweidlem38  46015  stoweidlem42  46019  stoweidlem51  46028  stoweidlem59  46036  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem13  46063  stirlinglem15  46065  dirkercncflem1  46080  dirkercncflem4  46083  fourierdlem4  46088  fourierdlem10  46094  fourierdlem11  46095  fourierdlem15  46099  fourierdlem20  46104  fourierdlem25  46109  fourierdlem26  46110  fourierdlem30  46114  fourierdlem37  46121  fourierdlem39  46123  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem44  46128  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem52  46135  fourierdlem54  46137  fourierdlem60  46143  fourierdlem61  46144  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem81  46164  fourierdlem84  46167  fourierdlem87  46170  fourierdlem92  46175  fourierdlem93  46176  fourierdlem101  46184  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  etransclem19  46230  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem27  46238  etransclem32  46243  etransclem35  46246  etransclem48  46259  qndenserrnbllem  46271  ioorrnopnlem  46281  ioorrnopnxrlem  46283  fsumlesge0  46354  sge0cl  46358  sge0supre  46366  sge0less  46369  sge0gerp  46372  sge0ltfirp  46377  sge0le  46384  sge0ltfirpmpt  46385  sge0split  46386  sge0rpcpnf  46398  sge0ltfirpmpt2  46403  sge0isum  46404  sge0xaddlem1  46410  sge0pnffigtmpt  46417  sge0pnffsumgt  46419  sge0gtfsumgt  46420  sge0seq  46423  nnfoctbdjlem  46432  meassle  46440  meaiuninclem  46457  meaiininclem  46463  omeiunle  46494  omeiunltfirp  46496  carageniuncllem2  46499  carageniuncl  46500  omess0  46511  hoicvr  46525  ovnlerp  46539  ovnsubaddlem1  46547  hsphoidmvle2  46562  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem5  46576  ovnhoilem2  46579  ovnhoi  46580  hoidifhspdmvle  46597  hoiqssbllem2  46600  hspmbllem2  46604  hspmbllem3  46605  hspmbl  46606  vonioolem2  46658  vonicclem2  46661  smfaddlem1  46740  smflimlem2  46749  smflimlem4  46751  smfmullem1  46768  smfinflem  46794  smflimsuplem4  46800  smflimsuplem8  46804  perfectALTVlem2  47684  nnpw2blen  48508  itscnhlinecirc02plem1  48710  funcoppc3  49038  oppcuprcl2  49083  isinito3  49333