Theorem breqtrd 5128

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtrrd  5130  breqtrid  5139  domunsn  9068  mapdom2  9089  phplem2  9146  mapfien2  9336  wemaplem2  9476  infdifsn  9588  cantnff  9605  ttrclss  9651  rnttrcl  9653  infxpenlem  9944  infmap2  10148  ssfin4  10241  canthp1lem1  10583  nqereq  10866  ltexnq  10906  ltbtwnnq  10909  add20  11668  mullt0  11675  ltm1  12002  recgt0  12006  prodgt0  12007  ltmul1a  12009  mulge0b  12031  recp1lt1  12059  recreclt  12060  ledivp1  12063  ledivp1i  12086  ltdivp1i  12087  eluzmn  12778  ltaddrp2d  13007  mul2lt0bi  13037  prodge0rd  13038  xleadd1a  13191  xov1plusxeqvd  13437  fz01en  13491  fzonmapblen  13647  fladdz  13765  flhalf  13770  fldiv  13800  modsubdir  13883  fzen2  13912  serle  14000  ltexp2a  14109  leexp2a  14115  exple1  14120  expubnd  14121  bernneq  14172  expmulnbnd  14178  discr1  14182  discr  14183  faclbnd6  14242  hashfz  14370  hashfun  14380  seqcoll  14407  sqeqd  15109  01sqrexlem7  15191  sqrtge0  15200  sqrtneglem  15209  abslt  15258  absle  15259  abstri  15274  rlimge0  15524  reccn2  15540  climaddc2  15579  isercolllem1  15608  caucvgrlem  15616  summolem2a  15658  isumge0  15709  fsumle  15742  fsumlt  15743  o1fsum  15756  supcvg  15799  expcnv  15807  geolim  15813  geolim2  15814  georeclim  15815  geo2lim  15818  mertenslem1  15827  mertens  15829  prodmolem2a  15877  efcllem  16020  ef0lem  16021  efgt0  16048  eftlub  16054  eflt  16062  sinbnd  16125  cosbnd  16126  ef01bndlem  16129  sin01gt0  16135  cos01gt0  16136  sin02gt0  16137  eirrlem  16149  rpnnen2lem11  16169  rpnnen2lem12  16170  ruclem11  16185  dvdssub2  16248  dvdsadd2b  16253  dvdsexp  16275  3dvds  16278  opoe  16310  bitsfzolem  16381  bitsinv1lem  16388  bezoutlem4  16489  dvdsgcd  16491  dvdsmulgcd  16503  bezoutr1  16516  nn0seqcvgd  16517  rpmulgcd2  16603  qredeq  16604  rpdvds  16607  prmind2  16632  divdenle  16696  hashdvds  16722  phimullem  16726  eulerthlem2  16729  prmdiveq  16733  prmdivdiv  16734  pythagtriplem4  16767  pythagtriplem10  16768  pythagtriplem19  16781  iserodd  16783  pcpre1  16790  pcadd2  16838  qexpz  16849  expnprm  16850  oddprmdvds  16851  pockthlem  16853  prmreclem2  16865  prmreclem3  16866  4sqlem7  16892  4sqlem10  16895  4sqlem11  16903  4sqlem12  16904  4sqlem14  16906  4sqlem15  16907  4sqlem16  16908  0ram  16968  ffthiso  17874  latmlej12  18421  qusgrp  19101  pgpfi1  19510  sylow1lem4  19516  sylow1lem5  19517  odcau  19519  pgpfi  19520  pgpssslw  19529  sylow3lem4  19545  sylow3lem6  19547  efgsfo  19654  frgp0  19675  odadd1  19763  odadd2  19764  odadd  19765  gexexlem  19767  lt6abl  19810  gsumzsubmcl  19833  pwsgsum  19897  dprd2dlem1  19958  dprd2d2  19961  ablfacrplem  19982  ablfacrp  19983  ablfacrp2  19984  ablfac1b  19987  ablfac1eu  19990  pgpfac1lem3a  19993  ablfaclem2  20003  dvdsrid  20288  dvdsrtr  20289  dvdsrneg  20291  unitmulcl  20301  unitgrp  20304  unitnegcl  20318  subrguss  20508  subrgunit  20511  isdrng2  20664  fidomndrnglem  20693  abvsubtri  20748  orngsqr  20787  ornglmulle  20788  orngrmulle  20789  orng0le1  20795  gzrngunit  21376  prmirredlem  21415  znidomb  21504  frlmgsum  21715  psrbaglesupp  21865  psdmul  22087  psdmvr  22090  invrvald  22597  psmetsym  24232  psmettri  24233  mettri2  24263  xmetsym  24269  xmettri  24273  prdsxmetlem  24290  xblss2ps  24323  xblss2  24324  blhalf  24327  xmsge0  24385  ngptgp  24558  nrginvrcnlem  24613  nmoeq0  24658  cnmet  24693  blcvx  24720  opnreen  24754  metdcnlem  24759  metdstri  24774  metdsle  24775  metnrmlem1  24782  metnrmlem3  24784  lebnumlem1  24894  pi1inv  24986  cphnmf  25129  ipge0  25132  ipcau2  25168  tcphcphlem1  25169  csbren  25333  minveclem2  25360  minveclem3  25363  ovolssnul  25422  ovolctb  25425  ovolunnul  25435  ovoliunlem1  25437  ovoliun2  25441  ovoliunnul  25442  ioombl1lem4  25496  uniioombllem3  25520  uniioombllem4  25521  uniioombllem5  25522  uniioombl  25524  volcn  25541  vitalilem2  25544  vitalilem5  25547  itg1lea  25647  mbfi1fseqlem6  25655  mbfi1flimlem  25657  itg2eqa  25680  itg2splitlem  25683  itg2split  25684  itg2monolem1  25685  itg2cnlem2  25697  iblabsr  25765  iblmulc2  25766  bddiblnc  25777  dveflem  25917  dvef  25918  dvferm2lem  25924  dvlip  25932  c1liplem1  25935  dveq0  25939  dvlt0  25944  dvivthlem1  25947  lhop1  25953  dvfsumle  25960  dvfsumleOLD  25961  dvfsumlem4  25970  dvfsumrlim3  25974  dvfsum2  25975  ftc1a  25978  ftc1lem4  25980  deg1add  26042  ply1divex  26076  ply1rem  26105  fta1glem2  26108  fta1blem  26110  ig1pdvds  26119  plyeq0lem  26149  dgrcolem2  26214  plydivlem4  26238  plyrem  26247  fta1lem  26249  aalioulem3  26276  aaliou2b  26283  aaliou3lem3  26286  aaliou3lem8  26287  ulmcn  26342  ulmdvlem1  26343  itgulm  26351  pserulm  26365  pserdvlem2  26372  abelthlem2  26376  abelthlem5  26379  abelthlem6  26380  abelthlem7  26382  abelthlem8  26383  abelthlem9  26384  sinq12gt0  26450  sinq34lt0t  26452  cosq14gt0  26453  cosq14ge0  26454  cos02pilt1  26469  efif1olem3  26487  argimgt0  26555  argimlt0  26556  logneg2  26558  logcnlem3  26587  logcnlem4  26588  logtayllem  26602  logtayl2  26605  cxpsqrtlem  26645  cxpsqrt  26646  cxpaddlelem  26695  abscxpbnd  26697  zrtdvds  26703  rtprmirr  26704  loglesqrt  26705  ang180lem2  26754  atanlogaddlem  26857  atanlogsublem  26859  atantan  26867  atans2  26875  atantayl  26881  leibpi  26886  log2tlbnd  26889  birthdaylem2  26896  birthdaylem3  26897  cxp2limlem  26920  jensenlem2  26932  jensen  26933  logdiflbnd  26939  emcllem2  26941  emcllem4  26943  harmonicbnd4  26955  fsumharmonic  26956  lgamgulmlem2  26974  lgamgulm2  26980  lgambdd  26981  lgamucov  26982  lgamcvglem  26984  lgamcvg2  26999  gamcvg  27000  wilthlem3  27014  basellem1  27025  basellem3  27027  basellem4  27028  fsumdvdsdiaglem  27127  dvdsppwf1o  27130  mpodvdsmulf1o  27138  dvdsmulf1o  27140  chteq0  27154  chtub  27157  chpub  27165  logfacubnd  27166  logfaclbnd  27167  logexprlim  27170  perfectlem2  27175  dchrfi  27200  bclbnd  27225  bposlem1  27229  bposlem3  27231  bposlem4  27232  bposlem6  27234  lgslem1  27242  lgsqrlem2  27292  lgsqrlem4  27294  lgseisenlem2  27321  lgsquadlem1  27325  lgsquadlem2  27326  lgsquad2lem1  27329  2sqlem3  27365  2sqlem4  27366  2sqlem8  27371  2sqlem11  27374  2sqcoprm  27380  2sqmod  27381  chebbnd1lem2  27415  chebbnd1lem3  27416  chtppilimlem1  27418  chpchtlim  27424  vmadivsum  27427  vmadivsumb  27428  rpvmasumlem  27432  dchrisumlem2  27435  dchrmusum2  27439  dchrvmasumlem2  27443  dchrvmasumlem3  27444  dchrisum0flblem2  27454  dchrisum0fno1  27456  dchrisum0re  27458  dchrisum0lem1  27461  dchrisum0lem2a  27462  mudivsum  27475  mulogsumlem  27476  mulog2sumlem2  27480  vmalogdivsum2  27483  selberglem2  27491  selbergb  27494  selberg2b  27497  logdivbnd  27501  selberg3lem1  27502  selberg3lem2  27503  selberg4lem1  27505  pntrmax  27509  pntrlog2bndlem2  27523  pntrlog2bndlem3  27524  pntrlog2bndlem5  27526  pntrlog2bndlem6a  27527  pntrlog2bndlem6  27528  pntrlog2bnd  27529  pntpbnd1a  27530  pntpbnd1  27531  pntpbnd2  27532  pntibndlem1  27534  pntibndlem2  27536  pntlemb  27542  pntlemq  27546  pntlemr  27547  pntlemj  27548  pntlemk  27551  qabvle  27570  padicabvcxp  27577  ostth2lem2  27579  ostth2lem3  27580  ostth2lem4  27581  ostth3  27583  addsuniflem  27949  negsid  27988  negsunif  28002  mulsuniflem  28093  sltmul2  28115  precsexlem9  28158  absmuls  28187  zscut  28336  addhalfcut  28383  zs12ge0  28396  legtrid  28572  legov3  28579  krippenlem  28671  mideulem2  28715  midex  28718  opphllem5  28732  opphllem6  28733  opphl  28735  lmieu  28765  lmiisolem  28777  ttgcontlem1  28866  colinearalglem4  28890  axpaschlem  28921  axcontlem7  28951  nbfusgrlevtxm2  29359  clwlksndivn  30066  eucrct2eupth  30225  nvge0  30653  smcnlem  30677  nmoub3i  30753  nmoub2i  30754  nmlno0lem  30773  minvecolem2  30855  htthlem  30897  norm3dif2  31131  bcs2  31162  chscllem2  31618  eigposi  31816  nmopub2tALT  31889  nmfnleub2  31906  nmlnop0iALT  31975  riesz1  32045  cnlnadjlem2  32048  nmopcoadji  32081  leopsq  32109  leopmul  32114  leopnmid  32118  nmopleid  32119  opsqrlem6  32125  0leopj  32166  hstle1  32206  strlem3a  32232  mdslmd4i  32313  cvexchlem  32348  cdj1i  32413  unidifsnel  32515  unidifsnne  32516  le2halvesd  32730  xlt2addrd  32733  fsumub  32804  sgnmulsgp  32819  2exple2exp  32821  oexpled  32823  wrdt2ind  32926  xrge0tsmsd  33046  fzto1st1  33075  cycpmco2lem4  33102  cycpmco2lem6  33104  cyc3conja  33130  archiabllem1a  33161  archiabllem2a  33164  archiabllem2c  33165  rprmdvdsprod  33499  1arithidomlem1  33500  1arithidomlem2  33501  1arithidom  33502  ply1dg3rt0irred  33545  exsslsb  33586  fedgmullem1  33619  fedgmullem2  33620  fldsdrgfldext2  33652  fldextrspundgdvdslem  33669  fldextrspundgdvds  33670  fldext2rspun  33671  algextdeglem8  33708  rtelextdg2lem  33710  constrext2chnlem  33734  cos9thpiminplylem1  33766  cos9thpiminplylem2  33767  metideq  33877  metider  33878  sqsscirc1  33892  esummono  34038  esumpad2  34040  esumle  34042  esumlef  34046  esumcst  34047  esumrnmpt2  34052  esum2d  34077  aean  34228  dya2ub  34255  dya2icoseg  34262  omssubadd  34285  inelcarsg  34296  carsgsigalem  34300  carsggect  34303  carsgclctunlem2  34304  eulerpartlemb  34353  fibp1  34386  signsplypnf  34535  signsply0  34536  fdvposlt  34584  fdvposle  34586  reprgt  34606  logdivsqrle  34635  hgt750lemb  34641  hgt750leme  34643  tgoldbachgtde  34645  subfacval3  35170  sconnpht2  35219  sconnpi1  35220  resconn  35227  snmlff  35310  sinccvglem  35653  faclimlem2  35725  btwnouttr2  36004  weiunpo  36447  dnibndlem5  36464  dnibndlem7  36466  dnibndlem8  36467  dnibndlem9  36468  dnibndlem10  36469  dnibnd  36473  knoppcnlem4  36478  knoppcnlem9  36483  unbdqndv2lem1  36491  unbdqndv2lem2  36492  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem21  36514  ltflcei  37596  poimirlem9  37617  poimirlem26  37634  poimirlem27  37635  poimirlem29  37637  heicant  37643  mblfinlem2  37646  mblfinlem3  37647  mblfinlem4  37648  volsupnfl  37653  itg2addnclem  37659  itg2addnclem3  37661  iblmulc2nc  37673  ftc1cnnclem  37679  ftc1anclem6  37686  ftc1anclem7  37687  ftc1anclem8  37688  ftc2nc  37690  dvasin  37692  geomcau  37747  bfplem2  37811  rrncmslem  37820  rrnequiv  37823  lsatcvatlem  39036  islshpcv  39040  atlatmstc  39306  cvlsupr7  39335  cvrval3  39401  cvrval5  39403  cvrexchlem  39407  atcvrj1  39419  cvrat3  39430  cvrat4  39431  atbtwn  39434  1cvratex  39461  hlatexch4  39469  3atlem1  39471  3atlem2  39472  atcvrlln2  39507  atcvrlln  39508  lplnllnneN  39544  llncvrlpln2  39545  4atlem3b  39586  lplncvrlvol2  39603  dalemswapyz  39644  dalemswapyzps  39678  dalem25  39686  dalem39  39699  dalem58  39718  dalem59  39719  lneq2at  39766  lncvrat  39770  dalawlem2  39860  dalawlem3  39861  dalawlem4  39862  dalawlem6  39864  dalawlem9  39867  dalawlem11  39869  dalawlem12  39870  lhpocnle  40004  lhpmcvr3  40013  lhpmcvr5N  40015  lhpmcvr6N  40016  4atexlemunv  40054  4atexlemc  40057  4atexlemex2  40059  lautm  40082  cdlemc2  40180  cdleme5  40228  cdleme11j  40255  cdleme16b  40267  cdlemednpq  40287  cdleme19e  40295  cdleme20i  40305  cdleme22a  40328  cdleme22cN  40330  cdleme22d  40331  cdleme22e  40332  cdleme22eALTN  40333  cdleme22f  40334  cdleme23c  40339  cdleme30a  40366  cdleme35a  40436  cdleme35b  40438  cdleme42h  40470  cdlemeg46rgv  40516  cdlemg8b  40616  cdlemg12e  40635  cdlemg13a  40639  cdlemg17pq  40660  cdlemg18c  40668  cdlemg19  40672  cdlemg21  40674  cdlemg31d  40688  cdlemg33a  40694  tendoid  40761  cdlemk4  40822  cdlemki  40829  cdlemk10  40831  cdlemksv2  40835  cdlemk12  40838  cdlemk14  40842  cdlemk15  40843  cdlemk1u  40847  cdlemk5u  40849  cdlemk12u  40860  cdlemk45  40935  cdlemk48  40938  dia2dimlem1  41052  dia2dimlem2  41053  dia2dimlem3  41054  cdlemm10N  41106  cdlemn2  41183  dihjustlem  41204  dihglbcpreN  41288  dihmeetlem3N  41293  nnproddivdvdsd  41982  lcmineqlem17  42027  lcmineqlem18  42028  3lexlogpow2ineq1  42040  3lexlogpow2ineq2  42041  3lexlogpow5ineq5  42042  aks4d1p1p3  42051  aks4d1p1p2  42052  aks4d1p1p4  42053  aks4d1p1p5  42057  aks4d1p1  42058  aks4d1p3  42060  aks4d1p8  42069  posbezout  42082  primrootspoweq0  42088  aks6d1c1  42098  hashscontpow1  42103  aks6d1c4  42106  aks6d1c2  42112  aks6d1c5lem1  42118  aks6d1c5lem3  42119  aks6d1c5lem2  42120  deg1gprod  42122  sticksstones7  42134  sticksstones10  42137  sticksstones12  42140  sticksstones22  42150  aks6d1c6lem1  42152  aks6d1c6lem3  42154  aks6d1c6lem4  42155  bcled  42160  bcle2d  42161  aks6d1c7lem1  42162  unitscyglem4  42180  aks5lem7  42182  aks5  42186  explt1d  42305  mulgt0b2d  42460  evlselv  42569  dffltz  42616  fltdvdsabdvdsc  42620  fltaccoprm  42622  fltabcoprm  42624  flt4lem5elem  42633  flt4lem7  42641  fltnlta  42645  irrapxlem1  42804  pell1qrgaplem  42855  pell1qrgap  42856  monotoddzzfi  42925  jm2.24nn  42942  congtr  42948  congmul  42950  congsub  42953  fzmaxdif  42964  acongeq  42966  jm2.20nn  42980  jm2.25  42982  hbtlem4  43109  dgrsub2  43118  mpaaeu  43133  idomsubgmo  43176  iscard4  43516  sqrtcvallem4  43622  leeq2d  44141  int-sqgeq0d  44169  int-ineqmvtd  44174  cvgdvgrat  44296  radcnvrat  44297  hashnzfzclim  44305  dvconstbi  44317  binomcxplemdvbinom  44336  isosctrlem1ALT  44917  mulltgt0  45010  rnmptbd2lem  45236  oddfl  45270  2timesgt  45280  lt3addmuld  45293  lt4addmuld  45298  supxrgere  45323  supxrgelem  45327  supxrge  45328  xadd0ge2  45331  infrpge  45341  xrlexaddrp  45342  xralrple2  45344  infxr  45357  infleinflem1  45360  infleinflem2  45361  infleinf  45362  xralrple4  45363  xralrple3  45364  recnnltrp  45367  rpgtrecnn  45370  xrralrecnnge  45380  rexabslelem  45408  infrnmptle  45413  supminfxr  45454  xrpnf  45475  iccshift  45510  iooshift  45514  ressiocsup  45546  ressioosup  45547  fsumnncl  45564  fmul01  45572  fmul01lt1lem1  45576  fmul01lt1lem2  45577  mccllem  45589  climrec  45595  climexp  45597  climneg  45602  limcrecl  45621  sumnnodd  45622  lptioo2  45623  lptioo1  45624  ltmod  45630  lptre2pt  45632  0ellimcdiv  45641  limclner  45643  fnlimcnv  45659  climinf2lem  45698  limsupubuzlem  45704  limsup10exlem  45764  limsupgtlem  45769  dfxlim2v  45839  xlimliminflimsup  45854  cncficcgt0  45880  cncfioobdlem  45888  ioodvbdlimc1lem1  45923  ioodvbdlimc1lem2  45924  ioodvbdlimc2lem  45926  dvdsn1add  45931  dvnxpaek  45934  dvnmul  45935  dvnprodlem1  45938  itgiccshift  45972  itgperiod  45973  sublevolico  45976  ismbl3  45978  ovolsplit  45980  ismbl4  45985  stoweidlem1  45993  stoweidlem11  46003  stoweidlem13  46005  stoweidlem26  46018  stoweidlem34  46026  stoweidlem38  46030  stoweidlem42  46034  stoweidlem51  46043  stoweidlem59  46051  stirlinglem5  46070  stirlinglem6  46071  stirlinglem7  46072  stirlinglem10  46075  stirlinglem11  46076  stirlinglem13  46078  stirlinglem15  46080  dirkercncflem1  46095  dirkercncflem4  46098  fourierdlem4  46103  fourierdlem10  46109  fourierdlem11  46110  fourierdlem15  46114  fourierdlem20  46119  fourierdlem25  46124  fourierdlem26  46125  fourierdlem30  46129  fourierdlem37  46136  fourierdlem39  46138  fourierdlem40  46139  fourierdlem41  46140  fourierdlem42  46141  fourierdlem44  46143  fourierdlem47  46145  fourierdlem48  46146  fourierdlem49  46147  fourierdlem50  46148  fourierdlem51  46149  fourierdlem52  46150  fourierdlem54  46152  fourierdlem60  46158  fourierdlem61  46159  fourierdlem63  46161  fourierdlem64  46162  fourierdlem65  46163  fourierdlem73  46171  fourierdlem74  46172  fourierdlem75  46173  fourierdlem76  46174  fourierdlem78  46176  fourierdlem79  46177  fourierdlem81  46179  fourierdlem84  46182  fourierdlem87  46185  fourierdlem92  46190  fourierdlem93  46191  fourierdlem101  46199  fourierdlem102  46200  fourierdlem103  46201  fourierdlem104  46202  fourierdlem111  46209  fourierdlem114  46212  sqwvfoura  46220  sqwvfourb  46221  fouriersw  46223  etransclem19  46245  etransclem23  46249  etransclem24  46250  etransclem25  46251  etransclem27  46253  etransclem32  46258  etransclem35  46261  etransclem48  46274  qndenserrnbllem  46286  ioorrnopnlem  46296  ioorrnopnxrlem  46298  fsumlesge0  46369  sge0cl  46373  sge0supre  46381  sge0less  46384  sge0gerp  46387  sge0ltfirp  46392  sge0le  46399  sge0ltfirpmpt  46400  sge0split  46401  sge0rpcpnf  46413  sge0ltfirpmpt2  46418  sge0isum  46419  sge0xaddlem1  46425  sge0pnffigtmpt  46432  sge0pnffsumgt  46434  sge0gtfsumgt  46435  sge0seq  46438  nnfoctbdjlem  46447  meassle  46455  meaiuninclem  46472  meaiininclem  46478  omeiunle  46509  omeiunltfirp  46511  carageniuncllem2  46514  carageniuncl  46515  omess0  46526  hoicvr  46540  ovnlerp  46554  ovnsubaddlem1  46562  hsphoidmvle2  46577  hoidmv1lelem2  46584  hoidmv1le  46586  hoidmvlelem1  46587  hoidmvlelem2  46588  hoidmvlelem3  46589  hoidmvlelem5  46591  ovnhoilem2  46594  ovnhoi  46595  hoidifhspdmvle  46612  hoiqssbllem2  46615  hspmbllem2  46619  hspmbllem3  46620  hspmbl  46621  vonioolem2  46673  vonicclem2  46676  smfaddlem1  46755  smflimlem2  46764  smflimlem4  46766  smfmullem1  46783  smfinflem  46809  smflimsuplem4  46815  smflimsuplem8  46819  perfectALTVlem2  47717  nnpw2blen  48563  itscnhlinecirc02plem1  48765  funcoppc3  49130  oppcuprcl2  49185  isinito3  49483