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  2375  nfeqf  2381  eqeqan12dALT  2750  sylan9eq  2786  sylan9ss  3943  ssconb  4089  ineqan12d  4169  ifpr  4643  disjtp2  4666  dfopg  4820  disjxiun  5086  breqan12d  5105  eusv1  5327  opelvvg  5655  opthprc  5678  relop  5789  dmpropg  6162  unixp  6229  tz7.7  6332  ordin  6336  onin  6337  ontri1  6340  onfr  6345  onelpss  6346  onsseleq  6347  oneltri  6349  ontr2  6354  onunel  6413  onun2  6416  funssres  6525  funtpg  6536  funtp  6538  resasplit  6693  fodmrnu  6743  f1un  6783  dffv2  6917  fvreseq0  6971  fvcofneq  7026  funopdmsn  7083  fprg  7088  fprb  7128  fconst2g  7137  isofrlem  7274  oveqan12d  7365  ov3  7509  ovg  7511  ovima0  7525  f1opw2  7601  off  7628  unexgOLD  7682  pwuncl  7703  epweon  7708  epweonALT  7709  sucexeloni  7742  ordunpr  7756  omun  7818  peano4  7822  fabexg  7868  f1oabexg  7872  fiun  7875  offres  7915  el2mpocsbcl  8015  curry1  8034  curry1val  8035  curry2  8037  curry2val  8039  soxp  8059  wexp  8060  xpord2pred  8075  poxp3  8080  poseq  8088  soseq  8089  suppfnss  8119  frrlem4  8219  frrlem11  8226  frrlem12  8227  fprlem1  8230  iunon  8259  onfununi  8261  tfrlem11  8307  tz7.48lem  8360  seqomeq12  8373  oacan  8463  oawordri  8465  oaass  8476  omord2  8482  omcan  8484  oen0  8501  oeordi  8502  oeord  8503  oecan  8504  oeworde  8508  oeordsuc  8509  oelimcl  8515  nnawordi  8536  nnaword  8542  nnmord  8547  oaabslem  8562  omabslem  8565  omsmo  8573  eldifsucnn  8579  naddcllem  8591  naddov2  8594  ertr  8637  erex  8646  brecop  8734  ecopovtrn  8744  ecovdi  8749  mapvalg  8760  pmvalg  8761  pmss12g  8793  elmapresaun  8804  boxcutc  8865  undom  8978  sbthlem7  9006  sbth  9010  sdomnsym  9015  sdomdomtr  9023  xpf1o  9052  xpen  9053  limenpsi  9065  pssnn  9078  pwssfi  9086  sbthfi  9108  php2  9117  php3  9118  phpeqd  9121  nndomog  9122  onomeneq  9123  isinf  9149  fineqvlem  9150  f1finf1o  9157  dif1ennnALT  9161  findcard3  9167  unblem2  9177  isfinite2  9182  unfilem1  9189  unfi2  9194  fodomfir  9212  unifi2  9229  f1opwfi  9240  fsuppxpfi  9269  fsuppunbi  9273  fsuppco2  9287  fsuppcor  9288  fival  9296  fiin  9306  ordiso  9402  ordtypelem10  9413  hartogslem1  9428  wofib  9431  brwdom3  9468  unwdomg  9470  xpwdomg  9471  sucprcreg  9490  preleqALT  9507  inf3lem6  9523  oemapval  9573  cantnf  9583  wemapwe  9587  cnfcom  9590  ttrcltr  9606  dfttrcl2  9614  frmin  9642  r111  9668  r1ord3g  9672  prwf  9704  r1pw  9738  rankprb  9744  rankxplim  9772  tcrank  9777  updjud  9827  finnum  9841  xpnum  9844  carduni  9874  nnsdomel  9883  fidomtri  9886  infxpenlem  9904  fseqdom  9917  onssnum  9931  acndom2  9945  alephinit  9986  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem6  10047  undjudom  10059  endjudisj  10060  djuen  10061  djucomen  10069  pwdjuen  10073  djudom1  10074  djuxpdom  10077  djufi  10078  cardadju  10086  nnadju  10089  nnadjuALT  10090  ficardadju  10091  ficardun  10092  ficardun2  10093  pwsdompw  10094  unctb  10095  ackbij2lem1  10109  ackbij1lem6  10115  ackbij1lem16  10125  ackbij1b  10129  ackbij2  10133  coflim  10152  cflim2  10154  cofsmo  10160  coftr  10164  sornom  10168  infpssrlem5  10198  fin4en1  10200  fin23lem23  10217  fin23lem28  10231  isf32lem2  10245  isf32lem4  10247  isf32lem7  10250  isf34lem7  10270  isf34lem6  10271  fin67  10286  isfin7-2  10287  fin1a2lem9  10299  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  zorn2lem6  10392  ttukeylem3  10402  brdom6disj  10423  carddom  10445  cardsdom  10446  domtri  10447  konigthlem  10459  iunctb  10465  alephadd  10468  alephmul  10469  pwcfsdom  10474  cfpwsdom  10475  fpwwe2lem12  10533  canthp1lem2  10544  pwfseqlem3  10551  pwfseqlem4a  10552  inar1  10666  tskcard  10672  tskuni  10674  grur1  10711  mulclpi  10784  addcompi  10785  mulcompi  10787  distrpi  10789  ltexpi  10793  ltapi  10794  ltmpi  10795  enqbreq2  10811  nqereu  10820  addpipq  10828  addpqnq  10829  mulpipq  10831  mulpqnq  10832  addpqf  10835  addclnq  10836  mulpqf  10837  mulclnq  10838  adderpq  10847  mulerpq  10848  ltsonq  10860  lterpq  10861  ltbtwnnq  10869  ltrnq  10870  genpv  10890  genpdm  10893  genpnnp  10896  mulclprlem  10910  distrlem1pr  10916  distrlem4pr  10917  prlem934  10924  addcanpr  10937  suplem1pr  10943  mulcmpblnr  10962  mulclsr  10975  mulasssr  10981  distrsr  10982  ltsosr  10985  1idsr  10989  00sr  10990  recexsrlem  10994  mulgt0sr  10996  addcnsr  11026  axmulf  11037  axmulass  11048  axdistr  11049  axcnre  11055  mulrid  11110  axltadd  11186  lenlt  11191  dedekind  11276  dedekindle  11277  resubcl  11425  subeqrev  11539  muladd  11549  mulsub  11560  mulsub2  11561  ltaddsub2  11592  leaddsub2  11594  leltadd  11601  ltaddpos2  11608  posdif  11610  addge02  11628  mullt0  11636  ltord1  11643  leord1  11644  eqord1  11645  recextlem1  11747  recex  11749  divmuldiv  11821  conjmul  11838  div2sub  11946  prodgt02  11969  lemul2  11974  lemul2a  11976  ltmulgt12  11982  lemulge12  11985  mulge0b  11992  mulle0b  11993  ltmuldiv2  11996  ltdivmul2  11999  lt2mul2div  12000  ledivmul2  12001  lemuldiv2  12003  ledivdiv  12011  lediv2  12012  ltdiv23  12013  lediv23  12014  supmul  12094  riotaneg  12101  negiso  12102  cju  12121  nnaddcl  12148  nnmulcl  12149  nnmtmip  12151  nnsub  12169  addltmul  12357  avgle1  12361  avgle2  12362  avgle  12363  nnrecl  12379  nn0nnaddcl  12412  nn0sub  12431  elz2  12486  zaddcl  12512  zsubcl  12514  znnsub  12518  znn0sub  12519  nzadd  12520  zmulcl  12521  zltp1le  12522  zleltp1  12523  nnleltp1  12528  nnltp1le  12529  nnaddm1cl  12530  nn0ltp1le  12531  nn0leltp1  12532  nn0ltlem1  12533  nn0lem1lt  12538  nnlem1lt  12539  nnltlem1  12540  zdiv  12543  zextle  12546  zextlt  12547  btwnnz  12549  prime  12554  nneo  12557  peano2uz2  12561  uzind  12565  fzind  12571  zriotaneg  12586  uzneg  12752  uztric  12756  uz11  12757  eluzp1m1  12758  eluzp1p1  12760  uzin  12772  uzwo  12809  indstr  12814  uz2mulcl  12824  supminf  12833  uzsupss  12838  zmax  12843  rebtwnz  12845  qre  12851  qaddcl  12863  qsubcl  12866  irradd  12871  elpqb  12874  rpnnen1lem5  12879  cnref1o  12883  rpaddcl  12914  rpmulcl  12915  rpmtmip  12916  rpdivcl  12917  max1  13084  max2  13086  min1  13088  min2  13089  z2ge  13097  qbtwnxr  13099  xaddf  13123  rexadd  13131  rexsub  13132  xnn0xaddcl  13134  xaddcom  13139  xnn0xadd0  13146  xnegdi  13147  rexmul  13170  supxrbnd2  13221  ixxin  13262  elicc2  13311  difreicc  13384  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  fzval2  13410  elfz1eq  13435  peano2fzr  13437  fzn  13440  fzsplit2  13449  fzaddel  13458  fzadd2  13459  fzsubel  13460  fzrev2  13488  fzrev3  13490  uzsplit  13496  fznuz  13509  uznfz  13510  fzrevral  13512  fzrevral3  13514  fzshftral  13515  elfz2nn0  13518  fznn0sub2  13535  fz0fzdiffz0  13537  elfzmlbp  13539  difelfzle  13541  difelfznle  13542  elfzouz2  13574  fzo0n  13581  fzouzsplit  13594  fzoun  13596  elfzo0le  13603  fzonmapblen  13608  fzofzim  13609  fzoaddel2  13620  eluzgtdifelfzo  13627  elfzodifsumelfzo  13631  ssfzoulel  13660  ubmelm1fzo  13663  fzofzp1b  13665  elfzonelfzo  13669  elfznelfzo  13673  fzostep1  13686  injresinjlem  13690  subfzo0  13692  flflp1  13711  divfl0  13728  flzadd  13730  flmulnn0  13731  fldivnn0le  13736  fldiv  13764  uzsup  13767  mulmod0  13781  modlt  13784  modmulnn  13793  zmodcl  13795  zmodfz  13797  zmodid2  13803  modcyc  13810  muladdmodid  13817  modmuladdnn0  13822  negmod  13823  addmodidr  13827  modadd2mod  13828  modaddmodup  13841  modaddmulmod  13845  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  om2uzlti  13857  om2uzf1oi  13860  fzen2  13876  ssnn0fi  13892  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub0  13900  seqshft2  13935  seqsplit  13942  seqcaopr2  13945  seqf1olem2  13949  expcllem  13979  expcl2lem  13980  1exp  13998  expge1  14006  expadd  14011  expmul  14014  expsub  14017  nn0sq11  14039  lt2sq  14040  le2sq  14041  expmordi  14074  leexp2  14078  leexp1a  14082  sumsqeq0  14086  bernneq  14136  bernneq2  14137  expnbnd  14139  digit2  14143  digit1  14144  facdiv  14194  facwordi  14196  faclbnd  14197  faclbnd3  14199  faclbnd4lem4  14203  faclbnd5  14205  faclbnd6  14206  facavg  14208  bcrpcl  14215  bccmpl  14216  bcval5  14225  hashen  14254  hasheqf1oi  14258  hashgadd  14284  hashdom  14286  hashsdom  14288  hashun  14289  hashunsnggt  14301  hashprg  14302  hashssdif  14319  hashxplem  14340  seqcoll  14371  tpf1o  14408  eqwrd  14464  ccatfval  14480  ccatlen  14482  ccat0  14483  elfzelfzccat  14487  ccatsymb  14490  ccatval21sw  14493  ccatrn  14497  lswccatn0lsw  14499  ccatalpha  14501  ccatrcl1  14502  ccats1alpha  14527  swrdnd  14562  swrdfv2  14569  swrdsbslen  14572  swrdspsleq  14573  swrdccat2  14577  pfxnd0  14596  pfxeq  14603  ccatpfx  14608  pfxccat1  14609  swrdswrdlem  14611  pfxswrd  14613  pfxccatin12lem4  14633  pfxccatin12lem1  14635  pfxccatin12lem2  14638  pfxccatin12lem3  14639  pfxccatin12  14640  pfxccat3  14641  swrdccat  14642  pfxccatpfx2  14644  pfxccat3a  14645  swrdccat3blem  14646  swrdccat3b  14647  revccat  14673  revrev  14674  cshwlen  14706  cshwidxmod  14710  cshwidxmodr  14711  cshweqdif2  14726  cshweqrep  14728  2cshwcshw  14732  s3eq3seq  14846  cotr2g  14883  trclun  14921  shftf  14986  seqshft  14992  crre  15021  crim  15022  readd  15033  resub  15034  remul2  15037  imadd  15041  imsub  15042  immul2  15044  ipcnval  15050  cjsub  15056  cjreim  15067  01sqrexlem6  15154  sqrtle  15167  sqrt11  15169  absreimsq  15199  absreim  15200  absmul  15201  sqabs  15214  absdiflt  15225  absdifle  15226  abssuble0  15236  absmax  15237  abs2difabs  15242  fzomaxdif  15251  rexanuz  15253  rexuz3  15256  rexuzre  15260  caubnd2  15265  limsupgre  15388  limsupbnd2  15390  climconst2  15455  lo1resb  15471  o1resb  15473  2clim  15479  climshftlem  15481  climshft  15483  climshft2  15489  cjcn2  15507  o1of2  15520  o1rlimmul  15526  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  lo1le  15559  climlec2  15566  isershft  15571  isercolllem1  15572  isercolllem3  15574  isercoll  15575  isercoll2  15576  climsup  15577  caurcvg  15584  caucvg  15586  iseraltlem1  15589  iseraltlem2  15590  iseralt  15592  summolem2a  15622  isumclim3  15666  mptfzshft  15685  fsumrev  15686  fsum0diag2  15690  fsumconst  15697  telfsumo2  15710  fsumparts  15713  o1fsum  15720  cvgcmp  15723  cvgcmpub  15724  cvgcmpce  15725  binomlem  15736  binom1p  15738  binom1dif  15740  bcxmas  15742  incexclem  15743  incexc  15744  incexc2  15745  isumshft  15746  isumsplit  15747  isumsup2  15753  climcndslem1  15756  climcndslem2  15757  climcnds  15758  supcvg  15763  expcnv  15771  geoserg  15773  pwdif  15775  geolim  15777  geoisum1  15786  geoisum1c  15787  cvgrat  15790  mertenslem1  15791  mertenslem2  15792  mertens  15793  ntrivcvgfvn0  15806  ntrivcvgmullem  15808  prodmolem2a  15841  prodmo  15843  fprodf1o  15853  fproddiv  15868  fprodeq0  15882  risefacval2  15917  fallfacval2  15918  fallfacval3  15919  rprisefaccl  15930  risefallfac  15931  fallfacfwd  15943  binomfallfaclem1  15946  binomfallfaclem2  15947  binomrisefac  15949  bpolycl  15959  bpolysum  15960  bpolydiflem  15961  fsumkthpow  15963  efcj  15999  fprodefsum  16002  efexp  16010  eftlub  16018  effsumlt  16020  efle  16027  reef11  16028  efieq  16072  sinsub  16077  cossub  16078  subsin  16080  sinmul  16081  cosmul  16082  addcos  16083  subcos  16084  rpnnen2lem10  16132  rpnnen2lem12  16134  ruclem8  16146  ruclem12  16150  sqrt2irr  16158  dvdssub2  16212  dvdsadd  16213  dvdsaddr  16214  dvdssub  16215  dvdssubr  16216  dvdsle  16221  alzdvds  16231  fzocongeq  16235  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  pwp1fsum  16302  divalglem4  16307  divalglem9  16312  divalgb  16315  divalgmod  16317  ndvdsadd  16321  smueqlem  16401  gcdaddm  16436  modgcd  16443  bezoutlem1  16450  dvdsgcd  16455  absmulgcd  16460  rpmulgcd  16468  rprpwr  16470  sqgcd  16473  dvdssqlem  16477  dvdssq  16478  nn0seqcvgd  16481  algrf  16484  algcvg  16487  lcmcllem  16507  lcmabs  16516  lcmgcd  16518  lcmdvds  16519  lcmgcdnn  16522  lcmf  16544  coprmgcdb  16560  coprmdvds  16564  coprmdvds2  16565  qredeq  16568  isprm3  16594  nprm  16599  oddprmgt2  16610  isprm5  16618  isprm7  16619  divgcdodd  16621  prmdvdsexp  16626  zgcdsq  16664  hashdvds  16686  phiprmpw  16687  crth  16689  phimullem  16690  modprm0  16717  coprimeprodsq  16720  coprimeprodsq2  16721  pythagtriplem2  16729  pythagtriplem19  16745  iserodd  16747  pcpremul  16755  pcmul  16763  pcexp  16771  pcdvdsb  16781  pcneg  16786  pc2dvds  16791  pc11  16792  pcmpt  16804  fldivp1  16809  pcfac  16811  infpnlem1  16822  prmunb  16826  prmreclem1  16828  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  1arithlem4  16838  1arith  16839  gzaddcl  16849  gzmulcl  16850  gzreim  16851  gzsubcl  16852  4sqlem1  16860  4sqlem4a  16863  4sqlem4  16864  4sqlem12  16868  ramlb  16931  prmgaplem4  16966  prmgaplem5  16967  prmgaplem6  16968  prmgaplem7  16969  prmgaplem8  16970  prmgapprmolem  16973  cshwshashlem2  17008  setsvalg  17077  ressval  17144  ressval3d  17157  restval  17330  pwsval  17390  xpsval  17474  ssclem  17726  rescval  17734  funcestrcsetclem9  18054  embedsetcestrclem  18063  lubel  18420  ipodrsima  18447  tsrss  18495  chnrdss  18523  resmgmhm  18619  resmgmhm2  18620  mgmhmco  18622  submnd0  18671  mndinvmod  18672  xpsmnd0  18686  resmhm  18728  resmhm2  18729  mhmco  18731  frmdplusg  18762  frmdmnd  18767  efmndcl  18790  smndex1id  18819  mgm2nsgrplem1  18826  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2nmndlem1  18831  sgrp2rid2  18834  dfgrp3  18952  mhmmnd  18977  mulgnngsum  18992  mulgnnsubcl  18999  mulgnn0z  19014  mulgnndir  19016  mulgmodid  19026  eqgfval  19088  cycsubgcl  19118  cycsubg2  19122  0ghm  19142  resghm  19144  resghm2  19145  ghmco  19148  ghmeql  19151  isgim  19174  gicsubgen  19191  cntzmhm  19253  symgcl  19297  symgextf1  19333  gsmsymgrfixlem1  19339  symgfixf1  19349  symgtrinv  19384  pmtrdifellem3  19390  mndodcongi  19455  odmod  19458  odf1  19474  odf1o1  19484  gexdvds  19496  sylow1lem1  19510  pgpssslw  19526  lsmub1  19569  lsmub2  19570  cntzrecd  19590  pj1ghm  19615  lsmhash  19617  efgred  19660  frgpup1  19687  ablsubadd23  19725  ablsubsub23  19736  mulgnn0di  19737  torsubg  19766  zaddablx  19784  gsumzaddlem  19833  gsumzadd  19834  gsumconst  19846  gsumzmhm  19849  telgsumfzslem  19900  dprdfadd  19934  dprd2dlem1  19955  ablsimpgfindlem1  20021  srgbinomlem3  20146  srgbinomlem4  20147  srgbinomlem  20148  gsummgp0  20236  gsumdixp  20237  xpsring1d  20251  unitnegcl  20315  isrnghm  20359  rnghmco  20375  dfrhm2  20392  rhmco  20416  c0rhm  20449  c0rnghm  20450  rhmimasubrng  20481  cntzsubrng  20482  issubrg3  20515  resrhm  20516  rhmeql  20518  rhmima  20519  isdomn4  20631  imadrhmcl  20712  fldsdrgfld  20713  abvres  20746  suborng  20791  lmodfopne  20833  lspf  20907  lspcl  20909  0lmhm  20974  lmhmco  20977  lmhmeql  20989  islmim  20996  rngqiprngghm  21236  rngqiprnglin  21239  xrsdsreval  21348  xrsdsreclb  21350  xrs1cmn  21379  xrge0omnd  21382  znfld  21497  znchr  21499  znunithash  21501  znrrg  21502  freshmansdream  21511  cnmsgnsubg  21514  zrhpsgnmhm  21521  evpmodpmf1o  21533  psgndiflemB  21537  psgndif  21539  phlssphl  21596  frlmval  21685  uvcfval  21721  frlmsslsp  21733  frlmup2  21736  lindfmm  21764  lmimlbs  21773  islindf4  21775  issubassa3  21803  psrbaglesupp  21859  psrcom  21905  resspsrmul  21913  mplsubrglem  21941  mplcoe3  21973  ltbval  21978  ltbwe  21979  evlslem4  22011  evlslem3  22015  psdmvr  22084  psropprmul  22150  coe1tmmul  22191  cply1mul  22211  gsummoncoe1  22223  lply1binomsc  22226  pf1ind  22270  mamufacex  22311  grpvlinv  22313  grpvrinv  22314  eqmat  22339  mat1dimcrng  22392  dmatcrng  22417  scmatf1  22446  m1detdiag  22512  mdetdiaglem  22513  mdet1  22516  mdetunilem9  22535  madulid  22560  gsummatr01lem4  22573  gsummatr01  22574  mat2pmatlin  22650  m2pmfzgsumcl  22663  monmatcollpw  22694  pmatcollpw3lem  22698  mp2pm2mplem4  22724  chpscmatgsummon  22760  chfacfscmulfsupp  22774  chfacfpmmulfsupp  22778  cayhamlem1  22781  cpmadugsumlemF  22791  clsval2  22965  innei  23040  ordtrest  23117  ordtrestixx  23137  isnrm2  23273  lpcls  23279  tgcmp  23316  cmpcld  23317  uncmp  23318  hauscmplem  23321  hauscmp  23322  1stcfb  23360  1stcrest  23368  kgencmp2  23461  1stckgenlem  23468  kgen2ss  23470  kgencn  23471  kgencn3  23473  txval  23479  txuni2  23480  txbasex  23481  txbas  23482  txtop  23484  ptbasin  23492  txtopon  23506  txcld  23518  txss12  23520  txbasval  23521  xkoccn  23534  txcnp  23535  ptcnplem  23536  upxp  23538  txcnmpt  23539  uptx  23540  txrest  23546  txdis  23547  txindislem  23548  txlly  23551  txnlly  23552  txcmp  23558  hausdiag  23560  txhaus  23562  tx1stc  23565  tx2ndc  23566  txkgen  23567  xkoptsub  23569  cnmpt21  23586  txconn  23604  qtopval  23610  hmeoco  23687  txhmeo  23718  xpstopnlem1  23724  fbun  23755  filss  23768  infil  23778  fbunfip  23784  filuni  23800  fmfnfmlem4  23872  ufldom  23877  flffval  23904  flfval  23905  txflf  23921  fcfval  23948  alexsubALTlem3  23964  tgpmulg  24008  subgtgp  24020  qustgplem  24036  tsmsfbas  24043  tsmsres  24059  tsmsmhm  24061  tsmsadd  24062  isxmet2d  24242  blin2  24344  comet  24428  met2ndci  24437  metcn  24458  txmetcn  24463  dscopn  24488  nrmmetd  24489  isngp3  24513  tngval  24554  nm1  24582  subrgnrg  24588  nrginvrcn  24607  rlmnvc  24618  nmo0  24650  nmoco  24652  nghmco  24653  nmotri  24654  0nghm  24656  isnmhm2  24667  0nmhm  24670  nmhmco  24671  nmhmplusg  24672  qtopbaslem  24673  remetdval  24704  bl2ioo  24707  reperflem  24734  iccntr  24737  icccmplem2  24739  icccmp  24741  reconnlem2  24743  xrge0gsumle  24749  xrge0tsms  24750  divcnOLD  24784  divcn  24786  cncfmet  24829  iccpnfcnv  24869  bndth  24884  copco  24945  pcopt  24949  pcopt2  24950  nmhmcn  25047  cmodscexp  25048  cphassr  25139  lmmbrf  25189  lmnn  25190  iscauf  25207  caucfil  25210  iscmet3lem1  25218  iscmet3lem2  25219  iscmet3  25220  cfilres  25223  caussi  25224  caubl  25235  caublcls  25236  bcthlem2  25252  bcthlem5  25255  cmsss  25278  lssbn  25279  ovolfioo  25395  ovollb2lem  25416  ovolunlem1a  25424  ovoliunlem1  25430  ovoliunlem2  25431  ovoliunlem3  25432  ovoliun2  25434  ovolscalem1  25441  ovolicc2lem1  25445  ovolicc2lem4  25448  ovolicc2lem5  25449  inmbl  25470  voliunlem1  25478  volsup  25484  ioombl1lem4  25489  iccvolcl  25495  ioovolcl  25498  uniioovol  25507  uniioombllem3a  25512  uniioombllem3  25513  uniioombllem4  25514  uniioombllem5  25515  uniioombllem6  25516  dyadf  25519  dyadovol  25521  dyadss  25522  dyadmbl  25528  opnmbllem  25529  volsup2  25533  volcn  25534  ismbf  25556  mbfima  25558  ismbf3d  25582  mbfadd  25589  mbfsub  25590  mbflimsup  25594  itg1mulc  25632  itg1sub  25637  itg1climres  25642  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfmul  25654  itg2const2  25669  itg2seq  25670  itg2uba  25671  itg2lea  25672  itg2eqa  25673  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2i1fseqle  25682  itg2i1fseq  25683  itg2i1fseq2  25684  itg2addlem  25686  itg2cnlem1  25689  bddmulibl  25767  ellimc3  25807  dvaddbr  25867  dvcobr  25876  dvcobrOLD  25877  dvcjbr  25880  dvcnvlem  25907  c1lip1  25929  lhop  25948  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumrlimf  25958  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsum2  25968  tdeglem4  25992  deg1ge  26030  coe1mul3  26031  fta1g  26102  plyco0  26124  plyf  26130  ply1termlem  26135  plyeq0lem  26142  plypf1  26144  plymullem1  26146  plyaddlem  26147  plymullem  26148  coeeulem  26156  coeidlem  26169  plyco  26173  dgreq  26176  coefv0  26180  coeaddlem  26181  coemullem  26182  coemulhi  26186  coemulc  26187  plycn  26193  plycnOLD  26194  dgrlt  26199  dgrsub  26205  plycjlem  26209  plycj  26210  plycjOLD  26212  plyrecj  26214  plymul0or  26215  plyreres  26217  dvply1  26218  vieta1lem2  26246  plyexmo  26248  elqaalem2  26255  elqaalem3  26256  aareccl  26261  aalioulem1  26267  aalioulem3  26269  aaliou  26273  geolim3  26274  ulmcaulem  26330  ulmcau  26331  mtest  26340  dvradcnv  26357  psercn2  26359  psercn2OLD  26360  pserdvlem2  26365  pserdv2  26367  abelthlem6  26373  abelthlem8  26376  abelthlem9  26377  reeff1o  26384  reefgim  26387  sinperlem  26416  sincosq2sgn  26435  sincosq3sgn  26436  sinq12ge0  26444  sincos6thpi  26452  sineq0  26460  cosord  26467  cos11  26469  sinord  26470  tanord1  26473  eff1olem  26484  logrnaddcl  26510  relogeftb  26520  relogoprlem  26527  logleb  26539  advlogexp  26591  logtayllem  26595  logtayl  26596  logtaylsum  26597  logtayl2  26598  recxpcl  26611  rpcxpcl  26612  cxple3  26637  cxpcom  26675  cxpcn3  26685  cxpeq  26694  relogbmul  26714  relogbcxp  26722  relogbf  26728  atanord  26864  atantayl  26874  birthdaylem2  26889  birthdaylem3  26890  cxp2limlem  26913  fsumharmonic  26949  zetacvg  26952  ftalem1  27010  ftalem4  27013  ftalem5  27014  basellem2  27019  basellem3  27020  basellem4  27021  vmappw  27053  sqf11  27076  mumul  27118  fsumdvdscom  27122  dvdsppwf1o  27123  dvdsflf1o  27124  musum  27128  muinv  27130  fsumdvdsmul  27132  1sgmprm  27137  vmalelog  27143  chtublem  27149  fsumvma  27151  vmasum  27154  logfac2  27155  chpval2  27156  logfaclbnd  27160  logexprlim  27163  mersenne  27165  dchrmulcl  27187  dchrinvcl  27191  dchrfi  27193  dchrghm  27194  dchrptlem1  27202  dchrsum2  27206  dchrsum  27207  pcbcctr  27214  bcmono  27215  bposlem1  27222  bposlem2  27223  bposlem3  27224  bposlem5  27226  bposlem6  27227  bposlem7  27228  lgslem3  27237  lgscllem  27242  lgsval4a  27257  lgsneg  27259  lgsdir2  27268  lgsdir  27270  lgsdilem2  27271  lgsdi  27272  lgsne0  27273  gausslemma2dlem1a  27303  gausslemma2dlem3  27306  gausslemma2dlem6  27310  lgseisenlem3  27315  lgseisenlem4  27316  lgsquadlem1  27318  lgsquadlem2  27319  lgsquad2  27324  lgsquad3  27325  2lgslem1a1  27327  2lgslem1a  27329  2lgslem1c  27331  2sqlem2  27356  mul2sq  27357  2sqlem7  27362  2sqreultlem  27385  2sqreunnltlem  27388  2sqreunnltblem  27389  chebbnd1lem1  27407  vmadivsum  27420  rplogsumlem2  27423  dchrisum0lem1a  27424  rpvmasumlem  27425  dchrisumlem1  27427  dchrisumlem2  27428  dchrisumlem3  27429  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrvmasum2if  27435  dchrvmasumlem2  27436  dchrvmasumlem3  27437  dchrvmasumiflem1  27439  dchrvmasumiflem2  27440  dchrisum0ff  27445  dchrisum0flblem1  27446  dchrisum0fno1  27449  rpvmasum2  27450  dchrisum0re  27451  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrisum0lem3  27457  mudivsum  27468  mulogsum  27470  mulog2sumlem1  27472  mulog2sumlem2  27473  mulog2sumlem3  27474  selberglem2  27484  selberg2  27489  chpdifbndlem1  27491  selberg3lem1  27495  pntrsumbnd2  27505  selbergr  27506  pntpbnd1  27524  pntpbnd2  27525  pntlemh  27537  pntlemj  27541  pntlemi  27542  pntlemf  27543  pntlemp  27548  ostth2lem1  27556  ostth1  27571  ostth2lem3  27573  ostth3  27576  noreson  27599  nosepon  27604  noextendseq  27606  nosupbnd1lem5  27651  noetasuplem4  27675  addscom  27909  negsdi  27992  om2noseqlt  28229  om2noseqf1o  28231  n0s0suc  28270  nnsge1  28271  n0sbday  28280  n0sfincut  28282  n0sltp1le  28291  bdayn0sf1o  28295  zaddscl  28318  elzn0s  28322  zsoring  28332  zseo  28345  zs12subscl  28389  remulscllem2  28403  istrkg2ld  28438  isismt  28512  eedimeq  28876  eqeefv  28881  brbtwn2  28883  colinearalglem1  28884  colinearalglem2  28885  colinearalg  28888  eleesub  28889  eleesubd  28890  axcgrrflx  28892  axcgrid  28894  axsegconlem2  28896  axsegconlem7  28901  axsegconlem9  28903  axsegconlem10  28904  axlowdimlem14  28933  axlowdimlem16  28935  axlowdimlem17  28936  axcontlem2  28943  axcontlem4  28945  axcontlem8  28949  axcontlem10  28951  structiedg0val  29000  upgr1eop  29093  numedglnl  29122  usgredg2v  29205  ushgredgedg  29207  ushgredgedgloop  29209  uspgr1eop  29225  usgr1eop  29228  uhgrissubgr  29253  umgrres1lem  29288  upgrres1  29291  nbuhgr  29321  edgnbusgreu  29345  nb3gr2nb  29362  uvtxnm1nbgr  29382  cusgrexilem2  29420  finsumvtxdg2ssteplem4  29527  vtxdgoddnumeven  29532  wlkeq  29612  uspgr2wlkeq  29624  wlksoneq1eq2  29641  upgrwlkdvdelem  29714  usgr2wlkspthlem1  29735  usgrn2cycl  29787  crctcshwlkn0lem3  29790  crctcshwlkn0lem6  29793  crctcshwlkn0lem7  29794  crctcshwlkn0  29799  wspthneq1eq2  29838  wwlkseq  29869  wwlksnext  29871  rusgrnumwlkg  29958  clwwlkccatlem  29969  clwwlkccat  29970  clwlkclwwlklem2a4  29977  clwlkclwwlklem2  29980  clwlkclwwlkf1lem3  29986  clwwisshclwwslemlem  29993  clwwisshclwws  29995  erclwwlkeqlen  29999  erclwwlkref  30000  clwwnisshclwwsn  30039  clwwlknccat  30043  erclwwlkneqlen  30048  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  clwlksndivn  30066  uhgr3cyclex  30162  eucrctshift  30223  eucrct2eupth  30225  frgreu  30248  frgr3v  30255  3vfriswmgr  30258  frgrncvvdeqlem3  30281  frgrregorufrg  30306  numclwwlk1lem2f1  30337  numclwwlk1lem2fo  30338  numclwlk1lem2  30350  numclwwlk3  30365  numclwwlk6  30370  frgrreg  30374  frgrregord013  30375  nsnlplig  30461  nsnlpligALT  30462  ablodivdiv4  30534  imsdval  30666  nmcvcn  30675  sspval  30703  lnoadd  30738  lnosub  30739  nmooge0  30747  nmoolb  30751  nmoub3i  30753  blocnilem  30784  blocni  30785  cncph  30799  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem11  30820  ipblnfi  30835  phoeqi  30837  ubthlem1  30850  ubthlem3  30852  htthlem  30897  hvsub4  31017  his7  31070  his2sub2  31073  hial2eq2  31087  hhip  31157  hhph  31158  bcs2  31162  hhssabloi  31242  hhssnv  31244  ocorth  31271  shsel  31294  shsel3  31295  shscli  31297  chsupss  31322  shjval  31331  chjval  31332  shjcl  31336  chjcl  31337  shsleji  31350  chslej  31478  chsscon2  31482  chjcom  31486  chub1  31487  chdmj1  31509  spanunsni  31559  spanpr  31560  fh1  31598  fh2  31599  cm2j  31600  spansncvi  31632  5oalem1  31634  5oalem3  31636  5oalem5  31638  3oalem2  31643  pjcompi  31652  pjds3i  31693  hoeq  31740  hoadddi  31783  hoadddir  31784  hosubdi  31788  hosub4  31793  hoeq1  31810  hoeq2  31811  adjval2  31871  counop  31901  adjeq  31915  brafnmul  31931  lnopsubi  31954  hmops  32000  hmopm  32001  hmopd  32002  hmopco  32003  nmcopexi  32007  lnconi  32013  lnfnsubi  32026  nmcfnexi  32031  imaelshi  32038  nlelshi  32040  riesz3i  32042  riesz1  32045  cnlnadjlem2  32048  cnlnadjlem6  32052  adjbdln  32063  adjlnop  32066  adjmul  32072  adjadd  32073  nmopcoi  32075  rnbra  32087  cnvbramul  32095  kbass2  32097  kbass4  32099  kbass5  32100  kbass6  32101  leopadd  32112  leopmul2i  32115  leoptri  32116  dmdmd  32280  mddmd  32281  cvdmd  32317  superpos  32334  chrelati  32344  atcv0eq  32359  atomli  32362  atcvatlem  32365  atcvati  32366  atcvat2i  32367  chirredlem4  32373  atcvat3i  32376  atcvat4i  32377  mdsymlem2  32384  mdsymlem3  32385  mdsymlem5  32387  mdsymlem8  32390  dmdsym  32393  cdjreui  32412  cdj1i  32413  cdj3lem2b  32417  cdj3lem3  32418  cdj3lem3b  32420  cdj3i  32421  brabgaf  32589  prct  32696  fcobijfs  32704  fzsplit3  32776  bcm1n  32777  dpfrac1  32872  wrdres  32916  xrge0mulgnn0  32996  xrge0tsmsd  33042  cycpmco2  33102  isarchiofld  33168  resvval  33294  nsgqusf1olem2  33379  lbslsat  33629  ply1degltdimlem  33635  ply1degltdim  33636  ordtrestNEW  33934  mhmhmeotmd  33940  xrge0iifcnv  33946  xrge0iifiso  33948  xrge0pluscn  33953  hasheuni  34098  sxval  34203  measvuni  34227  ddemeas  34249  br2base  34282  dya2iocucvr  34297  sxbrsigalem2  34299  sxbrsiga  34303  omssubadd  34313  eulerpartlemgc  34375  ballotlemfc0  34506  ballotlemfcc  34507  signstfvc  34587  signstres  34588  signsvfn  34595  bnj563  34755  bnj554  34911  bnj557  34913  bnj570  34917  bnj594  34924  bnj849  34937  bnj970  34959  bnj1118  34996  bnj1145  35005  bnj1190  35020  bnj1398  35046  bnj1417  35053  r1omfi  35116  zltp1ne  35154  nnltp1ne  35155  nn0ltp1ne  35156  0nn0m1nnn0  35157  cusgr3cyclex  35180  derangsn  35214  derangen  35216  subfacp1lem5  35228  erdsze2lem1  35247  txpconn  35276  txsconn  35285  cvmliftphtlem  35361  satfdm  35413  satfun  35455  ex-sategoelel  35465  mrsubff1  35558  msubff  35574  msubff1  35600  msubvrs  35604  inffz  35774  bcprod  35782  bccolsum  35783  faclim  35790  dfon2lem4  35828  colineardim1  36105  btwnconn1lem4  36134  btwnconn1lem5  36135  btwnconn1lem6  36136  btwnconn1lem8  36138  btwnconn1lem9  36139  btwnconn1lem12  36142  btwnconn1lem13  36143  btwnconn1lem14  36144  outsideofeu  36175  funray  36184  lineintmo  36201  fwddifnp1  36209  hfun  36222  nn0prpw  36367  opnregcld  36374  cldregopn  36375  ivthALT  36379  onsucconni  36481  bj-nnfim1  36788  bj-nnfim2  36789  bj-2uplex  37066  bj-unexg  37082  bj-prexg  37083  bj-idres  37204  isbasisrelowllem1  37399  isbasisrelowllem2  37400  icoreclin  37401  relowlssretop  37407  exrecfnlem  37423  pibt2  37461  unccur  37642  phpreu  37643  finixpnum  37644  ltflcei  37647  cos2h  37650  lindsadd  37652  lindsdom  37653  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem13  37672  poimirlem14  37673  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem24  37683  poimirlem26  37685  poimirlem27  37686  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  heicant  37694  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  ovoliunnfl  37701  mbfresfi  37705  itg2addnclem  37710  itg2addnc  37713  itg2gt0cn  37714  ftc1cnnc  37731  ftc1anclem3  37734  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  ftc2nc  37741  indexa  37772  incsequz  37787  incsequz2  37788  geomcau  37798  sstotbnd2  37813  prdsbnd  37832  prdstotbnd  37833  prdsbnd2  37834  cntotbnd  37835  ismtyhmeolem  37843  ismtybndlem  37845  heibor1lem  37848  heiborlem3  37852  heiborlem6  37855  heibor  37860  bfplem1  37861  bfplem2  37862  elghomlem1OLD  37924  rngogrphom  38010  prnc  38106  ispridlc  38109  pridlc3  38112  mpobi123f  38201  mptbi12f  38205  antisymressn  38545  eqvreltr  38702  ax12indalem  39043  lsateln0  39093  atlatmstc  39417  hlatjidm  39467  llnneat  39612  lplnneat  39643  lplnnelln  39644  lvolneatN  39686  lvolnelln  39687  lvolnelpln  39688  dalem23  39794  snatpsubN  39848  linepsubN  39850  pmapsub  39866  pmapglbx  39867  paddasslem14  39931  polsubN  40005  pol1N  40008  2polvalN  40012  2polssN  40013  3polN  40014  2pmaplubN  40024  polatN  40029  2polatN  40030  pnonsingN  40031  polsubclN  40050  lautco  40195  cdlemefrs29cpre1  40496  dian0  41137  dia0eldmN  41138  dia1eldmN  41139  dia0  41150  dia1N  41151  dvhopaddN  41212  dib0  41262  dih0  41378  dih1  41384  dihglblem5apreN  41389  dihatexv2  41437  dochfN  41454  lcmineqlem1  42121  lcmineqlem17  42137  xppss12  42321  sumcubes  42405  dvdsexpnn  42425  remul01  42499  resubeqsub  42522  ricdrng1  42620  prjspeclsp  42704  ismrcd2  42791  nacsfix  42804  mzpaddmpt  42833  mzpmulmpt  42834  eq0rabdioph  42868  lerabdioph  42897  ltrabdioph  42900  nerabdioph  42901  dvdsrabdioph  42902  fiphp3d  42911  congneg  43061  jm2.22  43087  jm2.23  43088  jm2.15nn0  43095  jm3.1  43112  aomclem8  43153  lsmfgcl  43166  lmhmfgima  43176  lnmepi  43177  dgrsub2  43227  mpaaeu  43242  mendring  43280  proot1ex  43288  unielss  43310  onsucwordi  43380  oaabsb  43386  rp-oelim2  43400  nnoeomeqom  43404  cantnfresb  43416  oawordex2  43418  omcl3g  43426  ordsssucb  43427  tfsconcatrev  43440  onsucunipr  43464  onsucunitp  43465  oaun3lem1  43466  naddgeoa  43486  oaltom  43497  minregex2  43627  sssymdifcl  43664  relexp01min  43805  ntrclsiso  44159  ntrclsk3  44162  cvgdvgrat  44405  nznngen  44408  uzmptshftfval  44438  addrval  44557  subrval  44558  mulvval  44559  elpwgded  44656  eel2131  44805  eel3132  44806  el12  44817  sspwimp  45009  sspwimpcf  45011  suctrALTcf  45013  suctrALT3  45015  relpfrlem  45045  cnfex  45124  disjinfi  45288  infxrbnd2  45466  supminfxr  45561  climinf  45705  lptre2pt  45737  limcresiooub  45739  limcresioolb  45740  addlimc  45745  limclner  45748  limsuppnflem  45807  limsupmnfuzlem  45823  limsupvaluz2  45835  limsupresxr  45863  liminfresxr  45864  cnrefiisplem  45926  cncfdmsn  45987  iblspltprt  46070  itgspltprt  46076  dirkertrigeqlem3  46197  fourierdlem62  46265  fourierdlem80  46283  fourierdlem102  46305  fourierdlem103  46306  fourierdlem104  46307  fourierdlem114  46317  sge0f1o  46479  hoidmvlelem2  46693  pimdecfgtioo  46814  smfliminflem  46927  fnresfnco  47140  fcores  47166  dfatcolem  47354  nn0resubcl  47407  zgeltp1eq  47408  eluzge0nn0  47411  fz0addcom  47416  elfzlble  47419  fzopredsuc  47422  subsubelfzo0  47425  ceilbi  47432  minusmod5ne  47448  submodlt  47449  mod0mul  47455  m1modmmod  47457  uniimafveqt  47480  fundcmpsurinjimaid  47510  icceuelpartlem  47534  iccpartnel  47537  elsprel  47574  fmtnodvds  47643  goldbachth  47646  fmtnoprmfac2  47666  prmdvdsfmtnof1  47686  2pwp1prm  47688  flsqrt  47692  lighneallem4  47709  dfodd6  47736  divgcdoddALTV  47781  opoeALTV  47782  opeoALTV  47783  omoeALTV  47784  omeoALTV  47785  epoo  47802  emoo  47803  epee  47804  emee  47805  evensumeven  47806  even3prm2  47818  mogoldbblem  47819  fpprmod  47826  dfwppr  47837  fpprwppr  47838  fpprwpprb  47839  gbepos  47857  gbegt5  47860  gbowgt5  47861  gboge9  47863  sbgoldbst  47877  nnsum3primesgbe  47891  bgoldbtbndlem1  47904  bgoldbtbndlem2  47905  bgoldbtbndlem3  47906  grimco  47988  isuspgrim0  47993  isuspgrimlem  47994  uhgrimisgrgriclem  48029  uhgrimisgrgric  48030  clnbgrgrim  48033  grimedg  48034  isgrtri  48042  cycl3grtri  48046  isubgr3stgrlem6  48070  isubgr3stgrlem7  48071  isubgr3stgrlem8  48072  uspgrlimlem2  48088  uspgrlimlem3  48089  uspgrlimlem4  48090  grlictr  48114  gpgusgralem  48155  gpgedg2ov  48165  gpgnbgrvtx0  48173  gpgnbgrvtx1  48174  gpg5nbgrvtx03star  48179  gpg5nbgr3star  48180  gpg5grlic  48193  2zrngmmgm  48351  2zrngnmrid  48355  2zrngnmlid2  48356  altgsumbc  48451  altgsumbcALT  48452  zlmodzxzadd  48457  zlmodzxzsub  48459  invginvrid  48466  ply1mulgsumlem2  48487  ply1mulgsum  48490  lincvalpr  48518  lindslinindimp2lem1  48558  ldepsprlem  48572  ldepspr  48573  lincresunit3lem3  48574  lincresunitlem1  48575  lincresunit3lem1  48579  lincresunit3  48581  elfzolborelfzop1  48619  zgtp1leeq  48621  flsubz  48622  nneom  48627  nn0ofldiv2  48632  rege1logbrege0  48658  nnpw2pb  48687  dignn0fr  48701  dignn0ldlem  48702  dignnld  48703  dignn0flhalflem1  48715  nn0sumshdiglemB  48720  nn0mulfsum  48724  rrx2plordisom  48823  ehl2eudis0lt  48826  itsclinecirc0in  48875  2itscp  48881  inlinecirc02plem  48886  mof0ALT  48939  i0oii  49019  resccat  49174