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  2377  nfeqf  2383  eqeqan12dALT  2752  sylan9eq  2788  sylan9ss  3945  ssconb  4093  ineqan12d  4173  ifpr  4647  disjtp2  4670  dfopg  4824  disjxiun  5092  breqan12d  5111  eusv1  5333  opelvvg  5662  opthprc  5685  relop  5797  dmpropg  6170  unixp  6237  tz7.7  6340  ordin  6344  onin  6345  ontri1  6348  onfr  6353  onelpss  6354  onsseleq  6355  oneltri  6357  ontr2  6362  onunel  6421  onun2  6424  funssres  6533  funtpg  6544  funtp  6546  resasplit  6701  fodmrnu  6751  f1un  6791  dffv2  6926  fvreseq0  6980  fvcofneq  7035  funopdmsn  7092  fprg  7097  fprb  7137  fconst2g  7146  isofrlem  7283  oveqan12d  7374  ov3  7518  ovg  7520  ovima0  7534  f1opw2  7610  off  7637  unexgOLD  7691  pwuncl  7712  epweon  7717  epweonALT  7718  sucexeloni  7751  ordunpr  7765  omun  7827  peano4  7831  fabexg  7877  f1oabexg  7881  fiun  7884  offres  7924  el2mpocsbcl  8024  curry1  8043  curry1val  8044  curry2  8046  curry2val  8048  soxp  8068  wexp  8069  xpord2pred  8084  poxp3  8089  poseq  8097  soseq  8098  suppfnss  8128  frrlem4  8228  frrlem11  8235  frrlem12  8236  fprlem1  8239  iunon  8268  onfununi  8270  tfrlem11  8316  tz7.48lem  8369  seqomeq12  8382  oacan  8472  oawordri  8474  oaass  8485  omord2  8491  omcan  8493  oen0  8510  oeordi  8511  oeord  8512  oecan  8513  oeworde  8517  oeordsuc  8518  oelimcl  8524  nnawordi  8545  nnaword  8551  nnmord  8556  oaabslem  8571  omabslem  8574  omsmo  8582  eldifsucnn  8588  naddcllem  8600  naddov2  8603  ertr  8646  erex  8655  brecop  8743  ecopovtrn  8753  ecovdi  8758  mapvalg  8769  pmvalg  8770  pmss12g  8802  elmapresaun  8813  boxcutc  8874  undom  8988  sbthlem7  9016  sbth  9020  sdomnsym  9025  sdomdomtr  9033  xpf1o  9062  xpen  9063  limenpsi  9075  pssnn  9088  pwssfi  9096  sbthfi  9118  php2  9127  php3  9128  phpeqd  9131  nndomog  9132  onomeneq  9133  isinf  9159  fineqvlem  9160  f1finf1o  9167  dif1ennnALT  9171  findcard3  9177  unblem2  9187  isfinite2  9192  unfilem1  9199  unfi2  9204  fodomfir  9222  unifi2  9239  f1opwfi  9250  fsuppxpfi  9279  fsuppunbi  9283  fsuppco2  9297  fsuppcor  9298  fival  9306  fiin  9316  ordiso  9412  ordtypelem10  9423  hartogslem1  9438  wofib  9441  brwdom3  9478  unwdomg  9480  xpwdomg  9481  sucprcreg  9500  preleqALT  9517  inf3lem6  9533  oemapval  9583  cantnf  9593  wemapwe  9597  cnfcom  9600  ttrcltr  9616  dfttrcl2  9624  frmin  9652  r111  9678  r1ord3g  9682  prwf  9714  r1pw  9748  rankprb  9754  rankxplim  9782  tcrank  9787  updjud  9837  finnum  9851  xpnum  9854  carduni  9884  nnsdomel  9893  fidomtri  9896  infxpenlem  9914  fseqdom  9927  onssnum  9941  acndom2  9955  alephinit  9996  dfac5lem4  10027  dfac5lem4OLD  10029  kmlem6  10057  undjudom  10069  endjudisj  10070  djuen  10071  djucomen  10079  pwdjuen  10083  djudom1  10084  djuxpdom  10087  djufi  10088  cardadju  10096  nnadju  10099  nnadjuALT  10100  ficardadju  10101  ficardun  10102  ficardun2  10103  pwsdompw  10104  unctb  10105  ackbij2lem1  10119  ackbij1lem6  10125  ackbij1lem16  10135  ackbij1b  10139  ackbij2  10143  coflim  10162  cflim2  10164  cofsmo  10170  coftr  10174  sornom  10178  infpssrlem5  10208  fin4en1  10210  fin23lem23  10227  fin23lem28  10241  isf32lem2  10255  isf32lem4  10257  isf32lem7  10260  isf34lem7  10280  isf34lem6  10281  fin67  10296  isfin7-2  10297  fin1a2lem9  10309  domtriomlem  10343  axdc3lem2  10352  axdc3lem4  10354  axdc4lem  10356  zorn2lem6  10402  ttukeylem3  10412  brdom6disj  10433  carddom  10455  cardsdom  10456  domtri  10457  konigthlem  10469  iunctb  10475  alephadd  10478  alephmul  10479  pwcfsdom  10484  cfpwsdom  10485  fpwwe2lem12  10543  canthp1lem2  10554  pwfseqlem3  10561  pwfseqlem4a  10562  inar1  10676  tskcard  10682  tskuni  10684  grur1  10721  mulclpi  10794  addcompi  10795  mulcompi  10797  distrpi  10799  ltexpi  10803  ltapi  10804  ltmpi  10805  enqbreq2  10821  nqereu  10830  addpipq  10838  addpqnq  10839  mulpipq  10841  mulpqnq  10842  addpqf  10845  addclnq  10846  mulpqf  10847  mulclnq  10848  adderpq  10857  mulerpq  10858  ltsonq  10870  lterpq  10871  ltbtwnnq  10879  ltrnq  10880  genpv  10900  genpdm  10903  genpnnp  10906  mulclprlem  10920  distrlem1pr  10926  distrlem4pr  10927  prlem934  10934  addcanpr  10947  suplem1pr  10953  mulcmpblnr  10972  mulclsr  10985  mulasssr  10991  distrsr  10992  ltsosr  10995  1idsr  10999  00sr  11000  recexsrlem  11004  mulgt0sr  11006  addcnsr  11036  axmulf  11047  axmulass  11058  axdistr  11059  axcnre  11065  mulrid  11120  axltadd  11196  lenlt  11201  dedekind  11286  dedekindle  11287  resubcl  11435  subeqrev  11549  muladd  11559  mulsub  11570  mulsub2  11571  ltaddsub2  11602  leaddsub2  11604  leltadd  11611  ltaddpos2  11618  posdif  11620  addge02  11638  mullt0  11646  ltord1  11653  leord1  11654  eqord1  11655  recextlem1  11757  recex  11759  divmuldiv  11831  conjmul  11848  div2sub  11956  prodgt02  11979  lemul2  11984  lemul2a  11986  ltmulgt12  11992  lemulge12  11995  mulge0b  12002  mulle0b  12003  ltmuldiv2  12006  ltdivmul2  12009  lt2mul2div  12010  ledivmul2  12011  lemuldiv2  12013  ledivdiv  12021  lediv2  12022  ltdiv23  12023  lediv23  12024  supmul  12104  riotaneg  12111  negiso  12112  cju  12131  nnaddcl  12158  nnmulcl  12159  nnmtmip  12161  nnsub  12179  addltmul  12367  avgle1  12371  avgle2  12372  avgle  12373  nnrecl  12389  nn0nnaddcl  12422  nn0sub  12441  elz2  12496  zaddcl  12522  zsubcl  12524  znnsub  12528  znn0sub  12529  nzadd  12530  zmulcl  12531  zltp1le  12532  zleltp1  12533  nnleltp1  12538  nnltp1le  12539  nnaddm1cl  12540  nn0ltp1le  12541  nn0leltp1  12542  nn0ltlem1  12543  nn0lem1lt  12548  nnlem1lt  12549  nnltlem1  12550  zdiv  12553  zextle  12556  zextlt  12557  btwnnz  12559  prime  12564  nneo  12567  peano2uz2  12571  uzind  12575  fzind  12581  zriotaneg  12596  uzneg  12762  uztric  12766  uz11  12767  eluzp1m1  12768  eluzp1p1  12770  uzin  12782  uzwo  12819  indstr  12824  uz2mulcl  12834  supminf  12843  uzsupss  12848  zmax  12853  rebtwnz  12855  qre  12861  qaddcl  12873  qsubcl  12876  irradd  12881  elpqb  12884  rpnnen1lem5  12889  cnref1o  12893  rpaddcl  12924  rpmulcl  12925  rpmtmip  12926  rpdivcl  12927  max1  13094  max2  13096  min1  13098  min2  13099  z2ge  13107  qbtwnxr  13109  xaddf  13133  rexadd  13141  rexsub  13142  xnn0xaddcl  13144  xaddcom  13149  xnn0xadd0  13156  xnegdi  13157  rexmul  13180  supxrbnd2  13231  ixxin  13272  elicc2  13321  difreicc  13394  iccshftr  13396  iccshftl  13398  iccdil  13400  icccntr  13402  fzval2  13420  elfz1eq  13445  peano2fzr  13447  fzn  13450  fzsplit2  13459  fzaddel  13468  fzadd2  13469  fzsubel  13470  fzrev2  13498  fzrev3  13500  uzsplit  13506  fznuz  13519  uznfz  13520  fzrevral  13522  fzrevral3  13524  fzshftral  13525  elfz2nn0  13528  fznn0sub2  13545  fz0fzdiffz0  13547  elfzmlbp  13549  difelfzle  13551  difelfznle  13552  elfzouz2  13584  fzo0n  13591  fzouzsplit  13604  fzoun  13606  elfzo0le  13613  fzonmapblen  13618  fzofzim  13619  fzoaddel2  13630  eluzgtdifelfzo  13637  elfzodifsumelfzo  13641  ssfzoulel  13670  ubmelm1fzo  13673  fzofzp1b  13675  elfzonelfzo  13679  elfznelfzo  13683  fzostep1  13696  injresinjlem  13700  subfzo0  13702  flflp1  13721  divfl0  13738  flzadd  13740  flmulnn0  13741  fldivnn0le  13746  fldiv  13774  uzsup  13777  mulmod0  13791  modlt  13794  modmulnn  13803  zmodcl  13805  zmodfz  13807  zmodid2  13813  modcyc  13820  muladdmodid  13827  modmuladdnn0  13832  negmod  13833  addmodidr  13837  modadd2mod  13838  modaddmodup  13851  modaddmulmod  13855  modfzo0difsn  13860  modsumfzodifsn  13861  addmodlteq  13863  om2uzlti  13867  om2uzf1oi  13870  fzen2  13886  ssnn0fi  13902  fsuppmapnn0fiublem  13907  fsuppmapnn0fiub0  13910  seqshft2  13945  seqsplit  13952  seqcaopr2  13955  seqf1olem2  13959  expcllem  13989  expcl2lem  13990  1exp  14008  expge1  14016  expadd  14021  expmul  14024  expsub  14027  nn0sq11  14049  lt2sq  14050  le2sq  14051  expmordi  14084  leexp2  14088  leexp1a  14092  sumsqeq0  14096  bernneq  14146  bernneq2  14147  expnbnd  14149  digit2  14153  digit1  14154  facdiv  14204  facwordi  14206  faclbnd  14207  faclbnd3  14209  faclbnd4lem4  14213  faclbnd5  14215  faclbnd6  14216  facavg  14218  bcrpcl  14225  bccmpl  14226  bcval5  14235  hashen  14264  hasheqf1oi  14268  hashgadd  14294  hashdom  14296  hashsdom  14298  hashun  14299  hashunsnggt  14311  hashprg  14312  hashssdif  14329  hashxplem  14350  seqcoll  14381  tpf1o  14418  eqwrd  14474  ccatfval  14490  ccatlen  14492  ccat0  14493  elfzelfzccat  14497  ccatsymb  14500  ccatval21sw  14503  ccatrn  14507  lswccatn0lsw  14509  ccatalpha  14511  ccatrcl1  14512  ccats1alpha  14537  swrdnd  14572  swrdfv2  14579  swrdsbslen  14582  swrdspsleq  14583  swrdccat2  14587  pfxnd0  14606  pfxeq  14613  ccatpfx  14618  pfxccat1  14619  swrdswrdlem  14621  pfxswrd  14623  pfxccatin12lem4  14643  pfxccatin12lem1  14645  pfxccatin12lem2  14648  pfxccatin12lem3  14649  pfxccatin12  14650  pfxccat3  14651  swrdccat  14652  pfxccatpfx2  14654  pfxccat3a  14655  swrdccat3blem  14656  swrdccat3b  14657  revccat  14683  revrev  14684  cshwlen  14716  cshwidxmod  14720  cshwidxmodr  14721  cshweqdif2  14736  cshweqrep  14738  2cshwcshw  14742  s3eq3seq  14856  cotr2g  14893  trclun  14931  shftf  14996  seqshft  15002  crre  15031  crim  15032  readd  15043  resub  15044  remul2  15047  imadd  15051  imsub  15052  immul2  15054  ipcnval  15060  cjsub  15066  cjreim  15077  01sqrexlem6  15164  sqrtle  15177  sqrt11  15179  absreimsq  15209  absreim  15210  absmul  15211  sqabs  15224  absdiflt  15235  absdifle  15236  abssuble0  15246  absmax  15247  abs2difabs  15252  fzomaxdif  15261  rexanuz  15263  rexuz3  15266  rexuzre  15270  caubnd2  15275  limsupgre  15398  limsupbnd2  15400  climconst2  15465  lo1resb  15481  o1resb  15483  2clim  15489  climshftlem  15491  climshft  15493  climshft2  15499  cjcn2  15517  o1of2  15530  o1rlimmul  15536  climaddc1  15552  climmulc2  15554  climsubc1  15555  climsubc2  15556  lo1le  15569  climlec2  15576  isershft  15581  isercolllem1  15582  isercolllem3  15584  isercoll  15585  isercoll2  15586  climsup  15587  caurcvg  15594  caucvg  15596  iseraltlem1  15599  iseraltlem2  15600  iseralt  15602  summolem2a  15632  isumclim3  15676  mptfzshft  15695  fsumrev  15696  fsum0diag2  15700  fsumconst  15707  telfsumo2  15720  fsumparts  15723  o1fsum  15730  cvgcmp  15733  cvgcmpub  15734  cvgcmpce  15735  binomlem  15746  binom1p  15748  binom1dif  15750  bcxmas  15752  incexclem  15753  incexc  15754  incexc2  15755  isumshft  15756  isumsplit  15757  isumsup2  15763  climcndslem1  15766  climcndslem2  15767  climcnds  15768  supcvg  15773  expcnv  15781  geoserg  15783  pwdif  15785  geolim  15787  geoisum1  15796  geoisum1c  15797  cvgrat  15800  mertenslem1  15801  mertenslem2  15802  mertens  15803  ntrivcvgfvn0  15816  ntrivcvgmullem  15818  prodmolem2a  15851  prodmo  15853  fprodf1o  15863  fproddiv  15878  fprodeq0  15892  risefacval2  15927  fallfacval2  15928  fallfacval3  15929  rprisefaccl  15940  risefallfac  15941  fallfacfwd  15953  binomfallfaclem1  15956  binomfallfaclem2  15957  binomrisefac  15959  bpolycl  15969  bpolysum  15970  bpolydiflem  15971  fsumkthpow  15973  efcj  16009  fprodefsum  16012  efexp  16020  eftlub  16028  effsumlt  16030  efle  16037  reef11  16038  efieq  16082  sinsub  16087  cossub  16088  subsin  16090  sinmul  16091  cosmul  16092  addcos  16093  subcos  16094  rpnnen2lem10  16142  rpnnen2lem12  16144  ruclem8  16156  ruclem12  16160  sqrt2irr  16168  dvdssub2  16222  dvdsadd  16223  dvdsaddr  16224  dvdssub  16225  dvdssubr  16226  dvdsle  16231  alzdvds  16241  fzocongeq  16245  odd2np1  16262  opoe  16284  omoe  16285  opeo  16286  omeo  16287  pwp1fsum  16312  divalglem4  16317  divalglem9  16322  divalgb  16325  divalgmod  16327  ndvdsadd  16331  smueqlem  16411  gcdaddm  16446  modgcd  16453  bezoutlem1  16460  dvdsgcd  16465  absmulgcd  16470  rpmulgcd  16478  rprpwr  16480  sqgcd  16483  dvdssqlem  16487  dvdssq  16488  nn0seqcvgd  16491  algrf  16494  algcvg  16497  lcmcllem  16517  lcmabs  16526  lcmgcd  16528  lcmdvds  16529  lcmgcdnn  16532  lcmf  16554  coprmgcdb  16570  coprmdvds  16574  coprmdvds2  16575  qredeq  16578  isprm3  16604  nprm  16609  oddprmgt2  16620  isprm5  16628  isprm7  16629  divgcdodd  16631  prmdvdsexp  16636  zgcdsq  16674  hashdvds  16696  phiprmpw  16697  crth  16699  phimullem  16700  modprm0  16727  coprimeprodsq  16730  coprimeprodsq2  16731  pythagtriplem2  16739  pythagtriplem19  16755  iserodd  16757  pcpremul  16765  pcmul  16773  pcexp  16781  pcdvdsb  16791  pcneg  16796  pc2dvds  16801  pc11  16802  pcmpt  16814  fldivp1  16819  pcfac  16821  infpnlem1  16832  prmunb  16836  prmreclem1  16838  prmreclem3  16840  prmreclem4  16841  prmreclem5  16842  1arithlem4  16848  1arith  16849  gzaddcl  16859  gzmulcl  16860  gzreim  16861  gzsubcl  16862  4sqlem1  16870  4sqlem4a  16873  4sqlem4  16874  4sqlem12  16878  ramlb  16941  prmgaplem4  16976  prmgaplem5  16977  prmgaplem6  16978  prmgaplem7  16979  prmgaplem8  16980  prmgapprmolem  16983  cshwshashlem2  17018  setsvalg  17087  ressval  17154  ressval3d  17167  restval  17340  pwsval  17400  xpsval  17484  ssclem  17736  rescval  17744  funcestrcsetclem9  18064  embedsetcestrclem  18073  lubel  18430  ipodrsima  18457  tsrss  18505  chnrdss  18533  resmgmhm  18629  resmgmhm2  18630  mgmhmco  18632  submnd0  18681  mndinvmod  18682  xpsmnd0  18696  resmhm  18738  resmhm2  18739  mhmco  18741  frmdplusg  18772  frmdmnd  18777  efmndcl  18800  smndex1id  18829  mgm2nsgrplem1  18836  mgm2nsgrplem2  18837  mgm2nsgrplem3  18838  sgrp2nmndlem1  18841  sgrp2rid2  18844  dfgrp3  18962  mhmmnd  18987  mulgnngsum  19002  mulgnnsubcl  19009  mulgnn0z  19024  mulgnndir  19026  mulgmodid  19036  eqgfval  19098  cycsubgcl  19128  cycsubg2  19132  0ghm  19152  resghm  19154  resghm2  19155  ghmco  19158  ghmeql  19161  isgim  19184  gicsubgen  19201  cntzmhm  19263  symgcl  19307  symgextf1  19343  gsmsymgrfixlem1  19349  symgfixf1  19359  symgtrinv  19394  pmtrdifellem3  19400  mndodcongi  19465  odmod  19468  odf1  19484  odf1o1  19494  gexdvds  19506  sylow1lem1  19520  pgpssslw  19536  lsmub1  19579  lsmub2  19580  cntzrecd  19600  pj1ghm  19625  lsmhash  19627  efgred  19670  frgpup1  19697  ablsubadd23  19735  ablsubsub23  19746  mulgnn0di  19747  torsubg  19776  zaddablx  19794  gsumzaddlem  19843  gsumzadd  19844  gsumconst  19856  gsumzmhm  19859  telgsumfzslem  19910  dprdfadd  19944  dprd2dlem1  19965  ablsimpgfindlem1  20031  srgbinomlem3  20156  srgbinomlem4  20157  srgbinomlem  20158  gsummgp0  20246  gsumdixp  20247  xpsring1d  20261  unitnegcl  20325  isrnghm  20369  rnghmco  20385  dfrhm2  20402  rhmco  20426  c0rhm  20459  c0rnghm  20460  rhmimasubrng  20491  cntzsubrng  20492  issubrg3  20525  resrhm  20526  rhmeql  20528  rhmima  20529  isdomn4  20641  imadrhmcl  20722  fldsdrgfld  20723  abvres  20756  suborng  20801  lmodfopne  20843  lspf  20917  lspcl  20919  0lmhm  20984  lmhmco  20987  lmhmeql  20999  islmim  21006  rngqiprngghm  21246  rngqiprnglin  21249  xrsdsreval  21358  xrsdsreclb  21360  xrs1cmn  21389  xrge0omnd  21392  znfld  21507  znchr  21509  znunithash  21511  znrrg  21512  freshmansdream  21521  cnmsgnsubg  21524  zrhpsgnmhm  21531  evpmodpmf1o  21543  psgndiflemB  21547  psgndif  21549  phlssphl  21606  frlmval  21695  uvcfval  21731  frlmsslsp  21743  frlmup2  21746  lindfmm  21774  lmimlbs  21783  islindf4  21785  issubassa3  21813  psrbaglesupp  21869  psrcom  21915  resspsrmul  21923  mplsubrglem  21951  mplcoe3  21983  ltbval  21988  ltbwe  21989  evlslem4  22021  evlslem3  22025  psdmvr  22094  psropprmul  22160  coe1tmmul  22201  cply1mul  22221  gsummoncoe1  22233  lply1binomsc  22236  pf1ind  22280  mamufacex  22321  grpvlinv  22323  grpvrinv  22324  eqmat  22349  mat1dimcrng  22402  dmatcrng  22427  scmatf1  22456  m1detdiag  22522  mdetdiaglem  22523  mdet1  22526  mdetunilem9  22545  madulid  22570  gsummatr01lem4  22583  gsummatr01  22584  mat2pmatlin  22660  m2pmfzgsumcl  22673  monmatcollpw  22704  pmatcollpw3lem  22708  mp2pm2mplem4  22734  chpscmatgsummon  22770  chfacfscmulfsupp  22784  chfacfpmmulfsupp  22788  cayhamlem1  22791  cpmadugsumlemF  22801  clsval2  22975  innei  23050  ordtrest  23127  ordtrestixx  23147  isnrm2  23283  lpcls  23289  tgcmp  23326  cmpcld  23327  uncmp  23328  hauscmplem  23331  hauscmp  23332  1stcfb  23370  1stcrest  23378  kgencmp2  23471  1stckgenlem  23478  kgen2ss  23480  kgencn  23481  kgencn3  23483  txval  23489  txuni2  23490  txbasex  23491  txbas  23492  txtop  23494  ptbasin  23502  txtopon  23516  txcld  23528  txss12  23530  txbasval  23531  xkoccn  23544  txcnp  23545  ptcnplem  23546  upxp  23548  txcnmpt  23549  uptx  23550  txrest  23556  txdis  23557  txindislem  23558  txlly  23561  txnlly  23562  txcmp  23568  hausdiag  23570  txhaus  23572  tx1stc  23575  tx2ndc  23576  txkgen  23577  xkoptsub  23579  cnmpt21  23596  txconn  23614  qtopval  23620  hmeoco  23697  txhmeo  23728  xpstopnlem1  23734  fbun  23765  filss  23778  infil  23788  fbunfip  23794  filuni  23810  fmfnfmlem4  23882  ufldom  23887  flffval  23914  flfval  23915  txflf  23931  fcfval  23958  alexsubALTlem3  23974  tgpmulg  24018  subgtgp  24030  qustgplem  24046  tsmsfbas  24053  tsmsres  24069  tsmsmhm  24071  tsmsadd  24072  isxmet2d  24252  blin2  24354  comet  24438  met2ndci  24447  metcn  24468  txmetcn  24473  dscopn  24498  nrmmetd  24499  isngp3  24523  tngval  24564  nm1  24592  subrgnrg  24598  nrginvrcn  24617  rlmnvc  24628  nmo0  24660  nmoco  24662  nghmco  24663  nmotri  24664  0nghm  24666  isnmhm2  24677  0nmhm  24680  nmhmco  24681  nmhmplusg  24682  qtopbaslem  24683  remetdval  24714  bl2ioo  24717  reperflem  24744  iccntr  24747  icccmplem2  24749  icccmp  24751  reconnlem2  24753  xrge0gsumle  24759  xrge0tsms  24760  divcnOLD  24794  divcn  24796  cncfmet  24839  iccpnfcnv  24879  bndth  24894  copco  24955  pcopt  24959  pcopt2  24960  nmhmcn  25057  cmodscexp  25058  cphassr  25149  lmmbrf  25199  lmnn  25200  iscauf  25217  caucfil  25220  iscmet3lem1  25228  iscmet3lem2  25229  iscmet3  25230  cfilres  25233  caussi  25234  caubl  25245  caublcls  25246  bcthlem2  25262  bcthlem5  25265  cmsss  25288  lssbn  25289  ovolfioo  25405  ovollb2lem  25426  ovolunlem1a  25434  ovoliunlem1  25440  ovoliunlem2  25441  ovoliunlem3  25442  ovoliun2  25444  ovolscalem1  25451  ovolicc2lem1  25455  ovolicc2lem4  25458  ovolicc2lem5  25459  inmbl  25480  voliunlem1  25488  volsup  25494  ioombl1lem4  25499  iccvolcl  25505  ioovolcl  25508  uniioovol  25517  uniioombllem3a  25522  uniioombllem3  25523  uniioombllem4  25524  uniioombllem5  25525  uniioombllem6  25526  dyadf  25529  dyadovol  25531  dyadss  25532  dyadmbl  25538  opnmbllem  25539  volsup2  25543  volcn  25544  ismbf  25566  mbfima  25568  ismbf3d  25592  mbfadd  25599  mbfsub  25600  mbflimsup  25604  itg1mulc  25642  itg1sub  25647  itg1climres  25652  mbfi1fseqlem1  25653  mbfi1fseqlem3  25655  mbfi1fseqlem4  25656  mbfi1fseqlem5  25657  mbfmul  25664  itg2const2  25679  itg2seq  25680  itg2uba  25681  itg2lea  25682  itg2eqa  25683  itg2splitlem  25686  itg2split  25687  itg2monolem1  25688  itg2i1fseqle  25692  itg2i1fseq  25693  itg2i1fseq2  25694  itg2addlem  25696  itg2cnlem1  25699  bddmulibl  25777  ellimc3  25817  dvaddbr  25877  dvcobr  25886  dvcobrOLD  25887  dvcjbr  25890  dvcnvlem  25917  c1lip1  25939  lhop  25958  dvfsumle  25963  dvfsumleOLD  25964  dvfsumabs  25966  dvfsumrlimf  25968  dvfsumlem1  25969  dvfsumlem2  25970  dvfsumlem2OLD  25971  dvfsumlem3  25972  dvfsumlem4  25973  dvfsum2  25978  tdeglem4  26002  deg1ge  26040  coe1mul3  26041  fta1g  26112  plyco0  26134  plyf  26140  ply1termlem  26145  plyeq0lem  26152  plypf1  26154  plymullem1  26156  plyaddlem  26157  plymullem  26158  coeeulem  26166  coeidlem  26179  plyco  26183  dgreq  26186  coefv0  26190  coeaddlem  26191  coemullem  26192  coemulhi  26196  coemulc  26197  plycn  26203  plycnOLD  26204  dgrlt  26209  dgrsub  26215  plycjlem  26219  plycj  26220  plycjOLD  26222  plyrecj  26224  plymul0or  26225  plyreres  26227  dvply1  26228  vieta1lem2  26256  plyexmo  26258  elqaalem2  26265  elqaalem3  26266  aareccl  26271  aalioulem1  26277  aalioulem3  26279  aaliou  26283  geolim3  26284  ulmcaulem  26340  ulmcau  26341  mtest  26350  dvradcnv  26367  psercn2  26369  psercn2OLD  26370  pserdvlem2  26375  pserdv2  26377  abelthlem6  26383  abelthlem8  26386  abelthlem9  26387  reeff1o  26394  reefgim  26397  sinperlem  26426  sincosq2sgn  26445  sincosq3sgn  26446  sinq12ge0  26454  sincos6thpi  26462  sineq0  26470  cosord  26477  cos11  26479  sinord  26480  tanord1  26483  eff1olem  26494  logrnaddcl  26520  relogeftb  26530  relogoprlem  26537  logleb  26549  advlogexp  26601  logtayllem  26605  logtayl  26606  logtaylsum  26607  logtayl2  26608  recxpcl  26621  rpcxpcl  26622  cxple3  26647  cxpcom  26685  cxpcn3  26695  cxpeq  26704  relogbmul  26724  relogbcxp  26732  relogbf  26738  atanord  26874  atantayl  26884  birthdaylem2  26899  birthdaylem3  26900  cxp2limlem  26923  fsumharmonic  26959  zetacvg  26962  ftalem1  27020  ftalem4  27023  ftalem5  27024  basellem2  27029  basellem3  27030  basellem4  27031  vmappw  27063  sqf11  27086  mumul  27128  fsumdvdscom  27132  dvdsppwf1o  27133  dvdsflf1o  27134  musum  27138  muinv  27140  fsumdvdsmul  27142  1sgmprm  27147  vmalelog  27153  chtublem  27159  fsumvma  27161  vmasum  27164  logfac2  27165  chpval2  27166  logfaclbnd  27170  logexprlim  27173  mersenne  27175  dchrmulcl  27197  dchrinvcl  27201  dchrfi  27203  dchrghm  27204  dchrptlem1  27212  dchrsum2  27216  dchrsum  27217  pcbcctr  27224  bcmono  27225  bposlem1  27232  bposlem2  27233  bposlem3  27234  bposlem5  27236  bposlem6  27237  bposlem7  27238  lgslem3  27247  lgscllem  27252  lgsval4a  27267  lgsneg  27269  lgsdir2  27278  lgsdir  27280  lgsdilem2  27281  lgsdi  27282  lgsne0  27283  gausslemma2dlem1a  27313  gausslemma2dlem3  27316  gausslemma2dlem6  27320  lgseisenlem3  27325  lgseisenlem4  27326  lgsquadlem1  27328  lgsquadlem2  27329  lgsquad2  27334  lgsquad3  27335  2lgslem1a1  27337  2lgslem1a  27339  2lgslem1c  27341  2sqlem2  27366  mul2sq  27367  2sqlem7  27372  2sqreultlem  27395  2sqreunnltlem  27398  2sqreunnltblem  27399  chebbnd1lem1  27417  vmadivsum  27430  rplogsumlem2  27433  dchrisum0lem1a  27434  rpvmasumlem  27435  dchrisumlem1  27437  dchrisumlem2  27438  dchrisumlem3  27439  dchrmusumlema  27441  dchrmusum2  27442  dchrvmasumlem1  27443  dchrvmasum2lem  27444  dchrvmasum2if  27445  dchrvmasumlem2  27446  dchrvmasumlem3  27447  dchrvmasumiflem1  27449  dchrvmasumiflem2  27450  dchrisum0ff  27455  dchrisum0flblem1  27456  dchrisum0fno1  27459  rpvmasum2  27460  dchrisum0re  27461  dchrisum0lem1b  27463  dchrisum0lem1  27464  dchrisum0lem2a  27465  dchrisum0lem2  27466  dchrisum0lem3  27467  mudivsum  27478  mulogsum  27480  mulog2sumlem1  27482  mulog2sumlem2  27483  mulog2sumlem3  27484  selberglem2  27494  selberg2  27499  chpdifbndlem1  27501  selberg3lem1  27505  pntrsumbnd2  27515  selbergr  27516  pntpbnd1  27534  pntpbnd2  27535  pntlemh  27547  pntlemj  27551  pntlemi  27552  pntlemf  27553  pntlemp  27558  ostth2lem1  27566  ostth1  27581  ostth2lem3  27583  ostth3  27586  noreson  27609  nosepon  27614  noextendseq  27616  nosupbnd1lem5  27661  noetasuplem4  27685  addscom  27919  negsdi  28002  om2noseqlt  28239  om2noseqf1o  28241  n0s0suc  28280  nnsge1  28281  n0sbday  28290  n0sfincut  28292  n0sltp1le  28301  bdayn0sf1o  28305  zaddscl  28328  elzn0s  28332  zsoring  28342  zseo  28355  zs12subscl  28399  remulscllem2  28413  istrkg2ld  28448  isismt  28522  eedimeq  28887  eqeefv  28892  brbtwn2  28894  colinearalglem1  28895  colinearalglem2  28896  colinearalg  28899  eleesub  28900  eleesubd  28901  axcgrrflx  28903  axcgrid  28905  axsegconlem2  28907  axsegconlem7  28912  axsegconlem9  28914  axsegconlem10  28915  axlowdimlem14  28944  axlowdimlem16  28946  axlowdimlem17  28947  axcontlem2  28954  axcontlem4  28956  axcontlem8  28960  axcontlem10  28962  structiedg0val  29011  upgr1eop  29104  numedglnl  29133  usgredg2v  29216  ushgredgedg  29218  ushgredgedgloop  29220  uspgr1eop  29236  usgr1eop  29239  uhgrissubgr  29264  umgrres1lem  29299  upgrres1  29302  nbuhgr  29332  edgnbusgreu  29356  nb3gr2nb  29373  uvtxnm1nbgr  29393  cusgrexilem2  29431  finsumvtxdg2ssteplem4  29538  vtxdgoddnumeven  29543  wlkeq  29623  uspgr2wlkeq  29635  wlksoneq1eq2  29652  upgrwlkdvdelem  29725  usgr2wlkspthlem1  29746  usgrn2cycl  29798  crctcshwlkn0lem3  29801  crctcshwlkn0lem6  29804  crctcshwlkn0lem7  29805  crctcshwlkn0  29810  wspthneq1eq2  29849  wwlkseq  29880  wwlksnext  29882  rusgrnumwlkg  29969  clwwlkccatlem  29980  clwwlkccat  29981  clwlkclwwlklem2a4  29988  clwlkclwwlklem2  29991  clwlkclwwlkf1lem3  29997  clwwisshclwwslemlem  30004  clwwisshclwws  30006  erclwwlkeqlen  30010  erclwwlkref  30011  clwwnisshclwwsn  30050  clwwlknccat  30054  erclwwlkneqlen  30059  hashecclwwlkn1  30068  umgrhashecclwwlk  30069  clwlksndivn  30077  uhgr3cyclex  30173  eucrctshift  30234  eucrct2eupth  30236  frgreu  30259  frgr3v  30266  3vfriswmgr  30269  frgrncvvdeqlem3  30292  frgrregorufrg  30317  numclwwlk1lem2f1  30348  numclwwlk1lem2fo  30349  numclwlk1lem2  30361  numclwwlk3  30376  numclwwlk6  30381  frgrreg  30385  frgrregord013  30386  nsnlplig  30472  nsnlpligALT  30473  ablodivdiv4  30545  imsdval  30677  nmcvcn  30686  sspval  30714  lnoadd  30749  lnosub  30750  nmooge0  30758  nmoolb  30762  nmoub3i  30764  blocnilem  30795  blocni  30796  cncph  30810  ipasslem1  30822  ipasslem2  30823  ipasslem4  30825  ipasslem11  30831  ipblnfi  30846  phoeqi  30848  ubthlem1  30861  ubthlem3  30863  htthlem  30908  hvsub4  31028  his7  31081  his2sub2  31084  hial2eq2  31098  hhip  31168  hhph  31169  bcs2  31173  hhssabloi  31253  hhssnv  31255  ocorth  31282  shsel  31305  shsel3  31306  shscli  31308  chsupss  31333  shjval  31342  chjval  31343  shjcl  31347  chjcl  31348  shsleji  31361  chslej  31489  chsscon2  31493  chjcom  31497  chub1  31498  chdmj1  31520  spanunsni  31570  spanpr  31571  fh1  31609  fh2  31610  cm2j  31611  spansncvi  31643  5oalem1  31645  5oalem3  31647  5oalem5  31649  3oalem2  31654  pjcompi  31663  pjds3i  31704  hoeq  31751  hoadddi  31794  hoadddir  31795  hosubdi  31799  hosub4  31804  hoeq1  31821  hoeq2  31822  adjval2  31882  counop  31912  adjeq  31926  brafnmul  31942  lnopsubi  31965  hmops  32011  hmopm  32012  hmopd  32013  hmopco  32014  nmcopexi  32018  lnconi  32024  lnfnsubi  32037  nmcfnexi  32042  imaelshi  32049  nlelshi  32051  riesz3i  32053  riesz1  32056  cnlnadjlem2  32059  cnlnadjlem6  32063  adjbdln  32074  adjlnop  32077  adjmul  32083  adjadd  32084  nmopcoi  32086  rnbra  32098  cnvbramul  32106  kbass2  32108  kbass4  32110  kbass5  32111  kbass6  32112  leopadd  32123  leopmul2i  32126  leoptri  32127  dmdmd  32291  mddmd  32292  cvdmd  32328  superpos  32345  chrelati  32355  atcv0eq  32370  atomli  32373  atcvatlem  32376  atcvati  32377  atcvat2i  32378  chirredlem4  32384  atcvat3i  32387  atcvat4i  32388  mdsymlem2  32395  mdsymlem3  32396  mdsymlem5  32398  mdsymlem8  32401  dmdsym  32404  cdjreui  32423  cdj1i  32424  cdj3lem2b  32428  cdj3lem3  32429  cdj3lem3b  32431  cdj3i  32432  brabgaf  32600  prct  32707  fcobijfs  32715  fzsplit3  32787  bcm1n  32788  dpfrac1  32883  wrdres  32927  xrge0mulgnn0  33007  xrge0tsmsd  33053  cycpmco2  33113  isarchiofld  33179  resvval  33305  nsgqusf1olem2  33390  lbslsat  33640  ply1degltdimlem  33646  ply1degltdim  33647  ordtrestNEW  33945  mhmhmeotmd  33951  xrge0iifcnv  33957  xrge0iifiso  33959  xrge0pluscn  33964  hasheuni  34109  sxval  34214  measvuni  34238  ddemeas  34260  br2base  34293  dya2iocucvr  34308  sxbrsigalem2  34310  sxbrsiga  34314  omssubadd  34324  eulerpartlemgc  34386  ballotlemfc0  34517  ballotlemfcc  34518  signstfvc  34598  signstres  34599  signsvfn  34606  bnj563  34766  bnj554  34922  bnj557  34924  bnj570  34928  bnj594  34935  bnj849  34948  bnj970  34970  bnj1118  35007  bnj1145  35016  bnj1190  35031  bnj1398  35057  bnj1417  35064  r1omfi  35127  zltp1ne  35165  nnltp1ne  35166  nn0ltp1ne  35167  0nn0m1nnn0  35168  cusgr3cyclex  35191  derangsn  35225  derangen  35227  subfacp1lem5  35239  erdsze2lem1  35258  txpconn  35287  txsconn  35296  cvmliftphtlem  35372  satfdm  35424  satfun  35466  ex-sategoelel  35476  mrsubff1  35569  msubff  35585  msubff1  35611  msubvrs  35615  inffz  35785  bcprod  35793  bccolsum  35794  faclim  35801  dfon2lem4  35839  colineardim1  36116  btwnconn1lem4  36145  btwnconn1lem5  36146  btwnconn1lem6  36147  btwnconn1lem8  36149  btwnconn1lem9  36150  btwnconn1lem12  36153  btwnconn1lem13  36154  btwnconn1lem14  36155  outsideofeu  36186  funray  36195  lineintmo  36212  fwddifnp1  36220  hfun  36233  nn0prpw  36378  opnregcld  36385  cldregopn  36386  ivthALT  36390  onsucconni  36492  bj-nnfim1  36799  bj-nnfim2  36800  bj-2uplex  37077  bj-unexg  37093  bj-prexg  37094  bj-idres  37215  isbasisrelowllem1  37410  isbasisrelowllem2  37411  icoreclin  37412  relowlssretop  37418  exrecfnlem  37434  pibt2  37472  unccur  37653  phpreu  37654  finixpnum  37655  ltflcei  37658  cos2h  37661  lindsadd  37663  lindsdom  37664  lindsenlbs  37665  matunitlindflem1  37666  matunitlindflem2  37667  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  heicant  37705  opnmbllem0  37706  mblfinlem1  37707  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  ovoliunnfl  37712  mbfresfi  37716  itg2addnclem  37721  itg2addnc  37724  itg2gt0cn  37725  ftc1cnnc  37742  ftc1anclem3  37745  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  ftc2nc  37752  indexa  37783  incsequz  37798  incsequz2  37799  geomcau  37809  sstotbnd2  37824  prdsbnd  37843  prdstotbnd  37844  prdsbnd2  37845  cntotbnd  37846  ismtyhmeolem  37854  ismtybndlem  37856  heibor1lem  37859  heiborlem3  37863  heiborlem6  37866  heibor  37871  bfplem1  37872  bfplem2  37873  elghomlem1OLD  37935  rngogrphom  38021  prnc  38117  ispridlc  38120  pridlc3  38123  mpobi123f  38212  mptbi12f  38216  antisymressn  38556  eqvreltr  38713  ax12indalem  39054  lsateln0  39104  atlatmstc  39428  hlatjidm  39478  llnneat  39623  lplnneat  39654  lplnnelln  39655  lvolneatN  39697  lvolnelln  39698  lvolnelpln  39699  dalem23  39805  snatpsubN  39859  linepsubN  39861  pmapsub  39877  pmapglbx  39878  paddasslem14  39942  polsubN  40016  pol1N  40019  2polvalN  40023  2polssN  40024  3polN  40025  2pmaplubN  40035  polatN  40040  2polatN  40041  pnonsingN  40042  polsubclN  40061  lautco  40206  cdlemefrs29cpre1  40507  dian0  41148  dia0eldmN  41149  dia1eldmN  41150  dia0  41161  dia1N  41162  dvhopaddN  41223  dib0  41273  dih0  41389  dih1  41395  dihglblem5apreN  41400  dihatexv2  41448  dochfN  41465  lcmineqlem1  42132  lcmineqlem17  42148  xppss12  42337  sumcubes  42421  dvdsexpnn  42441  remul01  42515  resubeqsub  42538  ricdrng1  42636  prjspeclsp  42720  ismrcd2  42806  nacsfix  42819  mzpaddmpt  42848  mzpmulmpt  42849  eq0rabdioph  42883  lerabdioph  42912  ltrabdioph  42915  nerabdioph  42916  dvdsrabdioph  42917  fiphp3d  42926  congneg  43076  jm2.22  43102  jm2.23  43103  jm2.15nn0  43110  jm3.1  43127  aomclem8  43168  lsmfgcl  43181  lmhmfgima  43191  lnmepi  43192  dgrsub2  43242  mpaaeu  43257  mendring  43295  proot1ex  43303  unielss  43325  onsucwordi  43395  oaabsb  43401  rp-oelim2  43415  nnoeomeqom  43419  cantnfresb  43431  oawordex2  43433  omcl3g  43441  ordsssucb  43442  tfsconcatrev  43455  onsucunipr  43479  onsucunitp  43480  oaun3lem1  43481  naddgeoa  43501  oaltom  43512  minregex2  43642  sssymdifcl  43679  relexp01min  43820  ntrclsiso  44174  ntrclsk3  44177  cvgdvgrat  44420  nznngen  44423  uzmptshftfval  44453  addrval  44572  subrval  44573  mulvval  44574  elpwgded  44671  eel2131  44820  eel3132  44821  el12  44832  sspwimp  45024  sspwimpcf  45026  suctrALTcf  45028  suctrALT3  45030  relpfrlem  45060  cnfex  45139  disjinfi  45303  infxrbnd2  45481  supminfxr  45576  climinf  45720  lptre2pt  45752  limcresiooub  45754  limcresioolb  45755  addlimc  45760  limclner  45763  limsuppnflem  45822  limsupmnfuzlem  45838  limsupvaluz2  45850  limsupresxr  45878  liminfresxr  45879  cnrefiisplem  45941  cncfdmsn  46002  iblspltprt  46085  itgspltprt  46091  dirkertrigeqlem3  46212  fourierdlem62  46280  fourierdlem80  46298  fourierdlem102  46320  fourierdlem103  46321  fourierdlem104  46322  fourierdlem114  46332  sge0f1o  46494  hoidmvlelem2  46708  pimdecfgtioo  46829  smfliminflem  46942  fnresfnco  47155  fcores  47181  dfatcolem  47369  nn0resubcl  47422  zgeltp1eq  47423  eluzge0nn0  47426  fz0addcom  47431  elfzlble  47434  fzopredsuc  47437  subsubelfzo0  47440  ceilbi  47447  minusmod5ne  47463  submodlt  47464  mod0mul  47470  m1modmmod  47472  uniimafveqt  47495  fundcmpsurinjimaid  47525  icceuelpartlem  47549  iccpartnel  47552  elsprel  47589  fmtnodvds  47658  goldbachth  47661  fmtnoprmfac2  47681  prmdvdsfmtnof1  47701  2pwp1prm  47703  flsqrt  47707  lighneallem4  47724  dfodd6  47751  divgcdoddALTV  47796  opoeALTV  47797  opeoALTV  47798  omoeALTV  47799  omeoALTV  47800  epoo  47817  emoo  47818  epee  47819  emee  47820  evensumeven  47821  even3prm2  47833  mogoldbblem  47834  fpprmod  47841  dfwppr  47852  fpprwppr  47853  fpprwpprb  47854  gbepos  47872  gbegt5  47875  gbowgt5  47876  gboge9  47878  sbgoldbst  47892  nnsum3primesgbe  47906  bgoldbtbndlem1  47919  bgoldbtbndlem2  47920  bgoldbtbndlem3  47921  grimco  48003  isuspgrim0  48008  isuspgrimlem  48009  uhgrimisgrgriclem  48044  uhgrimisgrgric  48045  clnbgrgrim  48048  grimedg  48049  isgrtri  48057  cycl3grtri  48061  isubgr3stgrlem6  48085  isubgr3stgrlem7  48086  isubgr3stgrlem8  48087  uspgrlimlem2  48103  uspgrlimlem3  48104  uspgrlimlem4  48105  grlictr  48129  gpgusgralem  48170  gpgedg2ov  48180  gpgnbgrvtx0  48188  gpgnbgrvtx1  48189  gpg5nbgrvtx03star  48194  gpg5nbgr3star  48195  gpg5grlic  48208  2zrngmmgm  48366  2zrngnmrid  48370  2zrngnmlid2  48371  altgsumbc  48466  altgsumbcALT  48467  zlmodzxzadd  48472  zlmodzxzsub  48474  invginvrid  48481  ply1mulgsumlem2  48502  ply1mulgsum  48505  lincvalpr  48533  lindslinindimp2lem1  48573  ldepsprlem  48587  ldepspr  48588  lincresunit3lem3  48589  lincresunitlem1  48590  lincresunit3lem1  48594  lincresunit3  48596  elfzolborelfzop1  48634  zgtp1leeq  48636  flsubz  48637  nneom  48642  nn0ofldiv2  48647  rege1logbrege0  48673  nnpw2pb  48702  dignn0fr  48716  dignn0ldlem  48717  dignnld  48718  dignn0flhalflem1  48730  nn0sumshdiglemB  48735  nn0mulfsum  48739  rrx2plordisom  48838  ehl2eudis0lt  48841  itsclinecirc0in  48890  2itscp  48896  inlinecirc02plem  48901  mof0ALT  48954  i0oii  49034  resccat  49189