Theorem syl2an 596

Description: A double syllogism inference. For an implication-only version, see syl2im 40. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2an	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 ⊢ (𝜏 → 𝜒)
2		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 593	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  syl2anr  597  anim12i  613  anim12ii  618  bi2anan9  638  syl3an132  1166  mp3an3an  1469  ax13  2374  nfeqf  2380  eqeqan12dALT  2749  sylan9eq  2785  sylan9ss  3963  ssconb  4108  ineqan12d  4188  ifpr  4660  disjtp2  4683  dfopg  4838  disjxiun  5107  breqan12d  5126  eusv1  5349  opelvvg  5682  opthprc  5705  relop  5817  dmpropg  6191  unixp  6258  tz7.7  6361  ordin  6365  onin  6366  ontri1  6369  onfr  6374  onelpss  6375  onsseleq  6376  oneltri  6378  ontr2  6383  onunel  6442  onun2  6445  funssres  6563  funtpg  6574  funtp  6576  resasplit  6733  fodmrnu  6783  f1un  6823  dffv2  6959  fvreseq0  7013  fvcofneq  7068  funopdmsn  7125  fprg  7130  fprb  7171  fconst2g  7180  isofrlem  7318  oveqan12d  7409  ov3  7555  ovg  7557  ovima0  7571  f1opw2  7647  off  7674  unexgOLD  7728  pwuncl  7749  epweon  7754  epweonALT  7755  sucexeloni  7788  ordunpr  7804  omun  7867  peano4  7871  fabexg  7917  f1oabexg  7921  fiun  7924  offres  7965  el2mpocsbcl  8067  curry1  8086  curry1val  8087  curry2  8089  curry2val  8091  soxp  8111  wexp  8112  xpord2pred  8127  poxp3  8132  poseq  8140  soseq  8141  suppfnss  8171  frrlem4  8271  frrlem11  8278  frrlem12  8279  fprlem1  8282  iunon  8311  onfununi  8313  tfrlem11  8359  tz7.48lem  8412  seqomeq12  8425  oacan  8515  oawordri  8517  oaass  8528  omord2  8534  omcan  8536  oen0  8553  oeordi  8554  oeord  8555  oecan  8556  oeworde  8560  oeordsuc  8561  oelimcl  8567  nnawordi  8588  nnaword  8594  nnmord  8599  oaabslem  8614  omabslem  8617  omsmo  8625  eldifsucnn  8631  naddcllem  8643  naddov2  8646  ertr  8689  erex  8698  brecop  8786  ecopovtrn  8796  ecovdi  8801  mapvalg  8812  pmvalg  8813  pmss12g  8845  elmapresaun  8856  boxcutc  8917  undom  9033  sbthlem7  9063  sbth  9067  sdomnsym  9072  sdomdomtr  9080  xpf1o  9109  xpen  9110  limenpsi  9122  pssnn  9138  pwssfi  9147  sbthfi  9169  php2  9178  php3  9179  phpeqd  9182  nndomog  9183  onomeneq  9184  1sdomOLD  9203  ominfOLD  9213  isinf  9214  isinfOLD  9215  fineqvlem  9216  f1finf1o  9223  en1eqsnOLD  9227  dif1ennnALT  9229  findcard3  9236  findcard3OLD  9237  unblem2  9247  isfinite2  9252  unfilem1  9261  unfi2  9266  fodomfir  9286  unifi2  9303  f1opwfi  9314  fsuppxpfi  9343  fsuppunbi  9347  fsuppco2  9361  fsuppcor  9362  fival  9370  fiin  9380  ordiso  9476  ordtypelem10  9487  hartogslem1  9502  wofib  9505  brwdom3  9542  unwdomg  9544  xpwdomg  9545  sucprcreg  9561  preleqALT  9577  inf3lem6  9593  oemapval  9643  cantnf  9653  wemapwe  9657  cnfcom  9660  ttrcltr  9676  dfttrcl2  9684  frmin  9709  r111  9735  r1ord3g  9739  prwf  9771  r1pw  9805  rankprb  9811  rankxplim  9839  tcrank  9844  updjud  9894  finnum  9908  xpnum  9911  carduni  9941  nnsdomel  9950  fidomtri  9953  pr2nelemOLD  9963  infxpenlem  9973  fseqdom  9986  onssnum  10000  acndom2  10014  alephinit  10055  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem6  10116  undjudom  10128  endjudisj  10129  djuen  10130  djucomen  10138  pwdjuen  10142  djudom1  10143  djuxpdom  10146  djufi  10147  cardadju  10155  nnadju  10158  nnadjuALT  10159  ficardadju  10160  ficardun  10161  ficardun2  10162  pwsdompw  10163  unctb  10164  ackbij2lem1  10178  ackbij1lem6  10184  ackbij1lem16  10194  ackbij1b  10198  ackbij2  10202  coflim  10221  cflim2  10223  cofsmo  10229  coftr  10233  sornom  10237  infpssrlem5  10267  fin4en1  10269  fin23lem23  10286  fin23lem28  10300  isf32lem2  10314  isf32lem4  10316  isf32lem7  10319  isf34lem7  10339  isf34lem6  10340  fin67  10355  isfin7-2  10356  fin1a2lem9  10368  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  zorn2lem6  10461  ttukeylem3  10471  brdom6disj  10492  carddom  10514  cardsdom  10515  domtri  10516  konigthlem  10528  iunctb  10534  alephadd  10537  alephmul  10538  pwcfsdom  10543  cfpwsdom  10544  fpwwe2lem12  10602  canthp1lem2  10613  pwfseqlem3  10620  pwfseqlem4a  10621  inar1  10735  tskcard  10741  tskuni  10743  grur1  10780  mulclpi  10853  addcompi  10854  mulcompi  10856  distrpi  10858  ltexpi  10862  ltapi  10863  ltmpi  10864  enqbreq2  10880  nqereu  10889  addpipq  10897  addpqnq  10898  mulpipq  10900  mulpqnq  10901  addpqf  10904  addclnq  10905  mulpqf  10906  mulclnq  10907  adderpq  10916  mulerpq  10917  ltsonq  10929  lterpq  10930  ltbtwnnq  10938  ltrnq  10939  genpv  10959  genpdm  10962  genpnnp  10965  mulclprlem  10979  distrlem1pr  10985  distrlem4pr  10986  prlem934  10993  addcanpr  11006  suplem1pr  11012  mulcmpblnr  11031  mulclsr  11044  mulasssr  11050  distrsr  11051  ltsosr  11054  1idsr  11058  00sr  11059  recexsrlem  11063  mulgt0sr  11065  addcnsr  11095  axmulf  11106  axmulass  11117  axdistr  11118  axcnre  11124  mulrid  11179  axltadd  11254  lenlt  11259  dedekind  11344  dedekindle  11345  resubcl  11493  subeqrev  11607  muladd  11617  mulsub  11628  mulsub2  11629  ltaddsub2  11660  leaddsub2  11662  leltadd  11669  ltaddpos2  11676  posdif  11678  addge02  11696  mullt0  11704  ltord1  11711  leord1  11712  eqord1  11713  recextlem1  11815  recex  11817  divmuldiv  11889  conjmul  11906  div2sub  12014  prodgt02  12037  lemul2  12042  lemul2a  12044  ltmulgt12  12050  lemulge12  12053  mulge0b  12060  mulle0b  12061  ltmuldiv2  12064  ltdivmul2  12067  lt2mul2div  12068  ledivmul2  12069  lemuldiv2  12071  ledivdiv  12079  lediv2  12080  ltdiv23  12081  lediv23  12082  supmul  12162  riotaneg  12169  negiso  12170  cju  12189  nnaddcl  12216  nnmulcl  12217  nnmtmip  12219  nnsub  12237  addltmul  12425  avgle1  12429  avgle2  12430  avgle  12431  nnrecl  12447  nn0nnaddcl  12480  nn0sub  12499  elz2  12554  zaddcl  12580  zsubcl  12582  znnsub  12586  znn0sub  12587  nzadd  12588  zmulcl  12589  zltp1le  12590  zleltp1  12591  nnleltp1  12596  nnltp1le  12597  nnaddm1cl  12598  nn0ltp1le  12599  nn0leltp1  12600  nn0ltlem1  12601  nn0lem1lt  12606  nnlem1lt  12607  nnltlem1  12608  zdiv  12611  zextle  12614  zextlt  12615  btwnnz  12617  prime  12622  nneo  12625  peano2uz2  12629  uzind  12633  fzind  12639  zriotaneg  12654  uzneg  12820  uztric  12824  uz11  12825  eluzp1m1  12826  eluzp1p1  12828  uzin  12840  uzwo  12877  indstr  12882  uz2mulcl  12892  supminf  12901  uzsupss  12906  zmax  12911  rebtwnz  12913  qre  12919  qaddcl  12931  qsubcl  12934  irradd  12939  elpqb  12942  rpnnen1lem5  12947  cnref1o  12951  rpaddcl  12982  rpmulcl  12983  rpmtmip  12984  rpdivcl  12985  max1  13152  max2  13154  min1  13156  min2  13157  z2ge  13165  qbtwnxr  13167  xaddf  13191  rexadd  13199  rexsub  13200  xnn0xaddcl  13202  xaddcom  13207  xnn0xadd0  13214  xnegdi  13215  rexmul  13238  supxrbnd2  13289  ixxin  13330  elicc2  13379  difreicc  13452  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzval2  13478  elfz1eq  13503  peano2fzr  13505  fzn  13508  fzsplit2  13517  fzaddel  13526  fzadd2  13527  fzsubel  13528  fzrev2  13556  fzrev3  13558  uzsplit  13564  fznuz  13577  uznfz  13578  fzrevral  13580  fzrevral3  13582  fzshftral  13583  elfz2nn0  13586  fznn0sub2  13603  fz0fzdiffz0  13605  elfzmlbp  13607  difelfzle  13609  difelfznle  13610  elfzouz2  13642  fzo0n  13649  fzouzsplit  13662  fzoun  13664  elfzo0le  13671  fzonmapblen  13676  fzofzim  13677  fzoaddel2  13688  eluzgtdifelfzo  13695  elfzodifsumelfzo  13699  ssfzoulel  13728  ubmelm1fzo  13731  fzofzp1b  13733  elfzonelfzo  13737  elfznelfzo  13740  fzostep1  13751  injresinjlem  13755  subfzo0  13757  flflp1  13776  divfl0  13793  flzadd  13795  flmulnn0  13796  fldivnn0le  13801  fldiv  13829  uzsup  13832  mulmod0  13846  modlt  13849  modmulnn  13858  zmodcl  13860  zmodfz  13862  zmodid2  13868  modcyc  13875  muladdmodid  13882  modmuladdnn0  13887  negmod  13888  addmodidr  13892  modadd2mod  13893  modaddmodup  13906  modaddmulmod  13910  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  om2uzlti  13922  om2uzf1oi  13925  fzen2  13941  ssnn0fi  13957  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub0  13965  seqshft2  14000  seqsplit  14007  seqcaopr2  14010  seqf1olem2  14014  expcllem  14044  expcl2lem  14045  1exp  14063  expge1  14071  expadd  14076  expmul  14079  expsub  14082  nn0sq11  14104  lt2sq  14105  le2sq  14106  expmordi  14139  leexp2  14143  leexp1a  14147  sumsqeq0  14151  bernneq  14201  bernneq2  14202  expnbnd  14204  digit2  14208  digit1  14209  facdiv  14259  facwordi  14261  faclbnd  14262  faclbnd3  14264  faclbnd4lem4  14268  faclbnd5  14270  faclbnd6  14271  facavg  14273  bcrpcl  14280  bccmpl  14281  bcval5  14290  hashen  14319  hasheqf1oi  14323  hashgadd  14349  hashdom  14351  hashsdom  14353  hashun  14354  hashunsnggt  14366  hashprg  14367  hashssdif  14384  hashxplem  14405  seqcoll  14436  tpf1o  14473  eqwrd  14529  ccatfval  14545  ccatlen  14547  ccat0  14548  elfzelfzccat  14552  ccatsymb  14554  ccatval21sw  14557  ccatrn  14561  lswccatn0lsw  14563  ccatalpha  14565  ccatrcl1  14566  ccats1alpha  14591  swrdnd  14626  swrdfv2  14633  swrdsbslen  14636  swrdspsleq  14637  swrdccat2  14641  pfxnd0  14660  addlenrevpfx  14662  pfxeq  14668  ccatpfx  14673  pfxccat1  14674  swrdswrdlem  14676  pfxswrd  14678  pfxccatin12lem4  14698  pfxccatin12lem1  14700  pfxccatin12lem2  14703  pfxccatin12lem3  14704  pfxccatin12  14705  pfxccat3  14706  swrdccat  14707  pfxccatpfx2  14709  pfxccat3a  14710  swrdccat3blem  14711  swrdccat3b  14712  revccat  14738  revrev  14739  cshwlen  14771  cshwidxmod  14775  cshwidxmodr  14776  cshweqdif2  14791  cshweqrep  14793  2cshwcshw  14798  s3eq3seq  14912  cotr2g  14949  trclun  14987  shftf  15052  seqshft  15058  crre  15087  crim  15088  readd  15099  resub  15100  remul2  15103  imadd  15107  imsub  15108  immul2  15110  ipcnval  15116  cjsub  15122  cjreim  15133  01sqrexlem6  15220  sqrtle  15233  sqrt11  15235  absreimsq  15265  absreim  15266  absmul  15267  sqabs  15280  absdiflt  15291  absdifle  15292  abssuble0  15302  absmax  15303  abs2difabs  15308  fzomaxdif  15317  rexanuz  15319  rexuz3  15322  rexuzre  15326  caubnd2  15331  limsupgre  15454  limsupbnd2  15456  climconst2  15521  lo1resb  15537  o1resb  15539  2clim  15545  climshftlem  15547  climshft  15549  climshft2  15555  cjcn2  15573  o1of2  15586  o1rlimmul  15592  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  lo1le  15625  climlec2  15632  isershft  15637  isercolllem1  15638  isercolllem3  15640  isercoll  15641  isercoll2  15642  climsup  15643  caurcvg  15650  caucvg  15652  iseraltlem1  15655  iseraltlem2  15656  iseralt  15658  summolem2a  15688  isumclim3  15732  mptfzshft  15751  fsumrev  15752  fsum0diag2  15756  fsumconst  15763  telfsumo2  15776  fsumparts  15779  o1fsum  15786  cvgcmp  15789  cvgcmpub  15790  cvgcmpce  15791  binomlem  15802  binom1p  15804  binom1dif  15806  bcxmas  15808  incexclem  15809  incexc  15810  incexc2  15811  isumshft  15812  isumsplit  15813  isumsup2  15819  climcndslem1  15822  climcndslem2  15823  climcnds  15824  supcvg  15829  expcnv  15837  geoserg  15839  pwdif  15841  geolim  15843  geoisum1  15852  geoisum1c  15853  cvgrat  15856  mertenslem1  15857  mertenslem2  15858  mertens  15859  ntrivcvgfvn0  15872  ntrivcvgmullem  15874  prodmolem2a  15907  prodmo  15909  fprodf1o  15919  fproddiv  15934  fprodeq0  15948  risefacval2  15983  fallfacval2  15984  fallfacval3  15985  rprisefaccl  15996  risefallfac  15997  fallfacfwd  16009  binomfallfaclem1  16012  binomfallfaclem2  16013  binomrisefac  16015  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  efcj  16065  fprodefsum  16068  efexp  16076  eftlub  16084  effsumlt  16086  efle  16093  reef11  16094  efieq  16138  sinsub  16143  cossub  16144  subsin  16146  sinmul  16147  cosmul  16148  addcos  16149  subcos  16150  rpnnen2lem10  16198  rpnnen2lem12  16200  ruclem8  16212  ruclem12  16216  sqrt2irr  16224  dvdssub2  16278  dvdsadd  16279  dvdsaddr  16280  dvdssub  16281  dvdssubr  16282  dvdsle  16287  alzdvds  16297  fzocongeq  16301  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  pwp1fsum  16368  divalglem4  16373  divalglem9  16378  divalgb  16381  divalgmod  16383  ndvdsadd  16387  smueqlem  16467  gcdaddm  16502  modgcd  16509  bezoutlem1  16516  dvdsgcd  16521  absmulgcd  16526  rpmulgcd  16534  rprpwr  16536  sqgcd  16539  dvdssqlem  16543  dvdssq  16544  nn0seqcvgd  16547  algrf  16550  algcvg  16553  lcmcllem  16573  lcmabs  16582  lcmgcd  16584  lcmdvds  16585  lcmgcdnn  16588  lcmf  16610  coprmgcdb  16626  coprmdvds  16630  coprmdvds2  16631  qredeq  16634  isprm3  16660  nprm  16665  oddprmgt2  16676  isprm5  16684  isprm7  16685  divgcdodd  16687  prmdvdsexp  16692  zgcdsq  16730  hashdvds  16752  phiprmpw  16753  crth  16755  phimullem  16756  modprm0  16783  coprimeprodsq  16786  coprimeprodsq2  16787  pythagtriplem2  16795  pythagtriplem19  16811  iserodd  16813  pcpremul  16821  pcmul  16829  pcexp  16837  pcdvdsb  16847  pcneg  16852  pc2dvds  16857  pc11  16858  pcmpt  16870  fldivp1  16875  pcfac  16877  infpnlem1  16888  prmunb  16892  prmreclem1  16894  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  1arithlem4  16904  1arith  16905  gzaddcl  16915  gzmulcl  16916  gzreim  16917  gzsubcl  16918  4sqlem1  16926  4sqlem4a  16929  4sqlem4  16930  4sqlem12  16934  ramlb  16997  prmgaplem4  17032  prmgaplem5  17033  prmgaplem6  17034  prmgaplem7  17035  prmgaplem8  17036  prmgapprmolem  17039  cshwshashlem2  17074  setsvalg  17143  ressval  17210  ressval3d  17223  restval  17396  pwsval  17456  xpsval  17540  ssclem  17788  rescval  17796  funcestrcsetclem9  18116  embedsetcestrclem  18125  lubel  18480  ipodrsima  18507  tsrss  18555  resmgmhm  18645  resmgmhm2  18646  mgmhmco  18648  submnd0  18697  mndinvmod  18698  xpsmnd0  18712  resmhm  18754  resmhm2  18755  mhmco  18757  frmdplusg  18788  frmdmnd  18793  efmndcl  18816  smndex1id  18845  mgm2nsgrplem1  18852  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2nmndlem1  18857  sgrp2rid2  18860  dfgrp3  18978  mhmmnd  19003  mulgnngsum  19018  mulgnnsubcl  19025  mulgnn0z  19040  mulgnndir  19042  mulgmodid  19052  eqgfval  19115  cycsubgcl  19145  cycsubg2  19149  0ghm  19169  resghm  19171  resghm2  19172  ghmco  19175  ghmeql  19178  isgim  19201  gicsubgen  19218  cntzmhm  19280  symgcl  19322  symgextf1  19358  gsmsymgrfixlem1  19364  symgfixf1  19374  symgtrinv  19409  pmtrdifellem3  19415  mndodcongi  19480  odmod  19483  odf1  19499  odf1o1  19509  gexdvds  19521  sylow1lem1  19535  pgpssslw  19551  lsmub1  19594  lsmub2  19595  cntzrecd  19615  pj1ghm  19640  lsmhash  19642  efgred  19685  frgpup1  19712  ablsubadd23  19750  ablsubsub23  19761  mulgnn0di  19762  torsubg  19791  zaddablx  19809  gsumzaddlem  19858  gsumzadd  19859  gsumconst  19871  gsumzmhm  19874  telgsumfzslem  19925  dprdfadd  19959  dprd2dlem1  19980  ablsimpgfindlem1  20046  srgbinomlem3  20144  srgbinomlem4  20145  srgbinomlem  20146  gsummgp0  20234  gsumdixp  20235  xpsring1d  20249  unitnegcl  20313  isrnghm  20357  rnghmco  20373  dfrhm2  20390  rhmco  20417  c0rhm  20450  c0rnghm  20451  rhmimasubrng  20482  cntzsubrng  20483  issubrg3  20516  resrhm  20517  rhmeql  20519  rhmima  20520  isdomn4  20632  imadrhmcl  20713  fldsdrgfld  20714  abvres  20747  lmodfopne  20813  lspf  20887  lspcl  20889  0lmhm  20954  lmhmco  20957  lmhmeql  20969  islmim  20976  rngqiprngghm  21216  rngqiprnglin  21219  xrs1cmn  21330  xrsdsreval  21335  xrsdsreclb  21337  znfld  21477  znchr  21479  znunithash  21481  znrrg  21482  freshmansdream  21491  cnmsgnsubg  21493  zrhpsgnmhm  21500  evpmodpmf1o  21512  psgndiflemB  21516  psgndif  21518  phlssphl  21575  frlmval  21664  uvcfval  21700  frlmsslsp  21712  frlmup2  21715  lindfmm  21743  lmimlbs  21752  islindf4  21754  issubassa3  21782  psrbaglesupp  21838  psrcom  21884  resspsrmul  21892  mplsubrglem  21920  mplcoe3  21952  ltbval  21957  ltbwe  21958  evlslem4  21990  evlslem3  21994  psdmvr  22063  psropprmul  22129  coe1tmmul  22170  cply1mul  22190  gsummoncoe1  22202  lply1binomsc  22205  pf1ind  22249  mamufacex  22290  grpvlinv  22292  grpvrinv  22293  eqmat  22318  mat1dimcrng  22371  dmatcrng  22396  scmatf1  22425  m1detdiag  22491  mdetdiaglem  22492  mdet1  22495  mdetunilem9  22514  madulid  22539  gsummatr01lem4  22552  gsummatr01  22553  mat2pmatlin  22629  m2pmfzgsumcl  22642  monmatcollpw  22673  pmatcollpw3lem  22677  mp2pm2mplem4  22703  chpscmatgsummon  22739  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  cayhamlem1  22760  cpmadugsumlemF  22770  clsval2  22944  innei  23019  ordtrest  23096  ordtrestixx  23116  isnrm2  23252  lpcls  23258  tgcmp  23295  cmpcld  23296  uncmp  23297  hauscmplem  23300  hauscmp  23301  1stcfb  23339  1stcrest  23347  kgencmp2  23440  1stckgenlem  23447  kgen2ss  23449  kgencn  23450  kgencn3  23452  txval  23458  txuni2  23459  txbasex  23460  txbas  23461  txtop  23463  ptbasin  23471  txtopon  23485  txcld  23497  txss12  23499  txbasval  23500  xkoccn  23513  txcnp  23514  ptcnplem  23515  upxp  23517  txcnmpt  23518  uptx  23519  txrest  23525  txdis  23526  txindislem  23527  txlly  23530  txnlly  23531  txcmp  23537  hausdiag  23539  txhaus  23541  tx1stc  23544  tx2ndc  23545  txkgen  23546  xkoptsub  23548  cnmpt21  23565  txconn  23583  qtopval  23589  hmeoco  23666  txhmeo  23697  xpstopnlem1  23703  fbun  23734  filss  23747  infil  23757  fbunfip  23763  filuni  23779  fmfnfmlem4  23851  ufldom  23856  flffval  23883  flfval  23884  txflf  23900  fcfval  23927  alexsubALTlem3  23943  tgpmulg  23987  subgtgp  23999  qustgplem  24015  tsmsfbas  24022  tsmsres  24038  tsmsmhm  24040  tsmsadd  24041  isxmet2d  24222  blin2  24324  comet  24408  met2ndci  24417  metcn  24438  txmetcn  24443  dscopn  24468  nrmmetd  24469  isngp3  24493  tngval  24534  nm1  24562  subrgnrg  24568  nrginvrcn  24587  rlmnvc  24598  nmo0  24630  nmoco  24632  nghmco  24633  nmotri  24634  0nghm  24636  isnmhm2  24647  0nmhm  24650  nmhmco  24651  nmhmplusg  24652  qtopbaslem  24653  remetdval  24684  bl2ioo  24687  reperflem  24714  iccntr  24717  icccmplem2  24719  icccmp  24721  reconnlem2  24723  xrge0gsumle  24729  xrge0tsms  24730  divcnOLD  24764  divcn  24766  cncfmet  24809  iccpnfcnv  24849  bndth  24864  copco  24925  pcopt  24929  pcopt2  24930  nmhmcn  25027  cmodscexp  25028  cphassr  25119  lmmbrf  25169  lmnn  25170  iscauf  25187  caucfil  25190  iscmet3lem1  25198  iscmet3lem2  25199  iscmet3  25200  cfilres  25203  caussi  25204  caubl  25215  caublcls  25216  bcthlem2  25232  bcthlem5  25235  cmsss  25258  lssbn  25259  ovolfioo  25375  ovollb2lem  25396  ovolunlem1a  25404  ovoliunlem1  25410  ovoliunlem2  25411  ovoliunlem3  25412  ovoliun2  25414  ovolscalem1  25421  ovolicc2lem1  25425  ovolicc2lem4  25428  ovolicc2lem5  25429  inmbl  25450  voliunlem1  25458  volsup  25464  ioombl1lem4  25469  iccvolcl  25475  ioovolcl  25478  uniioovol  25487  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombllem6  25496  dyadf  25499  dyadovol  25501  dyadss  25502  dyadmbl  25508  opnmbllem  25509  volsup2  25513  volcn  25514  ismbf  25536  mbfima  25538  ismbf3d  25562  mbfadd  25569  mbfsub  25570  mbflimsup  25574  itg1mulc  25612  itg1sub  25617  itg1climres  25622  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfmul  25634  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2lea  25652  itg2eqa  25653  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2i1fseqle  25662  itg2i1fseq  25663  itg2i1fseq2  25664  itg2addlem  25666  itg2cnlem1  25669  bddmulibl  25747  ellimc3  25787  dvaddbr  25847  dvcobr  25856  dvcobrOLD  25857  dvcjbr  25860  dvcnvlem  25887  c1lip1  25909  lhop  25928  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumrlimf  25938  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  tdeglem4  25972  deg1ge  26010  coe1mul3  26011  fta1g  26082  plyco0  26104  plyf  26110  ply1termlem  26115  plyeq0lem  26122  plypf1  26124  plymullem1  26126  plyaddlem  26127  plymullem  26128  coeeulem  26136  coeidlem  26149  plyco  26153  dgreq  26156  coefv0  26160  coeaddlem  26161  coemullem  26162  coemulhi  26166  coemulc  26167  plycn  26173  plycnOLD  26174  dgrlt  26179  dgrsub  26185  plycjlem  26189  plycj  26190  plycjOLD  26192  plyrecj  26194  plymul0or  26195  plyreres  26197  dvply1  26198  vieta1lem2  26226  plyexmo  26228  elqaalem2  26235  elqaalem3  26236  aareccl  26241  aalioulem1  26247  aalioulem3  26249  aaliou  26253  geolim3  26254  ulmcaulem  26310  ulmcau  26311  mtest  26320  dvradcnv  26337  psercn2  26339  psercn2OLD  26340  pserdvlem2  26345  pserdv2  26347  abelthlem6  26353  abelthlem8  26356  abelthlem9  26357  reeff1o  26364  reefgim  26367  sinperlem  26396  sincosq2sgn  26415  sincosq3sgn  26416  sinq12ge0  26424  sincos6thpi  26432  sineq0  26440  cosord  26447  cos11  26449  sinord  26450  tanord1  26453  eff1olem  26464  logrnaddcl  26490  relogeftb  26500  relogoprlem  26507  logleb  26519  advlogexp  26571  logtayllem  26575  logtayl  26576  logtaylsum  26577  logtayl2  26578  recxpcl  26591  rpcxpcl  26592  cxple3  26617  cxpcom  26655  cxpcn3  26665  cxpeq  26674  relogbmul  26694  relogbcxp  26702  relogbf  26708  atanord  26844  atantayl  26854  birthdaylem2  26869  birthdaylem3  26870  cxp2limlem  26893  fsumharmonic  26929  zetacvg  26932  ftalem1  26990  ftalem4  26993  ftalem5  26994  basellem2  26999  basellem3  27000  basellem4  27001  vmappw  27033  sqf11  27056  mumul  27098  fsumdvdscom  27102  dvdsppwf1o  27103  dvdsflf1o  27104  musum  27108  muinv  27110  fsumdvdsmul  27112  1sgmprm  27117  vmalelog  27123  chtublem  27129  fsumvma  27131  vmasum  27134  logfac2  27135  chpval2  27136  logfaclbnd  27140  logexprlim  27143  mersenne  27145  dchrmulcl  27167  dchrinvcl  27171  dchrfi  27173  dchrghm  27174  dchrptlem1  27182  dchrsum2  27186  dchrsum  27187  pcbcctr  27194  bcmono  27195  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem5  27206  bposlem6  27207  bposlem7  27208  lgslem3  27217  lgscllem  27222  lgsval4a  27237  lgsneg  27239  lgsdir2  27248  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  gausslemma2dlem6  27290  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2  27304  lgsquad3  27305  2lgslem1a1  27307  2lgslem1a  27309  2lgslem1c  27311  2sqlem2  27336  mul2sq  27337  2sqlem7  27342  2sqreultlem  27365  2sqreunnltlem  27368  2sqreunnltblem  27369  chebbnd1lem1  27387  vmadivsum  27400  rplogsumlem2  27403  dchrisum0lem1a  27404  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasum2if  27415  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  dchrisum0ff  27425  dchrisum0flblem1  27426  dchrisum0fno1  27429  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  mudivsum  27448  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  selberglem2  27464  selberg2  27469  chpdifbndlem1  27471  selberg3lem1  27475  pntrsumbnd2  27485  selbergr  27486  pntpbnd1  27504  pntpbnd2  27505  pntlemh  27517  pntlemj  27521  pntlemi  27522  pntlemf  27523  pntlemp  27528  ostth2lem1  27536  ostth1  27551  ostth2lem3  27553  ostth3  27556  noreson  27579  nosepon  27584  noextendseq  27586  nosupbnd1lem5  27631  noetasuplem4  27655  addscom  27880  negsdi  27963  om2noseqlt  28200  om2noseqf1o  28202  n0s0suc  28241  nnsge1  28242  n0sbday  28251  n0sfincut  28253  n0sltp1le  28262  bdayn0sf1o  28266  zaddscl  28289  elzn0s  28293  zseo  28315  remulscllem2  28359  istrkg2ld  28394  isismt  28468  eedimeq  28832  eqeefv  28837  brbtwn2  28839  colinearalglem1  28840  colinearalglem2  28841  colinearalg  28844  eleesub  28845  eleesubd  28846  axcgrrflx  28848  axcgrid  28850  axsegconlem2  28852  axsegconlem7  28857  axsegconlem9  28859  axsegconlem10  28860  axlowdimlem14  28889  axlowdimlem16  28891  axlowdimlem17  28892  axcontlem2  28899  axcontlem4  28901  axcontlem8  28905  axcontlem10  28907  structiedg0val  28956  upgr1eop  29049  numedglnl  29078  usgredg2v  29161  ushgredgedg  29163  ushgredgedgloop  29165  uspgr1eop  29181  usgr1eop  29184  uhgrissubgr  29209  umgrres1lem  29244  upgrres1  29247  nbuhgr  29277  edgnbusgreu  29301  nb3gr2nb  29318  uvtxnm1nbgr  29338  cusgrexilem2  29376  finsumvtxdg2ssteplem4  29483  vtxdgoddnumeven  29488  wlkeq  29569  uspgr2wlkeq  29581  wlksoneq1eq2  29599  upgrwlkdvdelem  29673  usgr2wlkspthlem1  29694  usgrn2cycl  29746  crctcshwlkn0lem3  29749  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  wspthneq1eq2  29797  wwlkseq  29828  wwlksnext  29830  rusgrnumwlkg  29914  clwwlkccatlem  29925  clwwlkccat  29926  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  clwlkclwwlkf1lem3  29942  clwwisshclwwslemlem  29949  clwwisshclwws  29951  erclwwlkeqlen  29955  erclwwlkref  29956  clwwnisshclwwsn  29995  clwwlknccat  29999  erclwwlkneqlen  30004  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwlksndivn  30022  uhgr3cyclex  30118  eucrctshift  30179  eucrct2eupth  30181  frgreu  30204  frgr3v  30211  3vfriswmgr  30214  frgrncvvdeqlem3  30237  frgrregorufrg  30262  numclwwlk1lem2f1  30293  numclwwlk1lem2fo  30294  numclwlk1lem2  30306  numclwwlk3  30321  numclwwlk6  30326  frgrreg  30330  frgrregord013  30331  nsnlplig  30417  nsnlpligALT  30418  ablodivdiv4  30490  imsdval  30622  nmcvcn  30631  sspval  30659  lnoadd  30694  lnosub  30695  nmooge0  30703  nmoolb  30707  nmoub3i  30709  blocnilem  30740  blocni  30741  cncph  30755  ipasslem1  30767  ipasslem2  30768  ipasslem4  30770  ipasslem11  30776  ipblnfi  30791  phoeqi  30793  ubthlem1  30806  ubthlem3  30808  htthlem  30853  hvsub4  30973  his7  31026  his2sub2  31029  hial2eq2  31043  hhip  31113  hhph  31114  bcs2  31118  hhssabloi  31198  hhssnv  31200  ocorth  31227  shsel  31250  shsel3  31251  shscli  31253  chsupss  31278  shjval  31287  chjval  31288  shjcl  31292  chjcl  31293  shsleji  31306  chslej  31434  chsscon2  31438  chjcom  31442  chub1  31443  chdmj1  31465  spanunsni  31515  spanpr  31516  fh1  31554  fh2  31555  cm2j  31556  spansncvi  31588  5oalem1  31590  5oalem3  31592  5oalem5  31594  3oalem2  31599  pjcompi  31608  pjds3i  31649  hoeq  31696  hoadddi  31739  hoadddir  31740  hosubdi  31744  hosub4  31749  hoeq1  31766  hoeq2  31767  adjval2  31827  counop  31857  adjeq  31871  brafnmul  31887  lnopsubi  31910  hmops  31956  hmopm  31957  hmopd  31958  hmopco  31959  nmcopexi  31963  lnconi  31969  lnfnsubi  31982  nmcfnexi  31987  imaelshi  31994  nlelshi  31996  riesz3i  31998  riesz1  32001  cnlnadjlem2  32004  cnlnadjlem6  32008  adjbdln  32019  adjlnop  32022  adjmul  32028  adjadd  32029  nmopcoi  32031  rnbra  32043  cnvbramul  32051  kbass2  32053  kbass4  32055  kbass5  32056  kbass6  32057  leopadd  32068  leopmul2i  32071  leoptri  32072  dmdmd  32236  mddmd  32237  cvdmd  32273  superpos  32290  chrelati  32300  atcv0eq  32315  atomli  32318  atcvatlem  32321  atcvati  32322  atcvat2i  32323  chirredlem4  32329  atcvat3i  32332  atcvat4i  32333  mdsymlem2  32340  mdsymlem3  32341  mdsymlem5  32343  mdsymlem8  32346  dmdsym  32349  cdjreui  32368  cdj1i  32369  cdj3lem2b  32373  cdj3lem3  32374  cdj3lem3b  32376  cdj3i  32377  brabgaf  32543  prct  32645  fcobijfs  32653  fzsplit3  32723  bcm1n  32725  dpfrac1  32819  wrdres  32863  xrge0mulgnn0  32963  xrge0tsmsd  33009  xrge0omnd  33032  cycpmco2  33097  suborng  33300  isarchiofld  33302  resvval  33308  nsgqusf1olem2  33392  lbslsat  33619  ply1degltdimlem  33625  ply1degltdim  33626  ordtrestNEW  33918  mhmhmeotmd  33924  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0pluscn  33937  hasheuni  34082  sxval  34187  measvuni  34211  ddemeas  34233  br2base  34267  dya2iocucvr  34282  sxbrsigalem2  34284  sxbrsiga  34288  omssubadd  34298  eulerpartlemgc  34360  ballotlemfc0  34491  ballotlemfcc  34492  signstfvc  34572  signstres  34573  signsvfn  34580  bnj563  34740  bnj554  34896  bnj557  34898  bnj570  34902  bnj594  34909  bnj849  34922  bnj970  34944  bnj1118  34981  bnj1145  34990  bnj1190  35005  bnj1398  35031  bnj1417  35038  zltp1ne  35104  nnltp1ne  35105  nn0ltp1ne  35106  0nn0m1nnn0  35107  cusgr3cyclex  35130  derangsn  35164  derangen  35166  subfacp1lem5  35178  erdsze2lem1  35197  txpconn  35226  txsconn  35235  cvmliftphtlem  35311  satfdm  35363  satfun  35405  ex-sategoelel  35415  mrsubff1  35508  msubff  35524  msubff1  35550  msubvrs  35554  inffz  35724  bcprod  35732  bccolsum  35733  faclim  35740  dfon2lem4  35781  colineardim1  36056  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem8  36089  btwnconn1lem9  36090  btwnconn1lem12  36093  btwnconn1lem13  36094  btwnconn1lem14  36095  outsideofeu  36126  funray  36135  lineintmo  36152  fwddifnp1  36160  hfun  36173  nn0prpw  36318  opnregcld  36325  cldregopn  36326  ivthALT  36330  onsucconni  36432  bj-nnfim1  36739  bj-nnfim2  36740  bj-2uplex  37017  bj-unexg  37033  bj-prexg  37034  bj-idres  37155  isbasisrelowllem1  37350  isbasisrelowllem2  37351  icoreclin  37352  relowlssretop  37358  exrecfnlem  37374  pibt2  37412  unccur  37604  phpreu  37605  finixpnum  37606  ltflcei  37609  cos2h  37612  lindsadd  37614  lindsdom  37615  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  heicant  37656  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  ovoliunnfl  37663  mbfresfi  37667  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anclem3  37696  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  indexa  37734  incsequz  37749  incsequz2  37750  geomcau  37760  sstotbnd2  37775  prdsbnd  37794  prdstotbnd  37795  prdsbnd2  37796  cntotbnd  37797  ismtyhmeolem  37805  ismtybndlem  37807  heibor1lem  37810  heiborlem3  37814  heiborlem6  37817  heibor  37822  bfplem1  37823  bfplem2  37824  elghomlem1OLD  37886  rngogrphom  37972  prnc  38068  ispridlc  38071  pridlc3  38074  mpobi123f  38163  mptbi12f  38167  antisymressn  38442  eqvreltr  38605  ax12indalem  38945  lsateln0  38995  atlatmstc  39319  hlatjidm  39369  llnneat  39515  lplnneat  39546  lplnnelln  39547  lvolneatN  39589  lvolnelln  39590  lvolnelpln  39591  dalem23  39697  snatpsubN  39751  linepsubN  39753  pmapsub  39769  pmapglbx  39770  paddasslem14  39834  polsubN  39908  pol1N  39911  2polvalN  39915  2polssN  39916  3polN  39917  2pmaplubN  39927  polatN  39932  2polatN  39933  pnonsingN  39934  polsubclN  39953  lautco  40098  cdlemefrs29cpre1  40399  dian0  41040  dia0eldmN  41041  dia1eldmN  41042  dia0  41053  dia1N  41054  dvhopaddN  41115  dib0  41165  dih0  41281  dih1  41287  dihglblem5apreN  41292  dihatexv2  41340  dochfN  41357  lcmineqlem1  42024  lcmineqlem17  42040  xppss12  42224  sumcubes  42308  dvdsexpnn  42328  remul01  42402  resubeqsub  42425  ricdrng1  42523  prjspeclsp  42607  ismrcd2  42694  nacsfix  42707  mzpaddmpt  42736  mzpmulmpt  42737  eq0rabdioph  42771  lerabdioph  42800  ltrabdioph  42803  nerabdioph  42804  dvdsrabdioph  42805  fiphp3d  42814  congneg  42965  jm2.22  42991  jm2.23  42992  jm2.15nn0  42999  jm3.1  43016  aomclem8  43057  lsmfgcl  43070  lmhmfgima  43080  lnmepi  43081  dgrsub2  43131  mpaaeu  43146  mendring  43184  proot1ex  43192  unielss  43214  onsucwordi  43284  oaabsb  43290  rp-oelim2  43304  nnoeomeqom  43308  cantnfresb  43320  oawordex2  43322  omcl3g  43330  ordsssucb  43331  tfsconcatrev  43344  onsucunipr  43368  onsucunitp  43369  oaun3lem1  43370  naddgeoa  43390  oaltom  43401  minregex2  43531  sssymdifcl  43568  relexp01min  43709  ntrclsiso  44063  ntrclsk3  44066  cvgdvgrat  44309  nznngen  44312  uzmptshftfval  44342  addrval  44462  subrval  44463  mulvval  44464  elpwgded  44561  eel2131  44710  eel3132  44711  el12  44722  sspwimp  44914  sspwimpcf  44916  suctrALTcf  44918  suctrALT3  44920  relpfrlem  44950  cnfex  45029  disjinfi  45193  infxrbnd2  45372  supminfxr  45467  climinf  45611  lptre2pt  45645  limcresiooub  45647  limcresioolb  45648  addlimc  45653  limclner  45656  limsuppnflem  45715  limsupmnfuzlem  45731  limsupvaluz2  45743  limsupresxr  45771  liminfresxr  45772  cnrefiisplem  45834  cncfdmsn  45895  iblspltprt  45978  itgspltprt  45984  dirkertrigeqlem3  46105  fourierdlem62  46173  fourierdlem80  46191  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  sge0f1o  46387  hoidmvlelem2  46601  pimdecfgtioo  46722  smfliminflem  46835  fnresfnco  47046  fcores  47072  dfatcolem  47260  nn0resubcl  47313  zgeltp1eq  47314  eluzge0nn0  47317  fz0addcom  47322  elfzlble  47325  fzopredsuc  47328  subsubelfzo0  47331  ceilbi  47338  minusmod5ne  47354  submodlt  47355  mod0mul  47361  m1modmmod  47363  uniimafveqt  47386  fundcmpsurinjimaid  47416  icceuelpartlem  47440  iccpartnel  47443  elsprel  47480  fmtnodvds  47549  goldbachth  47552  fmtnoprmfac2  47572  prmdvdsfmtnof1  47592  2pwp1prm  47594  flsqrt  47598  lighneallem4  47615  dfodd6  47642  divgcdoddALTV  47687  opoeALTV  47688  opeoALTV  47689  omoeALTV  47690  omeoALTV  47691  epoo  47708  emoo  47709  epee  47710  emee  47711  evensumeven  47712  even3prm2  47724  mogoldbblem  47725  fpprmod  47732  dfwppr  47743  fpprwppr  47744  fpprwpprb  47745  gbepos  47763  gbegt5  47766  gbowgt5  47767  gboge9  47769  sbgoldbst  47783  nnsum3primesgbe  47797  bgoldbtbndlem1  47810  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  grimco  47893  isuspgrim0  47898  isuspgrimlem  47899  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrim  47938  grimedg  47939  isgrtri  47946  cycl3grtri  47950  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  isubgr3stgrlem8  47976  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlimlem4  47994  grlictr  48011  gpgusgralem  48051  gpgedg2ov  48061  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg5grlic  48088  2zrngmmgm  48244  2zrngnmrid  48248  2zrngnmlid2  48249  altgsumbc  48344  altgsumbcALT  48345  zlmodzxzadd  48350  zlmodzxzsub  48352  invginvrid  48359  ply1mulgsumlem2  48380  ply1mulgsum  48383  lincvalpr  48411  lindslinindimp2lem1  48451  ldepsprlem  48465  ldepspr  48466  lincresunit3lem3  48467  lincresunitlem1  48468  lincresunit3lem1  48472  lincresunit3  48474  elfzolborelfzop1  48512  zgtp1leeq  48514  flsubz  48515  nneom  48520  nn0ofldiv2  48525  rege1logbrege0  48551  nnpw2pb  48580  dignn0fr  48594  dignn0ldlem  48595  dignnld  48596  dignn0flhalflem1  48608  nn0sumshdiglemB  48613  nn0mulfsum  48617  rrx2plordisom  48716  ehl2eudis0lt  48719  itsclinecirc0in  48768  2itscp  48774  inlinecirc02plem  48779  mof0ALT  48832  i0oii  48912  resccat  49067