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  2373  nfeqf  2379  eqeqan12dALT  2748  sylan9eq  2784  sylan9ss  3960  ssconb  4105  ineqan12d  4185  ifpr  4657  disjtp2  4680  dfopg  4835  disjxiun  5104  breqan12d  5123  eusv1  5346  opelvvg  5679  opthprc  5702  relop  5814  dmpropg  6188  unixp  6255  tz7.7  6358  ordin  6362  onin  6363  ontri1  6366  onfr  6371  onelpss  6372  onsseleq  6373  oneltri  6375  ontr2  6380  onunel  6439  onun2  6442  funssres  6560  funtpg  6571  funtp  6573  resasplit  6730  fodmrnu  6780  f1un  6820  dffv2  6956  fvreseq0  7010  fvcofneq  7065  funopdmsn  7122  fprg  7127  fprb  7168  fconst2g  7177  isofrlem  7315  oveqan12d  7406  ov3  7552  ovg  7554  ovima0  7568  f1opw2  7644  off  7671  unexgOLD  7725  pwuncl  7746  epweon  7751  epweonALT  7752  sucexeloni  7785  ordunpr  7801  omun  7864  peano4  7868  fabexg  7914  f1oabexg  7918  fiun  7921  offres  7962  el2mpocsbcl  8064  curry1  8083  curry1val  8084  curry2  8086  curry2val  8088  soxp  8108  wexp  8109  xpord2pred  8124  poxp3  8129  poseq  8137  soseq  8138  suppfnss  8168  frrlem4  8268  frrlem11  8275  frrlem12  8276  fprlem1  8279  iunon  8308  onfununi  8310  tfrlem11  8356  tz7.48lem  8409  seqomeq12  8422  oacan  8512  oawordri  8514  oaass  8525  omord2  8531  omcan  8533  oen0  8550  oeordi  8551  oeord  8552  oecan  8553  oeworde  8557  oeordsuc  8558  oelimcl  8564  nnawordi  8585  nnaword  8591  nnmord  8596  oaabslem  8611  omabslem  8614  omsmo  8622  eldifsucnn  8628  naddcllem  8640  naddov2  8643  ertr  8686  erex  8695  brecop  8783  ecopovtrn  8793  ecovdi  8798  mapvalg  8809  pmvalg  8810  pmss12g  8842  elmapresaun  8853  boxcutc  8914  undom  9029  sbthlem7  9057  sbth  9061  sdomnsym  9066  sdomdomtr  9074  xpf1o  9103  xpen  9104  limenpsi  9116  pssnn  9132  pwssfi  9141  sbthfi  9163  php2  9172  php3  9173  phpeqd  9176  nndomog  9177  onomeneq  9178  1sdomOLD  9196  ominfOLD  9206  isinf  9207  isinfOLD  9208  fineqvlem  9209  f1finf1o  9216  en1eqsnOLD  9220  dif1ennnALT  9222  findcard3  9229  findcard3OLD  9230  unblem2  9240  isfinite2  9245  unfilem1  9254  unfi2  9259  fodomfir  9279  unifi2  9296  f1opwfi  9307  fsuppxpfi  9336  fsuppunbi  9340  fsuppco2  9354  fsuppcor  9355  fival  9363  fiin  9373  ordiso  9469  ordtypelem10  9480  hartogslem1  9495  wofib  9498  brwdom3  9535  unwdomg  9537  xpwdomg  9538  sucprcreg  9554  preleqALT  9570  inf3lem6  9586  oemapval  9636  cantnf  9646  wemapwe  9650  cnfcom  9653  ttrcltr  9669  dfttrcl2  9677  frmin  9702  r111  9728  r1ord3g  9732  prwf  9764  r1pw  9798  rankprb  9804  rankxplim  9832  tcrank  9837  updjud  9887  finnum  9901  xpnum  9904  carduni  9934  nnsdomel  9943  fidomtri  9946  pr2nelemOLD  9956  infxpenlem  9966  fseqdom  9979  onssnum  9993  acndom2  10007  alephinit  10048  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem6  10109  undjudom  10121  endjudisj  10122  djuen  10123  djucomen  10131  pwdjuen  10135  djudom1  10136  djuxpdom  10139  djufi  10140  cardadju  10148  nnadju  10151  nnadjuALT  10152  ficardadju  10153  ficardun  10154  ficardun2  10155  pwsdompw  10156  unctb  10157  ackbij2lem1  10171  ackbij1lem6  10177  ackbij1lem16  10187  ackbij1b  10191  ackbij2  10195  coflim  10214  cflim2  10216  cofsmo  10222  coftr  10226  sornom  10230  infpssrlem5  10260  fin4en1  10262  fin23lem23  10279  fin23lem28  10293  isf32lem2  10307  isf32lem4  10309  isf32lem7  10312  isf34lem7  10332  isf34lem6  10333  fin67  10348  isfin7-2  10349  fin1a2lem9  10361  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  zorn2lem6  10454  ttukeylem3  10464  brdom6disj  10485  carddom  10507  cardsdom  10508  domtri  10509  konigthlem  10521  iunctb  10527  alephadd  10530  alephmul  10531  pwcfsdom  10536  cfpwsdom  10537  fpwwe2lem12  10595  canthp1lem2  10606  pwfseqlem3  10613  pwfseqlem4a  10614  inar1  10728  tskcard  10734  tskuni  10736  grur1  10773  mulclpi  10846  addcompi  10847  mulcompi  10849  distrpi  10851  ltexpi  10855  ltapi  10856  ltmpi  10857  enqbreq2  10873  nqereu  10882  addpipq  10890  addpqnq  10891  mulpipq  10893  mulpqnq  10894  addpqf  10897  addclnq  10898  mulpqf  10899  mulclnq  10900  adderpq  10909  mulerpq  10910  ltsonq  10922  lterpq  10923  ltbtwnnq  10931  ltrnq  10932  genpv  10952  genpdm  10955  genpnnp  10958  mulclprlem  10972  distrlem1pr  10978  distrlem4pr  10979  prlem934  10986  addcanpr  10999  suplem1pr  11005  mulcmpblnr  11024  mulclsr  11037  mulasssr  11043  distrsr  11044  ltsosr  11047  1idsr  11051  00sr  11052  recexsrlem  11056  mulgt0sr  11058  addcnsr  11088  axmulf  11099  axmulass  11110  axdistr  11111  axcnre  11117  mulrid  11172  axltadd  11247  lenlt  11252  dedekind  11337  dedekindle  11338  resubcl  11486  subeqrev  11600  muladd  11610  mulsub  11621  mulsub2  11622  ltaddsub2  11653  leaddsub2  11655  leltadd  11662  ltaddpos2  11669  posdif  11671  addge02  11689  mullt0  11697  ltord1  11704  leord1  11705  eqord1  11706  recextlem1  11808  recex  11810  divmuldiv  11882  conjmul  11899  div2sub  12007  prodgt02  12030  lemul2  12035  lemul2a  12037  ltmulgt12  12043  lemulge12  12046  mulge0b  12053  mulle0b  12054  ltmuldiv2  12057  ltdivmul2  12060  lt2mul2div  12061  ledivmul2  12062  lemuldiv2  12064  ledivdiv  12072  lediv2  12073  ltdiv23  12074  lediv23  12075  supmul  12155  riotaneg  12162  negiso  12163  cju  12182  nnaddcl  12209  nnmulcl  12210  nnmtmip  12212  nnsub  12230  addltmul  12418  avgle1  12422  avgle2  12423  avgle  12424  nnrecl  12440  nn0nnaddcl  12473  nn0sub  12492  elz2  12547  zaddcl  12573  zsubcl  12575  znnsub  12579  znn0sub  12580  nzadd  12581  zmulcl  12582  zltp1le  12583  zleltp1  12584  nnleltp1  12589  nnltp1le  12590  nnaddm1cl  12591  nn0ltp1le  12592  nn0leltp1  12593  nn0ltlem1  12594  nn0lem1lt  12599  nnlem1lt  12600  nnltlem1  12601  zdiv  12604  zextle  12607  zextlt  12608  btwnnz  12610  prime  12615  nneo  12618  peano2uz2  12622  uzind  12626  fzind  12632  zriotaneg  12647  uzneg  12813  uztric  12817  uz11  12818  eluzp1m1  12819  eluzp1p1  12821  uzin  12833  uzwo  12870  indstr  12875  uz2mulcl  12885  supminf  12894  uzsupss  12899  zmax  12904  rebtwnz  12906  qre  12912  qaddcl  12924  qsubcl  12927  irradd  12932  elpqb  12935  rpnnen1lem5  12940  cnref1o  12944  rpaddcl  12975  rpmulcl  12976  rpmtmip  12977  rpdivcl  12978  max1  13145  max2  13147  min1  13149  min2  13150  z2ge  13158  qbtwnxr  13160  xaddf  13184  rexadd  13192  rexsub  13193  xnn0xaddcl  13195  xaddcom  13200  xnn0xadd0  13207  xnegdi  13208  rexmul  13231  supxrbnd2  13282  ixxin  13323  elicc2  13372  difreicc  13445  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzval2  13471  elfz1eq  13496  peano2fzr  13498  fzn  13501  fzsplit2  13510  fzaddel  13519  fzadd2  13520  fzsubel  13521  fzrev2  13549  fzrev3  13551  uzsplit  13557  fznuz  13570  uznfz  13571  fzrevral  13573  fzrevral3  13575  fzshftral  13576  elfz2nn0  13579  fznn0sub2  13596  fz0fzdiffz0  13598  elfzmlbp  13600  difelfzle  13602  difelfznle  13603  elfzouz2  13635  fzo0n  13642  fzouzsplit  13655  fzoun  13657  elfzo0le  13664  fzonmapblen  13669  fzofzim  13670  fzoaddel2  13681  eluzgtdifelfzo  13688  elfzodifsumelfzo  13692  ssfzoulel  13721  ubmelm1fzo  13724  fzofzp1b  13726  elfzonelfzo  13730  elfznelfzo  13733  fzostep1  13744  injresinjlem  13748  subfzo0  13750  flflp1  13769  divfl0  13786  flzadd  13788  flmulnn0  13789  fldivnn0le  13794  fldiv  13822  uzsup  13825  mulmod0  13839  modlt  13842  modmulnn  13851  zmodcl  13853  zmodfz  13855  zmodid2  13861  modcyc  13868  muladdmodid  13875  modmuladdnn0  13880  negmod  13881  addmodidr  13885  modadd2mod  13886  modaddmodup  13899  modaddmulmod  13903  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  om2uzlti  13915  om2uzf1oi  13918  fzen2  13934  ssnn0fi  13950  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub0  13958  seqshft2  13993  seqsplit  14000  seqcaopr2  14003  seqf1olem2  14007  expcllem  14037  expcl2lem  14038  1exp  14056  expge1  14064  expadd  14069  expmul  14072  expsub  14075  nn0sq11  14097  lt2sq  14098  le2sq  14099  expmordi  14132  leexp2  14136  leexp1a  14140  sumsqeq0  14144  bernneq  14194  bernneq2  14195  expnbnd  14197  digit2  14201  digit1  14202  facdiv  14252  facwordi  14254  faclbnd  14255  faclbnd3  14257  faclbnd4lem4  14261  faclbnd5  14263  faclbnd6  14264  facavg  14266  bcrpcl  14273  bccmpl  14274  bcval5  14283  hashen  14312  hasheqf1oi  14316  hashgadd  14342  hashdom  14344  hashsdom  14346  hashun  14347  hashunsnggt  14359  hashprg  14360  hashssdif  14377  hashxplem  14398  seqcoll  14429  tpf1o  14466  eqwrd  14522  ccatfval  14538  ccatlen  14540  ccat0  14541  elfzelfzccat  14545  ccatsymb  14547  ccatval21sw  14550  ccatrn  14554  lswccatn0lsw  14556  ccatalpha  14558  ccatrcl1  14559  ccats1alpha  14584  swrdnd  14619  swrdfv2  14626  swrdsbslen  14629  swrdspsleq  14630  swrdccat2  14634  pfxnd0  14653  addlenrevpfx  14655  pfxeq  14661  ccatpfx  14666  pfxccat1  14667  swrdswrdlem  14669  pfxswrd  14671  pfxccatin12lem4  14691  pfxccatin12lem1  14693  pfxccatin12lem2  14696  pfxccatin12lem3  14697  pfxccatin12  14698  pfxccat3  14699  swrdccat  14700  pfxccatpfx2  14702  pfxccat3a  14703  swrdccat3blem  14704  swrdccat3b  14705  revccat  14731  revrev  14732  cshwlen  14764  cshwidxmod  14768  cshwidxmodr  14769  cshweqdif2  14784  cshweqrep  14786  2cshwcshw  14791  s3eq3seq  14905  cotr2g  14942  trclun  14980  shftf  15045  seqshft  15051  crre  15080  crim  15081  readd  15092  resub  15093  remul2  15096  imadd  15100  imsub  15101  immul2  15103  ipcnval  15109  cjsub  15115  cjreim  15126  01sqrexlem6  15213  sqrtle  15226  sqrt11  15228  absreimsq  15258  absreim  15259  absmul  15260  sqabs  15273  absdiflt  15284  absdifle  15285  abssuble0  15295  absmax  15296  abs2difabs  15301  fzomaxdif  15310  rexanuz  15312  rexuz3  15315  rexuzre  15319  caubnd2  15324  limsupgre  15447  limsupbnd2  15449  climconst2  15514  lo1resb  15530  o1resb  15532  2clim  15538  climshftlem  15540  climshft  15542  climshft2  15548  cjcn2  15566  o1of2  15579  o1rlimmul  15585  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  lo1le  15618  climlec2  15625  isershft  15630  isercolllem1  15631  isercolllem3  15633  isercoll  15634  isercoll2  15635  climsup  15636  caurcvg  15643  caucvg  15645  iseraltlem1  15648  iseraltlem2  15649  iseralt  15651  summolem2a  15681  isumclim3  15725  mptfzshft  15744  fsumrev  15745  fsum0diag2  15749  fsumconst  15756  telfsumo2  15769  fsumparts  15772  o1fsum  15779  cvgcmp  15782  cvgcmpub  15783  cvgcmpce  15784  binomlem  15795  binom1p  15797  binom1dif  15799  bcxmas  15801  incexclem  15802  incexc  15803  incexc2  15804  isumshft  15805  isumsplit  15806  isumsup2  15812  climcndslem1  15815  climcndslem2  15816  climcnds  15817  supcvg  15822  expcnv  15830  geoserg  15832  pwdif  15834  geolim  15836  geoisum1  15845  geoisum1c  15846  cvgrat  15849  mertenslem1  15850  mertenslem2  15851  mertens  15852  ntrivcvgfvn0  15865  ntrivcvgmullem  15867  prodmolem2a  15900  prodmo  15902  fprodf1o  15912  fproddiv  15927  fprodeq0  15941  risefacval2  15976  fallfacval2  15977  fallfacval3  15978  rprisefaccl  15989  risefallfac  15990  fallfacfwd  16002  binomfallfaclem1  16005  binomfallfaclem2  16006  binomrisefac  16008  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  efcj  16058  fprodefsum  16061  efexp  16069  eftlub  16077  effsumlt  16079  efle  16086  reef11  16087  efieq  16131  sinsub  16136  cossub  16137  subsin  16139  sinmul  16140  cosmul  16141  addcos  16142  subcos  16143  rpnnen2lem10  16191  rpnnen2lem12  16193  ruclem8  16205  ruclem12  16209  sqrt2irr  16217  dvdssub2  16271  dvdsadd  16272  dvdsaddr  16273  dvdssub  16274  dvdssubr  16275  dvdsle  16280  alzdvds  16290  fzocongeq  16294  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  pwp1fsum  16361  divalglem4  16366  divalglem9  16371  divalgb  16374  divalgmod  16376  ndvdsadd  16380  smueqlem  16460  gcdaddm  16495  modgcd  16502  bezoutlem1  16509  dvdsgcd  16514  absmulgcd  16519  rpmulgcd  16527  rprpwr  16529  sqgcd  16532  dvdssqlem  16536  dvdssq  16537  nn0seqcvgd  16540  algrf  16543  algcvg  16546  lcmcllem  16566  lcmabs  16575  lcmgcd  16577  lcmdvds  16578  lcmgcdnn  16581  lcmf  16603  coprmgcdb  16619  coprmdvds  16623  coprmdvds2  16624  qredeq  16627  isprm3  16653  nprm  16658  oddprmgt2  16669  isprm5  16677  isprm7  16678  divgcdodd  16680  prmdvdsexp  16685  zgcdsq  16723  hashdvds  16745  phiprmpw  16746  crth  16748  phimullem  16749  modprm0  16776  coprimeprodsq  16779  coprimeprodsq2  16780  pythagtriplem2  16788  pythagtriplem19  16804  iserodd  16806  pcpremul  16814  pcmul  16822  pcexp  16830  pcdvdsb  16840  pcneg  16845  pc2dvds  16850  pc11  16851  pcmpt  16863  fldivp1  16868  pcfac  16870  infpnlem1  16881  prmunb  16885  prmreclem1  16887  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  1arithlem4  16897  1arith  16898  gzaddcl  16908  gzmulcl  16909  gzreim  16910  gzsubcl  16911  4sqlem1  16919  4sqlem4a  16922  4sqlem4  16923  4sqlem12  16927  ramlb  16990  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem7  17028  prmgaplem8  17029  prmgapprmolem  17032  cshwshashlem2  17067  setsvalg  17136  ressval  17203  ressval3d  17216  restval  17389  pwsval  17449  xpsval  17533  ssclem  17781  rescval  17789  funcestrcsetclem9  18109  embedsetcestrclem  18118  lubel  18473  ipodrsima  18500  tsrss  18548  resmgmhm  18638  resmgmhm2  18639  mgmhmco  18641  submnd0  18690  mndinvmod  18691  xpsmnd0  18705  resmhm  18747  resmhm2  18748  mhmco  18750  frmdplusg  18781  frmdmnd  18786  efmndcl  18809  smndex1id  18838  mgm2nsgrplem1  18845  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem1  18850  sgrp2rid2  18853  dfgrp3  18971  mhmmnd  18996  mulgnngsum  19011  mulgnnsubcl  19018  mulgnn0z  19033  mulgnndir  19035  mulgmodid  19045  eqgfval  19108  cycsubgcl  19138  cycsubg2  19142  0ghm  19162  resghm  19164  resghm2  19165  ghmco  19168  ghmeql  19171  isgim  19194  gicsubgen  19211  cntzmhm  19273  symgcl  19315  symgextf1  19351  gsmsymgrfixlem1  19357  symgfixf1  19367  symgtrinv  19402  pmtrdifellem3  19408  mndodcongi  19473  odmod  19476  odf1  19492  odf1o1  19502  gexdvds  19514  sylow1lem1  19528  pgpssslw  19544  lsmub1  19587  lsmub2  19588  cntzrecd  19608  pj1ghm  19633  lsmhash  19635  efgred  19678  frgpup1  19705  ablsubadd23  19743  ablsubsub23  19754  mulgnn0di  19755  torsubg  19784  zaddablx  19802  gsumzaddlem  19851  gsumzadd  19852  gsumconst  19864  gsumzmhm  19867  telgsumfzslem  19918  dprdfadd  19952  dprd2dlem1  19973  ablsimpgfindlem1  20039  srgbinomlem3  20137  srgbinomlem4  20138  srgbinomlem  20139  gsummgp0  20227  gsumdixp  20228  xpsring1d  20242  unitnegcl  20306  isrnghm  20350  rnghmco  20366  dfrhm2  20383  rhmco  20410  c0rhm  20443  c0rnghm  20444  rhmimasubrng  20475  cntzsubrng  20476  issubrg3  20509  resrhm  20510  rhmeql  20512  rhmima  20513  isdomn4  20625  imadrhmcl  20706  fldsdrgfld  20707  abvres  20740  lmodfopne  20806  lspf  20880  lspcl  20882  0lmhm  20947  lmhmco  20950  lmhmeql  20962  islmim  20969  rngqiprngghm  21209  rngqiprnglin  21212  xrs1cmn  21323  xrsdsreval  21328  xrsdsreclb  21330  znfld  21470  znchr  21472  znunithash  21474  znrrg  21475  freshmansdream  21484  cnmsgnsubg  21486  zrhpsgnmhm  21493  evpmodpmf1o  21505  psgndiflemB  21509  psgndif  21511  phlssphl  21568  frlmval  21657  uvcfval  21693  frlmsslsp  21705  frlmup2  21708  lindfmm  21736  lmimlbs  21745  islindf4  21747  issubassa3  21775  psrbaglesupp  21831  psrcom  21877  resspsrmul  21885  mplsubrglem  21913  mplcoe3  21945  ltbval  21950  ltbwe  21951  evlslem4  21983  evlslem3  21987  psdmvr  22056  psropprmul  22122  coe1tmmul  22163  cply1mul  22183  gsummoncoe1  22195  lply1binomsc  22198  pf1ind  22242  mamufacex  22283  grpvlinv  22285  grpvrinv  22286  eqmat  22311  mat1dimcrng  22364  dmatcrng  22389  scmatf1  22418  m1detdiag  22484  mdetdiaglem  22485  mdet1  22488  mdetunilem9  22507  madulid  22532  gsummatr01lem4  22545  gsummatr01  22546  mat2pmatlin  22622  m2pmfzgsumcl  22635  monmatcollpw  22666  pmatcollpw3lem  22670  mp2pm2mplem4  22696  chpscmatgsummon  22732  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  cayhamlem1  22753  cpmadugsumlemF  22763  clsval2  22937  innei  23012  ordtrest  23089  ordtrestixx  23109  isnrm2  23245  lpcls  23251  tgcmp  23288  cmpcld  23289  uncmp  23290  hauscmplem  23293  hauscmp  23294  1stcfb  23332  1stcrest  23340  kgencmp2  23433  1stckgenlem  23440  kgen2ss  23442  kgencn  23443  kgencn3  23445  txval  23451  txuni2  23452  txbasex  23453  txbas  23454  txtop  23456  ptbasin  23464  txtopon  23478  txcld  23490  txss12  23492  txbasval  23493  xkoccn  23506  txcnp  23507  ptcnplem  23508  upxp  23510  txcnmpt  23511  uptx  23512  txrest  23518  txdis  23519  txindislem  23520  txlly  23523  txnlly  23524  txcmp  23530  hausdiag  23532  txhaus  23534  tx1stc  23537  tx2ndc  23538  txkgen  23539  xkoptsub  23541  cnmpt21  23558  txconn  23576  qtopval  23582  hmeoco  23659  txhmeo  23690  xpstopnlem1  23696  fbun  23727  filss  23740  infil  23750  fbunfip  23756  filuni  23772  fmfnfmlem4  23844  ufldom  23849  flffval  23876  flfval  23877  txflf  23893  fcfval  23920  alexsubALTlem3  23936  tgpmulg  23980  subgtgp  23992  qustgplem  24008  tsmsfbas  24015  tsmsres  24031  tsmsmhm  24033  tsmsadd  24034  isxmet2d  24215  blin2  24317  comet  24401  met2ndci  24410  metcn  24431  txmetcn  24436  dscopn  24461  nrmmetd  24462  isngp3  24486  tngval  24527  nm1  24555  subrgnrg  24561  nrginvrcn  24580  rlmnvc  24591  nmo0  24623  nmoco  24625  nghmco  24626  nmotri  24627  0nghm  24629  isnmhm2  24640  0nmhm  24643  nmhmco  24644  nmhmplusg  24645  qtopbaslem  24646  remetdval  24677  bl2ioo  24680  reperflem  24707  iccntr  24710  icccmplem2  24712  icccmp  24714  reconnlem2  24716  xrge0gsumle  24722  xrge0tsms  24723  divcnOLD  24757  divcn  24759  cncfmet  24802  iccpnfcnv  24842  bndth  24857  copco  24918  pcopt  24922  pcopt2  24923  nmhmcn  25020  cmodscexp  25021  cphassr  25112  lmmbrf  25162  lmnn  25163  iscauf  25180  caucfil  25183  iscmet3lem1  25191  iscmet3lem2  25192  iscmet3  25193  cfilres  25196  caussi  25197  caubl  25208  caublcls  25209  bcthlem2  25225  bcthlem5  25228  cmsss  25251  lssbn  25252  ovolfioo  25368  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliunlem2  25404  ovoliunlem3  25405  ovoliun2  25407  ovolscalem1  25414  ovolicc2lem1  25418  ovolicc2lem4  25421  ovolicc2lem5  25422  inmbl  25443  voliunlem1  25451  volsup  25457  ioombl1lem4  25462  iccvolcl  25468  ioovolcl  25471  uniioovol  25480  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  dyadf  25492  dyadovol  25494  dyadss  25495  dyadmbl  25501  opnmbllem  25502  volsup2  25506  volcn  25507  ismbf  25529  mbfima  25531  ismbf3d  25555  mbfadd  25562  mbfsub  25563  mbflimsup  25567  itg1mulc  25605  itg1sub  25610  itg1climres  25615  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfmul  25627  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2lea  25645  itg2eqa  25646  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  itg2cnlem1  25662  bddmulibl  25740  ellimc3  25780  dvaddbr  25840  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvcnvlem  25880  c1lip1  25902  lhop  25921  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumrlimf  25931  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  tdeglem4  25965  deg1ge  26003  coe1mul3  26004  fta1g  26075  plyco0  26097  plyf  26103  ply1termlem  26108  plyeq0lem  26115  plypf1  26117  plymullem1  26119  plyaddlem  26120  plymullem  26121  coeeulem  26129  coeidlem  26142  plyco  26146  dgreq  26149  coefv0  26153  coeaddlem  26154  coemullem  26155  coemulhi  26159  coemulc  26160  plycn  26166  plycnOLD  26167  dgrlt  26172  dgrsub  26178  plycjlem  26182  plycj  26183  plycjOLD  26185  plyrecj  26187  plymul0or  26188  plyreres  26190  dvply1  26191  vieta1lem2  26219  plyexmo  26221  elqaalem2  26228  elqaalem3  26229  aareccl  26234  aalioulem1  26240  aalioulem3  26242  aaliou  26246  geolim3  26247  ulmcaulem  26303  ulmcau  26304  mtest  26313  dvradcnv  26330  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv2  26340  abelthlem6  26346  abelthlem8  26349  abelthlem9  26350  reeff1o  26357  reefgim  26360  sinperlem  26389  sincosq2sgn  26408  sincosq3sgn  26409  sinq12ge0  26417  sincos6thpi  26425  sineq0  26433  cosord  26440  cos11  26442  sinord  26443  tanord1  26446  eff1olem  26457  logrnaddcl  26483  relogeftb  26493  relogoprlem  26500  logleb  26512  advlogexp  26564  logtayllem  26568  logtayl  26569  logtaylsum  26570  logtayl2  26571  recxpcl  26584  rpcxpcl  26585  cxple3  26610  cxpcom  26648  cxpcn3  26658  cxpeq  26667  relogbmul  26687  relogbcxp  26695  relogbf  26701  atanord  26837  atantayl  26847  birthdaylem2  26862  birthdaylem3  26863  cxp2limlem  26886  fsumharmonic  26922  zetacvg  26925  ftalem1  26983  ftalem4  26986  ftalem5  26987  basellem2  26992  basellem3  26993  basellem4  26994  vmappw  27026  sqf11  27049  mumul  27091  fsumdvdscom  27095  dvdsppwf1o  27096  dvdsflf1o  27097  musum  27101  muinv  27103  fsumdvdsmul  27105  1sgmprm  27110  vmalelog  27116  chtublem  27122  fsumvma  27124  vmasum  27127  logfac2  27128  chpval2  27129  logfaclbnd  27133  logexprlim  27136  mersenne  27138  dchrmulcl  27160  dchrinvcl  27164  dchrfi  27166  dchrghm  27167  dchrptlem1  27175  dchrsum2  27179  dchrsum  27180  pcbcctr  27187  bcmono  27188  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem5  27199  bposlem6  27200  bposlem7  27201  lgslem3  27210  lgscllem  27215  lgsval4a  27230  lgsneg  27232  lgsdir2  27241  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  gausslemma2dlem6  27283  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2  27297  lgsquad3  27298  2lgslem1a1  27300  2lgslem1a  27302  2lgslem1c  27304  2sqlem2  27329  mul2sq  27330  2sqlem7  27335  2sqreultlem  27358  2sqreunnltlem  27361  2sqreunnltblem  27362  chebbnd1lem1  27380  vmadivsum  27393  rplogsumlem2  27396  dchrisum0lem1a  27397  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  dchrisum0ff  27418  dchrisum0flblem1  27419  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  mudivsum  27441  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  selberglem2  27457  selberg2  27462  chpdifbndlem1  27464  selberg3lem1  27468  pntrsumbnd2  27478  selbergr  27479  pntpbnd1  27497  pntpbnd2  27498  pntlemh  27510  pntlemj  27514  pntlemi  27515  pntlemf  27516  pntlemp  27521  ostth2lem1  27529  ostth1  27544  ostth2lem3  27546  ostth3  27549  noreson  27572  nosepon  27577  noextendseq  27579  nosupbnd1lem5  27624  noetasuplem4  27648  addscom  27873  negsdi  27956  om2noseqlt  28193  om2noseqf1o  28195  n0s0suc  28234  nnsge1  28235  n0sbday  28244  n0sfincut  28246  n0sltp1le  28255  bdayn0sf1o  28259  zaddscl  28282  elzn0s  28286  zseo  28308  remulscllem2  28352  istrkg2ld  28387  isismt  28461  eedimeq  28825  eqeefv  28830  brbtwn2  28832  colinearalglem1  28833  colinearalglem2  28834  colinearalg  28837  eleesub  28838  eleesubd  28839  axcgrrflx  28841  axcgrid  28843  axsegconlem2  28845  axsegconlem7  28850  axsegconlem9  28852  axsegconlem10  28853  axlowdimlem14  28882  axlowdimlem16  28884  axlowdimlem17  28885  axcontlem2  28892  axcontlem4  28894  axcontlem8  28898  axcontlem10  28900  structiedg0val  28949  upgr1eop  29042  numedglnl  29071  usgredg2v  29154  ushgredgedg  29156  ushgredgedgloop  29158  uspgr1eop  29174  usgr1eop  29177  uhgrissubgr  29202  umgrres1lem  29237  upgrres1  29240  nbuhgr  29270  edgnbusgreu  29294  nb3gr2nb  29311  uvtxnm1nbgr  29331  cusgrexilem2  29369  finsumvtxdg2ssteplem4  29476  vtxdgoddnumeven  29481  wlkeq  29562  uspgr2wlkeq  29574  wlksoneq1eq2  29592  upgrwlkdvdelem  29666  usgr2wlkspthlem1  29687  usgrn2cycl  29739  crctcshwlkn0lem3  29742  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  crctcshwlkn0  29751  wspthneq1eq2  29790  wwlkseq  29821  wwlksnext  29823  rusgrnumwlkg  29907  clwwlkccatlem  29918  clwwlkccat  29919  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  clwlkclwwlkf1lem3  29935  clwwisshclwwslemlem  29942  clwwisshclwws  29944  erclwwlkeqlen  29948  erclwwlkref  29949  clwwnisshclwwsn  29988  clwwlknccat  29992  erclwwlkneqlen  29997  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwlksndivn  30015  uhgr3cyclex  30111  eucrctshift  30172  eucrct2eupth  30174  frgreu  30197  frgr3v  30204  3vfriswmgr  30207  frgrncvvdeqlem3  30230  frgrregorufrg  30255  numclwwlk1lem2f1  30286  numclwwlk1lem2fo  30287  numclwlk1lem2  30299  numclwwlk3  30314  numclwwlk6  30319  frgrreg  30323  frgrregord013  30324  nsnlplig  30410  nsnlpligALT  30411  ablodivdiv4  30483  imsdval  30615  nmcvcn  30624  sspval  30652  lnoadd  30687  lnosub  30688  nmooge0  30696  nmoolb  30700  nmoub3i  30702  blocnilem  30733  blocni  30734  cncph  30748  ipasslem1  30760  ipasslem2  30761  ipasslem4  30763  ipasslem11  30769  ipblnfi  30784  phoeqi  30786  ubthlem1  30799  ubthlem3  30801  htthlem  30846  hvsub4  30966  his7  31019  his2sub2  31022  hial2eq2  31036  hhip  31106  hhph  31107  bcs2  31111  hhssabloi  31191  hhssnv  31193  ocorth  31220  shsel  31243  shsel3  31244  shscli  31246  chsupss  31271  shjval  31280  chjval  31281  shjcl  31285  chjcl  31286  shsleji  31299  chslej  31427  chsscon2  31431  chjcom  31435  chub1  31436  chdmj1  31458  spanunsni  31508  spanpr  31509  fh1  31547  fh2  31548  cm2j  31549  spansncvi  31581  5oalem1  31583  5oalem3  31585  5oalem5  31587  3oalem2  31592  pjcompi  31601  pjds3i  31642  hoeq  31689  hoadddi  31732  hoadddir  31733  hosubdi  31737  hosub4  31742  hoeq1  31759  hoeq2  31760  adjval2  31820  counop  31850  adjeq  31864  brafnmul  31880  lnopsubi  31903  hmops  31949  hmopm  31950  hmopd  31951  hmopco  31952  nmcopexi  31956  lnconi  31962  lnfnsubi  31975  nmcfnexi  31980  imaelshi  31987  nlelshi  31989  riesz3i  31991  riesz1  31994  cnlnadjlem2  31997  cnlnadjlem6  32001  adjbdln  32012  adjlnop  32015  adjmul  32021  adjadd  32022  nmopcoi  32024  rnbra  32036  cnvbramul  32044  kbass2  32046  kbass4  32048  kbass5  32049  kbass6  32050  leopadd  32061  leopmul2i  32064  leoptri  32065  dmdmd  32229  mddmd  32230  cvdmd  32266  superpos  32283  chrelati  32293  atcv0eq  32308  atomli  32311  atcvatlem  32314  atcvati  32315  atcvat2i  32316  chirredlem4  32322  atcvat3i  32325  atcvat4i  32326  mdsymlem2  32333  mdsymlem3  32334  mdsymlem5  32336  mdsymlem8  32339  dmdsym  32342  cdjreui  32361  cdj1i  32362  cdj3lem2b  32366  cdj3lem3  32367  cdj3lem3b  32369  cdj3i  32370  brabgaf  32536  prct  32638  fcobijfs  32646  fzsplit3  32716  bcm1n  32718  dpfrac1  32812  wrdres  32856  xrge0mulgnn0  32956  xrge0tsmsd  33002  xrge0omnd  33025  cycpmco2  33090  suborng  33293  isarchiofld  33295  resvval  33301  nsgqusf1olem2  33385  lbslsat  33612  ply1degltdimlem  33618  ply1degltdim  33619  ordtrestNEW  33911  mhmhmeotmd  33917  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0pluscn  33930  hasheuni  34075  sxval  34180  measvuni  34204  ddemeas  34226  br2base  34260  dya2iocucvr  34275  sxbrsigalem2  34277  sxbrsiga  34281  omssubadd  34291  eulerpartlemgc  34353  ballotlemfc0  34484  ballotlemfcc  34485  signstfvc  34565  signstres  34566  signsvfn  34573  bnj563  34733  bnj554  34889  bnj557  34891  bnj570  34895  bnj594  34902  bnj849  34915  bnj970  34937  bnj1118  34974  bnj1145  34983  bnj1190  34998  bnj1398  35024  bnj1417  35031  zltp1ne  35097  nnltp1ne  35098  nn0ltp1ne  35099  0nn0m1nnn0  35100  cusgr3cyclex  35123  derangsn  35157  derangen  35159  subfacp1lem5  35171  erdsze2lem1  35190  txpconn  35219  txsconn  35228  cvmliftphtlem  35304  satfdm  35356  satfun  35398  ex-sategoelel  35408  mrsubff1  35501  msubff  35517  msubff1  35543  msubvrs  35547  inffz  35717  bcprod  35725  bccolsum  35726  faclim  35733  dfon2lem4  35774  colineardim1  36049  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem12  36086  btwnconn1lem13  36087  btwnconn1lem14  36088  outsideofeu  36119  funray  36128  lineintmo  36145  fwddifnp1  36153  hfun  36166  nn0prpw  36311  opnregcld  36318  cldregopn  36319  ivthALT  36323  onsucconni  36425  bj-nnfim1  36732  bj-nnfim2  36733  bj-2uplex  37010  bj-unexg  37026  bj-prexg  37027  bj-idres  37148  isbasisrelowllem1  37343  isbasisrelowllem2  37344  icoreclin  37345  relowlssretop  37351  exrecfnlem  37367  pibt2  37405  unccur  37597  phpreu  37598  finixpnum  37599  ltflcei  37602  cos2h  37605  lindsadd  37607  lindsdom  37608  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  heicant  37649  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  ovoliunnfl  37656  mbfresfi  37660  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  indexa  37727  incsequz  37742  incsequz2  37743  geomcau  37753  sstotbnd2  37768  prdsbnd  37787  prdstotbnd  37788  prdsbnd2  37789  cntotbnd  37790  ismtyhmeolem  37798  ismtybndlem  37800  heibor1lem  37803  heiborlem3  37807  heiborlem6  37810  heibor  37815  bfplem1  37816  bfplem2  37817  elghomlem1OLD  37879  rngogrphom  37965  prnc  38061  ispridlc  38064  pridlc3  38067  mpobi123f  38156  mptbi12f  38160  antisymressn  38435  eqvreltr  38598  ax12indalem  38938  lsateln0  38988  atlatmstc  39312  hlatjidm  39362  llnneat  39508  lplnneat  39539  lplnnelln  39540  lvolneatN  39582  lvolnelln  39583  lvolnelpln  39584  dalem23  39690  snatpsubN  39744  linepsubN  39746  pmapsub  39762  pmapglbx  39763  paddasslem14  39827  polsubN  39901  pol1N  39904  2polvalN  39908  2polssN  39909  3polN  39910  2pmaplubN  39920  polatN  39925  2polatN  39926  pnonsingN  39927  polsubclN  39946  lautco  40091  cdlemefrs29cpre1  40392  dian0  41033  dia0eldmN  41034  dia1eldmN  41035  dia0  41046  dia1N  41047  dvhopaddN  41108  dib0  41158  dih0  41274  dih1  41280  dihglblem5apreN  41285  dihatexv2  41333  dochfN  41350  lcmineqlem1  42017  lcmineqlem17  42033  xppss12  42217  sumcubes  42301  dvdsexpnn  42321  remul01  42395  resubeqsub  42418  ricdrng1  42516  prjspeclsp  42600  ismrcd2  42687  nacsfix  42700  mzpaddmpt  42729  mzpmulmpt  42730  eq0rabdioph  42764  lerabdioph  42793  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  fiphp3d  42807  congneg  42958  jm2.22  42984  jm2.23  42985  jm2.15nn0  42992  jm3.1  43009  aomclem8  43050  lsmfgcl  43063  lmhmfgima  43073  lnmepi  43074  dgrsub2  43124  mpaaeu  43139  mendring  43177  proot1ex  43185  unielss  43207  onsucwordi  43277  oaabsb  43283  rp-oelim2  43297  nnoeomeqom  43301  cantnfresb  43313  oawordex2  43315  omcl3g  43323  ordsssucb  43324  tfsconcatrev  43337  onsucunipr  43361  onsucunitp  43362  oaun3lem1  43363  naddgeoa  43383  oaltom  43394  minregex2  43524  sssymdifcl  43561  relexp01min  43702  ntrclsiso  44056  ntrclsk3  44059  cvgdvgrat  44302  nznngen  44305  uzmptshftfval  44335  addrval  44455  subrval  44456  mulvval  44457  elpwgded  44554  eel2131  44703  eel3132  44704  el12  44715  sspwimp  44907  sspwimpcf  44909  suctrALTcf  44911  suctrALT3  44913  relpfrlem  44943  cnfex  45022  disjinfi  45186  infxrbnd2  45365  supminfxr  45460  climinf  45604  lptre2pt  45638  limcresiooub  45640  limcresioolb  45641  addlimc  45646  limclner  45649  limsuppnflem  45708  limsupmnfuzlem  45724  limsupvaluz2  45736  limsupresxr  45764  liminfresxr  45765  cnrefiisplem  45827  cncfdmsn  45888  iblspltprt  45971  itgspltprt  45977  dirkertrigeqlem3  46098  fourierdlem62  46166  fourierdlem80  46184  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0f1o  46380  hoidmvlelem2  46594  pimdecfgtioo  46715  smfliminflem  46828  fnresfnco  47042  fcores  47068  dfatcolem  47256  nn0resubcl  47309  zgeltp1eq  47310  eluzge0nn0  47313  fz0addcom  47318  elfzlble  47321  fzopredsuc  47324  subsubelfzo0  47327  ceilbi  47334  minusmod5ne  47350  submodlt  47351  mod0mul  47357  m1modmmod  47359  uniimafveqt  47382  fundcmpsurinjimaid  47412  icceuelpartlem  47436  iccpartnel  47439  elsprel  47476  fmtnodvds  47545  goldbachth  47548  fmtnoprmfac2  47568  prmdvdsfmtnof1  47588  2pwp1prm  47590  flsqrt  47594  lighneallem4  47611  dfodd6  47638  divgcdoddALTV  47683  opoeALTV  47684  opeoALTV  47685  omoeALTV  47686  omeoALTV  47687  epoo  47704  emoo  47705  epee  47706  emee  47707  evensumeven  47708  even3prm2  47720  mogoldbblem  47721  fpprmod  47728  dfwppr  47739  fpprwppr  47740  fpprwpprb  47741  gbepos  47759  gbegt5  47762  gbowgt5  47763  gboge9  47765  sbgoldbst  47779  nnsum3primesgbe  47793  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  grimco  47889  isuspgrim0  47894  isuspgrimlem  47895  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrim  47934  grimedg  47935  isgrtri  47942  cycl3grtri  47946  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlimlem4  47990  grlictr  48007  gpgusgralem  48047  gpgedg2ov  48057  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg5grlic  48084  2zrngmmgm  48240  2zrngnmrid  48244  2zrngnmlid2  48245  altgsumbc  48340  altgsumbcALT  48341  zlmodzxzadd  48346  zlmodzxzsub  48348  invginvrid  48355  ply1mulgsumlem2  48376  ply1mulgsum  48379  lincvalpr  48407  lindslinindimp2lem1  48447  ldepsprlem  48461  ldepspr  48462  lincresunit3lem3  48463  lincresunitlem1  48464  lincresunit3lem1  48468  lincresunit3  48470  elfzolborelfzop1  48508  zgtp1leeq  48510  flsubz  48511  nneom  48516  nn0ofldiv2  48521  rege1logbrege0  48547  nnpw2pb  48576  dignn0fr  48590  dignn0ldlem  48591  dignnld  48592  dignn0flhalflem1  48604  nn0sumshdiglemB  48609  nn0mulfsum  48613  rrx2plordisom  48712  ehl2eudis0lt  48715  itsclinecirc0in  48764  2itscp  48770  inlinecirc02plem  48775  mof0ALT  48828  i0oii  48908  resccat  49063