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 231	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1534   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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5144

This theorem is referenced by:  breqtrrd  5171  breqtrid  5180  domunsn  9154  mapdom2  9175  phplem2  9232  phplem4OLD  9244  mapfien2  9442  wemaplem2  9580  infdifsn  9690  cantnff  9707  ttrclss  9753  rnttrcl  9755  infxpenlem  10046  infmap2  10249  ssfin4  10341  canthp1lem1  10683  nqereq  10966  ltexnq  11006  ltbtwnnq  11009  add20  11764  mullt0  11771  ltm1  12098  recgt0  12102  prodgt0  12103  ltmul1a  12105  mulge0b  12127  recp1lt1  12155  recreclt  12156  ledivp1  12159  ledivp1i  12182  ltdivp1i  12183  eluzmn  12872  ltaddrp2d  13095  mul2lt0bi  13125  prodge0rd  13126  xleadd1a  13277  xov1plusxeqvd  13520  fz01en  13574  fzonmapblen  13723  fladdz  13836  flhalf  13841  fldiv  13871  modsubdir  13951  fzen2  13980  serle  14068  ltexp2a  14176  leexp2a  14182  exple1  14186  expubnd  14187  bernneq  14238  expmulnbnd  14244  discr1  14248  discr  14249  faclbnd6  14308  hashfz  14436  hashfun  14446  seqcoll  14475  sqeqd  15163  01sqrexlem7  15245  sqrtge0  15254  sqrtneglem  15263  abslt  15311  absle  15312  abstri  15327  rlimge0  15575  reccn2  15591  climaddc2  15630  isercolllem1  15661  caucvgrlem  15669  summolem2a  15711  isumge0  15762  fsumle  15795  fsumlt  15796  o1fsum  15809  supcvg  15852  expcnv  15860  geolim  15866  geolim2  15867  georeclim  15868  geo2lim  15871  mertenslem1  15880  mertens  15882  prodmolem2a  15928  efcllem  16071  ef0lem  16072  efgt0  16097  eftlub  16103  eflt  16111  sinbnd  16174  cosbnd  16175  ef01bndlem  16178  sin01gt0  16184  cos01gt0  16185  sin02gt0  16186  eirrlem  16198  rpnnen2lem11  16218  rpnnen2lem12  16219  ruclem11  16234  dvdssub2  16295  dvdsadd2b  16300  dvdsexp  16322  3dvds  16325  opoe  16357  bitsfzolem  16426  bitsinv1lem  16433  bezoutlem4  16535  dvdsgcd  16537  dvdsmulgcd  16549  bezoutr1  16562  nn0seqcvgd  16563  rpmulgcd2  16649  qredeq  16650  rpdvds  16653  prmind2  16678  divdenle  16743  hashdvds  16769  phimullem  16773  eulerthlem2  16776  prmdiveq  16780  prmdivdiv  16781  pythagtriplem4  16813  pythagtriplem10  16814  pythagtriplem19  16827  iserodd  16829  pcpre1  16836  pcadd2  16884  qexpz  16895  expnprm  16896  oddprmdvds  16897  pockthlem  16899  prmreclem2  16911  prmreclem3  16912  4sqlem7  16938  4sqlem10  16941  4sqlem11  16949  4sqlem12  16950  4sqlem14  16952  4sqlem15  16953  4sqlem16  16954  0ram  17014  ffthiso  17943  latmlej12  18496  qusgrp  19173  pgpfi1  19586  sylow1lem4  19592  sylow1lem5  19593  odcau  19595  pgpfi  19596  pgpssslw  19605  sylow3lem4  19621  sylow3lem6  19623  efgsfo  19730  frgp0  19751  odadd1  19839  odadd2  19840  odadd  19841  gexexlem  19843  lt6abl  19886  gsumzsubmcl  19909  pwsgsum  19973  dprd2dlem1  20034  dprd2d2  20037  ablfacrplem  20058  ablfacrp  20059  ablfacrp2  20060  ablfac1b  20063  ablfac1eu  20066  pgpfac1lem3a  20069  ablfaclem2  20079  dvdsrid  20342  dvdsrtr  20343  dvdsrneg  20345  unitmulcl  20355  unitgrp  20358  unitnegcl  20372  subrguss  20564  subrgunit  20567  isdrng2  20714  fidomndrnglem  20744  abvsubtri  20799  gzrngunit  21423  prmirredlem  21455  znidomb  21552  frlmgsum  21763  psrbaglesupp  21914  psrbaglesuppOLD  21915  psdmul  22153  invrvald  22663  psmetsym  24301  psmettri  24302  mettri2  24332  xmetsym  24338  xmettri  24342  prdsxmetlem  24359  xblss2ps  24392  xblss2  24393  blhalf  24396  xmsge0  24454  ngptgp  24630  nrginvrcnlem  24693  nmoeq0  24738  cnmet  24773  blcvx  24799  opnreen  24832  metdcnlem  24837  metdstri  24852  metdsle  24853  metnrmlem1  24860  metnrmlem3  24862  lebnumlem1  24972  pi1inv  25064  cphnmf  25208  ipge0  25211  ipcau2  25247  tcphcphlem1  25248  csbren  25412  minveclem2  25439  minveclem3  25442  ovolssnul  25501  ovolctb  25504  ovolunnul  25514  ovoliunlem1  25516  ovoliun2  25520  ovoliunnul  25521  ioombl1lem4  25575  uniioombllem3  25599  uniioombllem4  25600  uniioombllem5  25601  uniioombl  25603  volcn  25620  vitalilem2  25623  vitalilem5  25626  itg1lea  25727  mbfi1fseqlem6  25735  mbfi1flimlem  25737  itg2eqa  25760  itg2splitlem  25763  itg2split  25764  itg2monolem1  25765  itg2cnlem2  25777  iblabsr  25844  iblmulc2  25845  bddiblnc  25856  dveflem  25996  dvef  25997  dvferm2lem  26003  dvlip  26011  c1liplem1  26014  dveq0  26018  dvlt0  26023  dvivthlem1  26026  lhop1  26032  dvfsumle  26039  dvfsumleOLD  26040  dvfsumlem4  26049  dvfsumrlim3  26053  dvfsum2  26054  ftc1a  26057  ftc1lem4  26059  deg1add  26124  ply1divex  26158  ply1rem  26187  fta1glem2  26190  fta1blem  26192  ig1pdvds  26201  plyeq0lem  26231  dgrcolem2  26296  plydivlem4  26318  plyrem  26327  fta1lem  26329  aalioulem3  26356  aaliou2b  26363  aaliou3lem3  26366  aaliou3lem8  26367  ulmcn  26422  ulmdvlem1  26423  itgulm  26431  pserulm  26445  pserdvlem2  26452  abelthlem2  26456  abelthlem5  26459  abelthlem6  26460  abelthlem7  26462  abelthlem8  26463  abelthlem9  26464  sinq12gt0  26529  sinq34lt0t  26531  cosq14gt0  26532  cosq14ge0  26533  cos02pilt1  26547  efif1olem3  26565  argimgt0  26633  argimlt0  26634  logneg2  26636  logcnlem3  26665  logcnlem4  26666  logtayllem  26680  logtayl2  26683  cxpsqrtlem  26723  cxpsqrt  26724  cxpaddlelem  26773  abscxpbnd  26775  zrtdvds  26781  rtprmirr  26782  loglesqrt  26783  ang180lem2  26832  atanlogaddlem  26935  atanlogsublem  26937  atantan  26945  atans2  26953  atantayl  26959  leibpi  26964  log2tlbnd  26967  birthdaylem2  26974  birthdaylem3  26975  cxp2limlem  26998  jensenlem2  27010  jensen  27011  logdiflbnd  27017  emcllem2  27019  emcllem4  27021  harmonicbnd4  27033  fsumharmonic  27034  lgamgulmlem2  27052  lgamgulm2  27058  lgambdd  27059  lgamucov  27060  lgamcvglem  27062  lgamcvg2  27077  gamcvg  27078  wilthlem3  27092  basellem1  27103  basellem3  27105  basellem4  27106  fsumdvdsdiaglem  27205  dvdsppwf1o  27208  mpodvdsmulf1o  27216  dvdsmulf1o  27218  chteq0  27232  chtub  27235  chpub  27243  logfacubnd  27244  logfaclbnd  27245  logexprlim  27248  perfectlem2  27253  dchrfi  27278  bclbnd  27303  bposlem1  27307  bposlem3  27309  bposlem4  27310  bposlem6  27312  lgslem1  27320  lgsqrlem2  27370  lgsqrlem4  27372  lgseisenlem2  27399  lgsquadlem1  27403  lgsquadlem2  27404  lgsquad2lem1  27407  2sqlem3  27443  2sqlem4  27444  2sqlem8  27449  2sqlem11  27452  2sqcoprm  27458  2sqmod  27459  chebbnd1lem2  27493  chebbnd1lem3  27494  chtppilimlem1  27496  chpchtlim  27502  vmadivsum  27505  vmadivsumb  27506  rpvmasumlem  27510  dchrisumlem2  27513  dchrmusum2  27517  dchrvmasumlem2  27521  dchrvmasumlem3  27522  dchrisum0flblem2  27532  dchrisum0fno1  27534  dchrisum0re  27536  dchrisum0lem1  27539  dchrisum0lem2a  27540  mudivsum  27553  mulogsumlem  27554  mulog2sumlem2  27558  vmalogdivsum2  27561  selberglem2  27569  selbergb  27572  selberg2b  27575  logdivbnd  27579  selberg3lem1  27580  selberg3lem2  27581  selberg4lem1  27583  pntrmax  27587  pntrlog2bndlem2  27601  pntrlog2bndlem3  27602  pntrlog2bndlem5  27604  pntrlog2bndlem6a  27605  pntrlog2bndlem6  27606  pntrlog2bnd  27607  pntpbnd1a  27608  pntpbnd1  27609  pntpbnd2  27610  pntibndlem1  27612  pntibndlem2  27614  pntlemb  27620  pntlemq  27624  pntlemr  27625  pntlemj  27626  pntlemk  27629  qabvle  27648  padicabvcxp  27655  ostth2lem2  27657  ostth2lem3  27658  ostth2lem4  27659  ostth3  27661  addsuniflem  28009  negsid  28044  negsunif  28058  mulsuniflem  28144  sltmul2  28166  precsexlem9  28208  absmuls  28233  legtrid  28512  legov3  28519  krippenlem  28611  mideulem2  28655  midex  28658  opphllem5  28672  opphllem6  28673  opphl  28675  lmieu  28705  lmiisolem  28717  ttgcontlem1  28812  colinearalglem4  28837  axpaschlem  28868  axcontlem7  28898  nbfusgrlevtxm2  29308  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  32458  unidifsnne  32459  le2halvesd  32659  xlt2addrd  32662  fsumub  32729  wrdt2ind  32817  xrge0tsmsd  32927  fzto1st1  32981  cycpmco2lem4  33008  cycpmco2lem6  33010  cyc3conja  33036  archiabllem1a  33057  archiabllem2a  33060  archiabllem2c  33061  orngsqr  33184  ornglmulle  33185  orngrmulle  33186  orng0le1  33192  rprmdvdsprod  33412  1arithidomlem1  33413  1arithidomlem2  33414  1arithidom  33415  ply1dg3rt0irred  33457  fedgmullem1  33527  fedgmullem2  33528  algextdeglem8  33594  rtelextdg2lem  33596  metideq  33718  metider  33719  sqsscirc1  33733  esummono  33897  esumpad2  33899  esumle  33901  esumlef  33905  esumcst  33906  esumrnmpt2  33911  esum2d  33936  aean  34087  dya2ub  34114  dya2icoseg  34121  omssubadd  34144  inelcarsg  34155  carsgsigalem  34159  carsggect  34162  carsgclctunlem2  34163  eulerpartlemb  34212  fibp1  34245  sgnmulsgp  34394  signsplypnf  34406  signsply0  34407  fdvposlt  34455  fdvposle  34457  reprgt  34477  logdivsqrle  34506  hgt750lemb  34512  hgt750leme  34514  tgoldbachgtde  34516  subfacval3  35027  sconnpht2  35076  sconnpi1  35077  resconn  35084  snmlff  35167  sinccvglem  35510  faclimlem2  35576  btwnouttr2  35856  dnibndlem5  36195  dnibndlem7  36197  dnibndlem8  36198  dnibndlem9  36199  dnibndlem10  36200  dnibnd  36204  knoppcnlem4  36209  knoppcnlem9  36214  unbdqndv2lem1  36222  unbdqndv2lem2  36223  knoppndvlem11  36235  knoppndvlem12  36236  knoppndvlem14  36238  knoppndvlem15  36239  knoppndvlem17  36241  knoppndvlem18  36242  knoppndvlem19  36243  knoppndvlem21  36245  ltflcei  37319  poimirlem9  37340  poimirlem26  37357  poimirlem27  37358  poimirlem29  37360  heicant  37366  mblfinlem2  37369  mblfinlem3  37370  mblfinlem4  37371  volsupnfl  37376  itg2addnclem  37382  itg2addnclem3  37384  iblmulc2nc  37396  ftc1cnnclem  37402  ftc1anclem6  37409  ftc1anclem7  37410  ftc1anclem8  37411  ftc2nc  37413  dvasin  37415  geomcau  37470  bfplem2  37534  rrncmslem  37543  rrnequiv  37546  lsatcvatlem  38757  islshpcv  38761  atlatmstc  39027  cvlsupr7  39056  cvrval3  39122  cvrval5  39124  cvrexchlem  39128  atcvrj1  39140  cvrat3  39151  cvrat4  39152  atbtwn  39155  1cvratex  39182  hlatexch4  39190  3atlem1  39192  3atlem2  39193  atcvrlln2  39228  atcvrlln  39229  lplnllnneN  39265  llncvrlpln2  39266  4atlem3b  39307  lplncvrlvol2  39324  dalemswapyz  39365  dalemswapyzps  39399  dalem25  39407  dalem39  39420  dalem58  39439  dalem59  39440  lneq2at  39487  lncvrat  39491  dalawlem2  39581  dalawlem3  39582  dalawlem4  39583  dalawlem6  39585  dalawlem9  39588  dalawlem11  39590  dalawlem12  39591  lhpocnle  39725  lhpmcvr3  39734  lhpmcvr5N  39736  lhpmcvr6N  39737  4atexlemunv  39775  4atexlemc  39778  4atexlemex2  39780  lautm  39803  cdlemc2  39901  cdleme5  39949  cdleme11j  39976  cdleme16b  39988  cdlemednpq  40008  cdleme19e  40016  cdleme20i  40026  cdleme22a  40049  cdleme22cN  40051  cdleme22d  40052  cdleme22e  40053  cdleme22eALTN  40054  cdleme22f  40055  cdleme23c  40060  cdleme30a  40087  cdleme35a  40157  cdleme35b  40159  cdleme42h  40191  cdlemeg46rgv  40237  cdlemg8b  40337  cdlemg12e  40356  cdlemg13a  40360  cdlemg17pq  40381  cdlemg18c  40389  cdlemg19  40393  cdlemg21  40395  cdlemg31d  40409  cdlemg33a  40415  tendoid  40482  cdlemk4  40543  cdlemki  40550  cdlemk10  40552  cdlemksv2  40556  cdlemk12  40559  cdlemk14  40563  cdlemk15  40564  cdlemk1u  40568  cdlemk5u  40570  cdlemk12u  40581  cdlemk45  40656  cdlemk48  40659  dia2dimlem1  40773  dia2dimlem2  40774  dia2dimlem3  40775  cdlemm10N  40827  cdlemn2  40904  dihjustlem  40925  dihglbcpreN  41009  dihmeetlem3N  41014  nnproddivdvdsd  41709  lcmineqlem17  41754  lcmineqlem18  41755  3lexlogpow2ineq1  41767  3lexlogpow2ineq2  41768  3lexlogpow5ineq5  41769  aks4d1p1p3  41778  aks4d1p1p2  41779  aks4d1p1p4  41780  aks4d1p1p5  41784  aks4d1p1  41785  aks4d1p3  41787  aks4d1p8  41796  posbezout  41809  primrootspoweq0  41815  aks6d1c1  41825  hashscontpow1  41830  aks6d1c4  41833  aks6d1c2  41839  aks6d1c5lem1  41845  aks6d1c5lem3  41846  aks6d1c5lem2  41847  deg1gprod  41849  sticksstones7  41861  sticksstones10  41864  sticksstones12  41867  sticksstones22  41877  aks6d1c6lem1  41879  aks6d1c6lem3  41881  aks6d1c6lem4  41882  bcled  41887  bcle2d  41888  aks6d1c7lem1  41889  unitscyglem4  41907  2xp3dxp2ge1d  41946  factwoffsmonot  41947  explt1d  42046  evlselv  42274  dffltz  42321  fltdvdsabdvdsc  42325  fltaccoprm  42327  fltabcoprm  42329  flt4lem5elem  42338  flt4lem7  42346  fltnlta  42350  irrapxlem1  42513  pell1qrgaplem  42564  pell1qrgap  42565  monotoddzzfi  42634  jm2.24nn  42651  congtr  42657  congmul  42659  congsub  42662  fzmaxdif  42673  acongeq  42675  jm2.20nn  42689  jm2.25  42691  hbtlem4  42821  dgrsub2  42830  mpaaeu  42845  idomsubgmo  42892  iscard4  43234  sqrtcvallem4  43340  leeq2d  43859  int-sqgeq0d  43887  int-ineqmvtd  43892  cvgdvgrat  44021  radcnvrat  44022  hashnzfzclim  44030  dvconstbi  44042  binomcxplemdvbinom  44061  isosctrlem1ALT  44644  mulltgt0  44655  rnmptbd2lem  44890  oddfl  44925  2timesgt  44936  lt3addmuld  44949  lt4addmuld  44954  supxrgere  44981  supxrgelem  44985  supxrge  44986  xadd0ge2  44989  infrpge  44999  xrlexaddrp  45000  xralrple2  45002  infxr  45015  infleinflem1  45018  infleinflem2  45019  infleinf  45020  xralrple4  45021  xralrple3  45022  recnnltrp  45025  rpgtrecnn  45028  xrralrecnnge  45038  rexabslelem  45066  infrnmptle  45071  supminfxr  45112  xrpnf  45134  iccshift  45169  iooshift  45173  ressiocsup  45205  ressioosup  45206  fsumnncl  45226  fmul01  45234  fmul01lt1lem1  45238  fmul01lt1lem2  45239  mccllem  45251  climrec  45257  climexp  45259  climneg  45264  limcrecl  45283  sumnnodd  45284  lptioo2  45285  lptioo1  45286  ltmod  45292  lptre2pt  45294  0ellimcdiv  45303  limclner  45305  fnlimcnv  45321  climinf2lem  45360  limsupubuzlem  45366  limsup10exlem  45426  limsupgtlem  45431  dfxlim2v  45501  xlimliminflimsup  45516  cncficcgt0  45542  cncfioobdlem  45550  ioodvbdlimc1lem1  45585  ioodvbdlimc1lem2  45586  ioodvbdlimc2lem  45588  dvdsn1add  45593  dvnxpaek  45596  dvnmul  45597  dvnprodlem1  45600  itgiccshift  45634  itgperiod  45635  sublevolico  45638  ismbl3  45640  ovolsplit  45642  ismbl4  45647  stoweidlem1  45655  stoweidlem11  45665  stoweidlem13  45667  stoweidlem26  45680  stoweidlem34  45688  stoweidlem38  45692  stoweidlem42  45696  stoweidlem51  45705  stoweidlem59  45713  stirlinglem5  45732  stirlinglem6  45733  stirlinglem7  45734  stirlinglem10  45737  stirlinglem11  45738  stirlinglem13  45740  stirlinglem15  45742  dirkercncflem1  45757  dirkercncflem4  45760  fourierdlem4  45765  fourierdlem10  45771  fourierdlem11  45772  fourierdlem15  45776  fourierdlem20  45781  fourierdlem25  45786  fourierdlem26  45787  fourierdlem30  45791  fourierdlem37  45798  fourierdlem39  45800  fourierdlem40  45801  fourierdlem41  45802  fourierdlem42  45803  fourierdlem44  45805  fourierdlem47  45807  fourierdlem48  45808  fourierdlem49  45809  fourierdlem50  45810  fourierdlem51  45811  fourierdlem52  45812  fourierdlem54  45814  fourierdlem60  45820  fourierdlem61  45821  fourierdlem63  45823  fourierdlem64  45824  fourierdlem65  45825  fourierdlem73  45833  fourierdlem74  45834  fourierdlem75  45835  fourierdlem76  45836  fourierdlem78  45838  fourierdlem79  45839  fourierdlem81  45841  fourierdlem84  45844  fourierdlem87  45847  fourierdlem92  45852  fourierdlem93  45853  fourierdlem101  45861  fourierdlem102  45862  fourierdlem103  45863  fourierdlem104  45864  fourierdlem111  45871  fourierdlem114  45874  sqwvfoura  45882  sqwvfourb  45883  fouriersw  45885  etransclem19  45907  etransclem23  45911  etransclem24  45912  etransclem25  45913  etransclem27  45915  etransclem32  45920  etransclem35  45923  etransclem48  45936  qndenserrnbllem  45948  ioorrnopnlem  45958  ioorrnopnxrlem  45960  fsumlesge0  46031  sge0cl  46035  sge0supre  46043  sge0less  46046  sge0gerp  46049  sge0ltfirp  46054  sge0le  46061  sge0ltfirpmpt  46062  sge0split  46063  sge0rpcpnf  46075  sge0ltfirpmpt2  46080  sge0isum  46081  sge0xaddlem1  46087  sge0pnffigtmpt  46094  sge0pnffsumgt  46096  sge0gtfsumgt  46097  sge0seq  46100  nnfoctbdjlem  46109  meassle  46117  meaiuninclem  46134  meaiininclem  46140  omeiunle  46171  omeiunltfirp  46173  carageniuncllem2  46176  carageniuncl  46177  omess0  46188  hoicvr  46202  ovnlerp  46216  ovnsubaddlem1  46224  hsphoidmvle2  46239  hoidmv1lelem2  46246  hoidmv1le  46248  hoidmvlelem1  46249  hoidmvlelem2  46250  hoidmvlelem3  46251  hoidmvlelem5  46253  ovnhoilem2  46256  ovnhoi  46257  hoidifhspdmvle  46274  hoiqssbllem2  46277  hspmbllem2  46281  hspmbllem3  46282  hspmbl  46283  vonioolem2  46335  vonicclem2  46338  smfaddlem1  46417  smflimlem2  46426  smflimlem4  46428  smfmullem1  46445  smfinflem  46471  smflimsuplem4  46477  smflimsuplem8  46481  perfectALTVlem2  47327  nnpw2blen  48001  itscnhlinecirc02plem1  48203