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  3951  ssconb  4095  ineqan12d  4175  ifpr  4647  disjtp2  4670  dfopg  4825  disjxiun  5092  breqan12d  5111  eusv1  5333  opelvvg  5664  opthprc  5687  relop  5797  dmpropg  6168  unixp  6234  tz7.7  6337  ordin  6341  onin  6342  ontri1  6345  onfr  6350  onelpss  6351  onsseleq  6352  oneltri  6354  ontr2  6359  onunel  6418  onun2  6421  funssres  6530  funtpg  6541  funtp  6543  resasplit  6698  fodmrnu  6748  f1un  6788  dffv2  6922  fvreseq0  6976  fvcofneq  7031  funopdmsn  7088  fprg  7093  fprb  7134  fconst2g  7143  isofrlem  7281  oveqan12d  7372  ov3  7516  ovg  7518  ovima0  7532  f1opw2  7608  off  7635  unexgOLD  7689  pwuncl  7710  epweon  7715  epweonALT  7716  sucexeloni  7749  ordunpr  7765  omun  7828  peano4  7832  fabexg  7878  f1oabexg  7882  fiun  7885  offres  7925  el2mpocsbcl  8025  curry1  8044  curry1val  8045  curry2  8047  curry2val  8049  soxp  8069  wexp  8070  xpord2pred  8085  poxp3  8090  poseq  8098  soseq  8099  suppfnss  8129  frrlem4  8229  frrlem11  8236  frrlem12  8237  fprlem1  8240  iunon  8269  onfununi  8271  tfrlem11  8317  tz7.48lem  8370  seqomeq12  8383  oacan  8473  oawordri  8475  oaass  8486  omord2  8492  omcan  8494  oen0  8511  oeordi  8512  oeord  8513  oecan  8514  oeworde  8518  oeordsuc  8519  oelimcl  8525  nnawordi  8546  nnaword  8552  nnmord  8557  oaabslem  8572  omabslem  8575  omsmo  8583  eldifsucnn  8589  naddcllem  8601  naddov2  8604  ertr  8647  erex  8656  brecop  8744  ecopovtrn  8754  ecovdi  8759  mapvalg  8770  pmvalg  8771  pmss12g  8803  elmapresaun  8814  boxcutc  8875  undom  8989  sbthlem7  9017  sbth  9021  sdomnsym  9026  sdomdomtr  9034  xpf1o  9063  xpen  9064  limenpsi  9076  pssnn  9092  pwssfi  9101  sbthfi  9123  php2  9132  php3  9133  phpeqd  9136  nndomog  9137  onomeneq  9138  ominfOLD  9164  isinf  9165  isinfOLD  9166  fineqvlem  9167  f1finf1o  9174  en1eqsnOLD  9178  dif1ennnALT  9180  findcard3  9187  findcard3OLD  9188  unblem2  9198  isfinite2  9203  unfilem1  9212  unfi2  9217  fodomfir  9237  unifi2  9254  f1opwfi  9265  fsuppxpfi  9294  fsuppunbi  9298  fsuppco2  9312  fsuppcor  9313  fival  9321  fiin  9331  ordiso  9427  ordtypelem10  9438  hartogslem1  9453  wofib  9456  brwdom3  9493  unwdomg  9495  xpwdomg  9496  sucprcreg  9515  preleqALT  9532  inf3lem6  9548  oemapval  9598  cantnf  9608  wemapwe  9612  cnfcom  9615  ttrcltr  9631  dfttrcl2  9639  frmin  9664  r111  9690  r1ord3g  9694  prwf  9726  r1pw  9760  rankprb  9766  rankxplim  9794  tcrank  9799  updjud  9849  finnum  9863  xpnum  9866  carduni  9896  nnsdomel  9905  fidomtri  9908  infxpenlem  9926  fseqdom  9939  onssnum  9953  acndom2  9967  alephinit  10008  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem6  10069  undjudom  10081  endjudisj  10082  djuen  10083  djucomen  10091  pwdjuen  10095  djudom1  10096  djuxpdom  10099  djufi  10100  cardadju  10108  nnadju  10111  nnadjuALT  10112  ficardadju  10113  ficardun  10114  ficardun2  10115  pwsdompw  10116  unctb  10117  ackbij2lem1  10131  ackbij1lem6  10137  ackbij1lem16  10147  ackbij1b  10151  ackbij2  10155  coflim  10174  cflim2  10176  cofsmo  10182  coftr  10186  sornom  10190  infpssrlem5  10220  fin4en1  10222  fin23lem23  10239  fin23lem28  10253  isf32lem2  10267  isf32lem4  10269  isf32lem7  10272  isf34lem7  10292  isf34lem6  10293  fin67  10308  isfin7-2  10309  fin1a2lem9  10321  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  zorn2lem6  10414  ttukeylem3  10424  brdom6disj  10445  carddom  10467  cardsdom  10468  domtri  10469  konigthlem  10481  iunctb  10487  alephadd  10490  alephmul  10491  pwcfsdom  10496  cfpwsdom  10497  fpwwe2lem12  10555  canthp1lem2  10566  pwfseqlem3  10573  pwfseqlem4a  10574  inar1  10688  tskcard  10694  tskuni  10696  grur1  10733  mulclpi  10806  addcompi  10807  mulcompi  10809  distrpi  10811  ltexpi  10815  ltapi  10816  ltmpi  10817  enqbreq2  10833  nqereu  10842  addpipq  10850  addpqnq  10851  mulpipq  10853  mulpqnq  10854  addpqf  10857  addclnq  10858  mulpqf  10859  mulclnq  10860  adderpq  10869  mulerpq  10870  ltsonq  10882  lterpq  10883  ltbtwnnq  10891  ltrnq  10892  genpv  10912  genpdm  10915  genpnnp  10918  mulclprlem  10932  distrlem1pr  10938  distrlem4pr  10939  prlem934  10946  addcanpr  10959  suplem1pr  10965  mulcmpblnr  10984  mulclsr  10997  mulasssr  11003  distrsr  11004  ltsosr  11007  1idsr  11011  00sr  11012  recexsrlem  11016  mulgt0sr  11018  addcnsr  11048  axmulf  11059  axmulass  11070  axdistr  11071  axcnre  11077  mulrid  11132  axltadd  11207  lenlt  11212  dedekind  11297  dedekindle  11298  resubcl  11446  subeqrev  11560  muladd  11570  mulsub  11581  mulsub2  11582  ltaddsub2  11613  leaddsub2  11615  leltadd  11622  ltaddpos2  11629  posdif  11631  addge02  11649  mullt0  11657  ltord1  11664  leord1  11665  eqord1  11666  recextlem1  11768  recex  11770  divmuldiv  11842  conjmul  11859  div2sub  11967  prodgt02  11990  lemul2  11995  lemul2a  11997  ltmulgt12  12003  lemulge12  12006  mulge0b  12013  mulle0b  12014  ltmuldiv2  12017  ltdivmul2  12020  lt2mul2div  12021  ledivmul2  12022  lemuldiv2  12024  ledivdiv  12032  lediv2  12033  ltdiv23  12034  lediv23  12035  supmul  12115  riotaneg  12122  negiso  12123  cju  12142  nnaddcl  12169  nnmulcl  12170  nnmtmip  12172  nnsub  12190  addltmul  12378  avgle1  12382  avgle2  12383  avgle  12384  nnrecl  12400  nn0nnaddcl  12433  nn0sub  12452  elz2  12507  zaddcl  12533  zsubcl  12535  znnsub  12539  znn0sub  12540  nzadd  12541  zmulcl  12542  zltp1le  12543  zleltp1  12544  nnleltp1  12549  nnltp1le  12550  nnaddm1cl  12551  nn0ltp1le  12552  nn0leltp1  12553  nn0ltlem1  12554  nn0lem1lt  12559  nnlem1lt  12560  nnltlem1  12561  zdiv  12564  zextle  12567  zextlt  12568  btwnnz  12570  prime  12575  nneo  12578  peano2uz2  12582  uzind  12586  fzind  12592  zriotaneg  12607  uzneg  12773  uztric  12777  uz11  12778  eluzp1m1  12779  eluzp1p1  12781  uzin  12793  uzwo  12830  indstr  12835  uz2mulcl  12845  supminf  12854  uzsupss  12859  zmax  12864  rebtwnz  12866  qre  12872  qaddcl  12884  qsubcl  12887  irradd  12892  elpqb  12895  rpnnen1lem5  12900  cnref1o  12904  rpaddcl  12935  rpmulcl  12936  rpmtmip  12937  rpdivcl  12938  max1  13105  max2  13107  min1  13109  min2  13110  z2ge  13118  qbtwnxr  13120  xaddf  13144  rexadd  13152  rexsub  13153  xnn0xaddcl  13155  xaddcom  13160  xnn0xadd0  13167  xnegdi  13168  rexmul  13191  supxrbnd2  13242  ixxin  13283  elicc2  13332  difreicc  13405  iccshftr  13407  iccshftl  13409  iccdil  13411  icccntr  13413  fzval2  13431  elfz1eq  13456  peano2fzr  13458  fzn  13461  fzsplit2  13470  fzaddel  13479  fzadd2  13480  fzsubel  13481  fzrev2  13509  fzrev3  13511  uzsplit  13517  fznuz  13530  uznfz  13531  fzrevral  13533  fzrevral3  13535  fzshftral  13536  elfz2nn0  13539  fznn0sub2  13556  fz0fzdiffz0  13558  elfzmlbp  13560  difelfzle  13562  difelfznle  13563  elfzouz2  13595  fzo0n  13602  fzouzsplit  13615  fzoun  13617  elfzo0le  13624  fzonmapblen  13629  fzofzim  13630  fzoaddel2  13641  eluzgtdifelfzo  13648  elfzodifsumelfzo  13652  ssfzoulel  13681  ubmelm1fzo  13684  fzofzp1b  13686  elfzonelfzo  13690  elfznelfzo  13693  fzostep1  13704  injresinjlem  13708  subfzo0  13710  flflp1  13729  divfl0  13746  flzadd  13748  flmulnn0  13749  fldivnn0le  13754  fldiv  13782  uzsup  13785  mulmod0  13799  modlt  13802  modmulnn  13811  zmodcl  13813  zmodfz  13815  zmodid2  13821  modcyc  13828  muladdmodid  13835  modmuladdnn0  13840  negmod  13841  addmodidr  13845  modadd2mod  13846  modaddmodup  13859  modaddmulmod  13863  modfzo0difsn  13868  modsumfzodifsn  13869  addmodlteq  13871  om2uzlti  13875  om2uzf1oi  13878  fzen2  13894  ssnn0fi  13910  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub0  13918  seqshft2  13953  seqsplit  13960  seqcaopr2  13963  seqf1olem2  13967  expcllem  13997  expcl2lem  13998  1exp  14016  expge1  14024  expadd  14029  expmul  14032  expsub  14035  nn0sq11  14057  lt2sq  14058  le2sq  14059  expmordi  14092  leexp2  14096  leexp1a  14100  sumsqeq0  14104  bernneq  14154  bernneq2  14155  expnbnd  14157  digit2  14161  digit1  14162  facdiv  14212  facwordi  14214  faclbnd  14215  faclbnd3  14217  faclbnd4lem4  14221  faclbnd5  14223  faclbnd6  14224  facavg  14226  bcrpcl  14233  bccmpl  14234  bcval5  14243  hashen  14272  hasheqf1oi  14276  hashgadd  14302  hashdom  14304  hashsdom  14306  hashun  14307  hashunsnggt  14319  hashprg  14320  hashssdif  14337  hashxplem  14358  seqcoll  14389  tpf1o  14426  eqwrd  14482  ccatfval  14498  ccatlen  14500  ccat0  14501  elfzelfzccat  14505  ccatsymb  14507  ccatval21sw  14510  ccatrn  14514  lswccatn0lsw  14516  ccatalpha  14518  ccatrcl1  14519  ccats1alpha  14544  swrdnd  14579  swrdfv2  14586  swrdsbslen  14589  swrdspsleq  14590  swrdccat2  14594  pfxnd0  14613  pfxeq  14620  ccatpfx  14625  pfxccat1  14626  swrdswrdlem  14628  pfxswrd  14630  pfxccatin12lem4  14650  pfxccatin12lem1  14652  pfxccatin12lem2  14655  pfxccatin12lem3  14656  pfxccatin12  14657  pfxccat3  14658  swrdccat  14659  pfxccatpfx2  14661  pfxccat3a  14662  swrdccat3blem  14663  swrdccat3b  14664  revccat  14690  revrev  14691  cshwlen  14723  cshwidxmod  14727  cshwidxmodr  14728  cshweqdif2  14743  cshweqrep  14745  2cshwcshw  14750  s3eq3seq  14864  cotr2g  14901  trclun  14939  shftf  15004  seqshft  15010  crre  15039  crim  15040  readd  15051  resub  15052  remul2  15055  imadd  15059  imsub  15060  immul2  15062  ipcnval  15068  cjsub  15074  cjreim  15085  01sqrexlem6  15172  sqrtle  15185  sqrt11  15187  absreimsq  15217  absreim  15218  absmul  15219  sqabs  15232  absdiflt  15243  absdifle  15244  abssuble0  15254  absmax  15255  abs2difabs  15260  fzomaxdif  15269  rexanuz  15271  rexuz3  15274  rexuzre  15278  caubnd2  15283  limsupgre  15406  limsupbnd2  15408  climconst2  15473  lo1resb  15489  o1resb  15491  2clim  15497  climshftlem  15499  climshft  15501  climshft2  15507  cjcn2  15525  o1of2  15538  o1rlimmul  15544  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  lo1le  15577  climlec2  15584  isershft  15589  isercolllem1  15590  isercolllem3  15592  isercoll  15593  isercoll2  15594  climsup  15595  caurcvg  15602  caucvg  15604  iseraltlem1  15607  iseraltlem2  15608  iseralt  15610  summolem2a  15640  isumclim3  15684  mptfzshft  15703  fsumrev  15704  fsum0diag2  15708  fsumconst  15715  telfsumo2  15728  fsumparts  15731  o1fsum  15738  cvgcmp  15741  cvgcmpub  15742  cvgcmpce  15743  binomlem  15754  binom1p  15756  binom1dif  15758  bcxmas  15760  incexclem  15761  incexc  15762  incexc2  15763  isumshft  15764  isumsplit  15765  isumsup2  15771  climcndslem1  15774  climcndslem2  15775  climcnds  15776  supcvg  15781  expcnv  15789  geoserg  15791  pwdif  15793  geolim  15795  geoisum1  15804  geoisum1c  15805  cvgrat  15808  mertenslem1  15809  mertenslem2  15810  mertens  15811  ntrivcvgfvn0  15824  ntrivcvgmullem  15826  prodmolem2a  15859  prodmo  15861  fprodf1o  15871  fproddiv  15886  fprodeq0  15900  risefacval2  15935  fallfacval2  15936  fallfacval3  15937  rprisefaccl  15948  risefallfac  15949  fallfacfwd  15961  binomfallfaclem1  15964  binomfallfaclem2  15965  binomrisefac  15967  bpolycl  15977  bpolysum  15978  bpolydiflem  15979  fsumkthpow  15981  efcj  16017  fprodefsum  16020  efexp  16028  eftlub  16036  effsumlt  16038  efle  16045  reef11  16046  efieq  16090  sinsub  16095  cossub  16096  subsin  16098  sinmul  16099  cosmul  16100  addcos  16101  subcos  16102  rpnnen2lem10  16150  rpnnen2lem12  16152  ruclem8  16164  ruclem12  16168  sqrt2irr  16176  dvdssub2  16230  dvdsadd  16231  dvdsaddr  16232  dvdssub  16233  dvdssubr  16234  dvdsle  16239  alzdvds  16249  fzocongeq  16253  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  pwp1fsum  16320  divalglem4  16325  divalglem9  16330  divalgb  16333  divalgmod  16335  ndvdsadd  16339  smueqlem  16419  gcdaddm  16454  modgcd  16461  bezoutlem1  16468  dvdsgcd  16473  absmulgcd  16478  rpmulgcd  16486  rprpwr  16488  sqgcd  16491  dvdssqlem  16495  dvdssq  16496  nn0seqcvgd  16499  algrf  16502  algcvg  16505  lcmcllem  16525  lcmabs  16534  lcmgcd  16536  lcmdvds  16537  lcmgcdnn  16540  lcmf  16562  coprmgcdb  16578  coprmdvds  16582  coprmdvds2  16583  qredeq  16586  isprm3  16612  nprm  16617  oddprmgt2  16628  isprm5  16636  isprm7  16637  divgcdodd  16639  prmdvdsexp  16644  zgcdsq  16682  hashdvds  16704  phiprmpw  16705  crth  16707  phimullem  16708  modprm0  16735  coprimeprodsq  16738  coprimeprodsq2  16739  pythagtriplem2  16747  pythagtriplem19  16763  iserodd  16765  pcpremul  16773  pcmul  16781  pcexp  16789  pcdvdsb  16799  pcneg  16804  pc2dvds  16809  pc11  16810  pcmpt  16822  fldivp1  16827  pcfac  16829  infpnlem1  16840  prmunb  16844  prmreclem1  16846  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  1arithlem4  16856  1arith  16857  gzaddcl  16867  gzmulcl  16868  gzreim  16869  gzsubcl  16870  4sqlem1  16878  4sqlem4a  16881  4sqlem4  16882  4sqlem12  16886  ramlb  16949  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  prmgaplem7  16987  prmgaplem8  16988  prmgapprmolem  16991  cshwshashlem2  17026  setsvalg  17095  ressval  17162  ressval3d  17175  restval  17348  pwsval  17408  xpsval  17492  ssclem  17744  rescval  17752  funcestrcsetclem9  18072  embedsetcestrclem  18081  lubel  18438  ipodrsima  18465  tsrss  18513  resmgmhm  18603  resmgmhm2  18604  mgmhmco  18606  submnd0  18655  mndinvmod  18656  xpsmnd0  18670  resmhm  18712  resmhm2  18713  mhmco  18715  frmdplusg  18746  frmdmnd  18751  efmndcl  18774  smndex1id  18803  mgm2nsgrplem1  18810  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  sgrp2nmndlem1  18815  sgrp2rid2  18818  dfgrp3  18936  mhmmnd  18961  mulgnngsum  18976  mulgnnsubcl  18983  mulgnn0z  18998  mulgnndir  19000  mulgmodid  19010  eqgfval  19073  cycsubgcl  19103  cycsubg2  19107  0ghm  19127  resghm  19129  resghm2  19130  ghmco  19133  ghmeql  19136  isgim  19159  gicsubgen  19176  cntzmhm  19238  symgcl  19282  symgextf1  19318  gsmsymgrfixlem1  19324  symgfixf1  19334  symgtrinv  19369  pmtrdifellem3  19375  mndodcongi  19440  odmod  19443  odf1  19459  odf1o1  19469  gexdvds  19481  sylow1lem1  19495  pgpssslw  19511  lsmub1  19554  lsmub2  19555  cntzrecd  19575  pj1ghm  19600  lsmhash  19602  efgred  19645  frgpup1  19672  ablsubadd23  19710  ablsubsub23  19721  mulgnn0di  19722  torsubg  19751  zaddablx  19769  gsumzaddlem  19818  gsumzadd  19819  gsumconst  19831  gsumzmhm  19834  telgsumfzslem  19885  dprdfadd  19919  dprd2dlem1  19940  ablsimpgfindlem1  20006  srgbinomlem3  20131  srgbinomlem4  20132  srgbinomlem  20133  gsummgp0  20221  gsumdixp  20222  xpsring1d  20236  unitnegcl  20300  isrnghm  20344  rnghmco  20360  dfrhm2  20377  rhmco  20404  c0rhm  20437  c0rnghm  20438  rhmimasubrng  20469  cntzsubrng  20470  issubrg3  20503  resrhm  20504  rhmeql  20506  rhmima  20507  isdomn4  20619  imadrhmcl  20700  fldsdrgfld  20701  abvres  20734  suborng  20779  lmodfopne  20821  lspf  20895  lspcl  20897  0lmhm  20962  lmhmco  20965  lmhmeql  20977  islmim  20984  rngqiprngghm  21224  rngqiprnglin  21227  xrsdsreval  21336  xrsdsreclb  21338  xrs1cmn  21367  xrge0omnd  21370  znfld  21485  znchr  21487  znunithash  21489  znrrg  21490  freshmansdream  21499  cnmsgnsubg  21502  zrhpsgnmhm  21509  evpmodpmf1o  21521  psgndiflemB  21525  psgndif  21527  phlssphl  21584  frlmval  21673  uvcfval  21709  frlmsslsp  21721  frlmup2  21724  lindfmm  21752  lmimlbs  21761  islindf4  21763  issubassa3  21791  psrbaglesupp  21847  psrcom  21893  resspsrmul  21901  mplsubrglem  21929  mplcoe3  21961  ltbval  21966  ltbwe  21967  evlslem4  21999  evlslem3  22003  psdmvr  22072  psropprmul  22138  coe1tmmul  22179  cply1mul  22199  gsummoncoe1  22211  lply1binomsc  22214  pf1ind  22258  mamufacex  22299  grpvlinv  22301  grpvrinv  22302  eqmat  22327  mat1dimcrng  22380  dmatcrng  22405  scmatf1  22434  m1detdiag  22500  mdetdiaglem  22501  mdet1  22504  mdetunilem9  22523  madulid  22548  gsummatr01lem4  22561  gsummatr01  22562  mat2pmatlin  22638  m2pmfzgsumcl  22651  monmatcollpw  22682  pmatcollpw3lem  22686  mp2pm2mplem4  22712  chpscmatgsummon  22748  chfacfscmulfsupp  22762  chfacfpmmulfsupp  22766  cayhamlem1  22769  cpmadugsumlemF  22779  clsval2  22953  innei  23028  ordtrest  23105  ordtrestixx  23125  isnrm2  23261  lpcls  23267  tgcmp  23304  cmpcld  23305  uncmp  23306  hauscmplem  23309  hauscmp  23310  1stcfb  23348  1stcrest  23356  kgencmp2  23449  1stckgenlem  23456  kgen2ss  23458  kgencn  23459  kgencn3  23461  txval  23467  txuni2  23468  txbasex  23469  txbas  23470  txtop  23472  ptbasin  23480  txtopon  23494  txcld  23506  txss12  23508  txbasval  23509  xkoccn  23522  txcnp  23523  ptcnplem  23524  upxp  23526  txcnmpt  23527  uptx  23528  txrest  23534  txdis  23535  txindislem  23536  txlly  23539  txnlly  23540  txcmp  23546  hausdiag  23548  txhaus  23550  tx1stc  23553  tx2ndc  23554  txkgen  23555  xkoptsub  23557  cnmpt21  23574  txconn  23592  qtopval  23598  hmeoco  23675  txhmeo  23706  xpstopnlem1  23712  fbun  23743  filss  23756  infil  23766  fbunfip  23772  filuni  23788  fmfnfmlem4  23860  ufldom  23865  flffval  23892  flfval  23893  txflf  23909  fcfval  23936  alexsubALTlem3  23952  tgpmulg  23996  subgtgp  24008  qustgplem  24024  tsmsfbas  24031  tsmsres  24047  tsmsmhm  24049  tsmsadd  24050  isxmet2d  24231  blin2  24333  comet  24417  met2ndci  24426  metcn  24447  txmetcn  24452  dscopn  24477  nrmmetd  24478  isngp3  24502  tngval  24543  nm1  24571  subrgnrg  24577  nrginvrcn  24596  rlmnvc  24607  nmo0  24639  nmoco  24641  nghmco  24642  nmotri  24643  0nghm  24645  isnmhm2  24656  0nmhm  24659  nmhmco  24660  nmhmplusg  24661  qtopbaslem  24662  remetdval  24693  bl2ioo  24696  reperflem  24723  iccntr  24726  icccmplem2  24728  icccmp  24730  reconnlem2  24732  xrge0gsumle  24738  xrge0tsms  24739  divcnOLD  24773  divcn  24775  cncfmet  24818  iccpnfcnv  24858  bndth  24873  copco  24934  pcopt  24938  pcopt2  24939  nmhmcn  25036  cmodscexp  25037  cphassr  25128  lmmbrf  25178  lmnn  25179  iscauf  25196  caucfil  25199  iscmet3lem1  25207  iscmet3lem2  25208  iscmet3  25209  cfilres  25212  caussi  25213  caubl  25224  caublcls  25225  bcthlem2  25241  bcthlem5  25244  cmsss  25267  lssbn  25268  ovolfioo  25384  ovollb2lem  25405  ovolunlem1a  25413  ovoliunlem1  25419  ovoliunlem2  25420  ovoliunlem3  25421  ovoliun2  25423  ovolscalem1  25430  ovolicc2lem1  25434  ovolicc2lem4  25437  ovolicc2lem5  25438  inmbl  25459  voliunlem1  25467  volsup  25473  ioombl1lem4  25478  iccvolcl  25484  ioovolcl  25487  uniioovol  25496  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombllem6  25505  dyadf  25508  dyadovol  25510  dyadss  25511  dyadmbl  25517  opnmbllem  25518  volsup2  25522  volcn  25523  ismbf  25545  mbfima  25547  ismbf3d  25571  mbfadd  25578  mbfsub  25579  mbflimsup  25583  itg1mulc  25621  itg1sub  25626  itg1climres  25631  mbfi1fseqlem1  25632  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfmul  25643  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2lea  25661  itg2eqa  25662  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2i1fseqle  25671  itg2i1fseq  25672  itg2i1fseq2  25673  itg2addlem  25675  itg2cnlem1  25678  bddmulibl  25756  ellimc3  25796  dvaddbr  25856  dvcobr  25865  dvcobrOLD  25866  dvcjbr  25869  dvcnvlem  25896  c1lip1  25918  lhop  25937  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumrlimf  25947  dvfsumlem1  25948  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsum2  25957  tdeglem4  25981  deg1ge  26019  coe1mul3  26020  fta1g  26091  plyco0  26113  plyf  26119  ply1termlem  26124  plyeq0lem  26131  plypf1  26133  plymullem1  26135  plyaddlem  26136  plymullem  26137  coeeulem  26145  coeidlem  26158  plyco  26162  dgreq  26165  coefv0  26169  coeaddlem  26170  coemullem  26171  coemulhi  26175  coemulc  26176  plycn  26182  plycnOLD  26183  dgrlt  26188  dgrsub  26194  plycjlem  26198  plycj  26199  plycjOLD  26201  plyrecj  26203  plymul0or  26204  plyreres  26206  dvply1  26207  vieta1lem2  26235  plyexmo  26237  elqaalem2  26244  elqaalem3  26245  aareccl  26250  aalioulem1  26256  aalioulem3  26258  aaliou  26262  geolim3  26263  ulmcaulem  26319  ulmcau  26320  mtest  26329  dvradcnv  26346  psercn2  26348  psercn2OLD  26349  pserdvlem2  26354  pserdv2  26356  abelthlem6  26362  abelthlem8  26365  abelthlem9  26366  reeff1o  26373  reefgim  26376  sinperlem  26405  sincosq2sgn  26424  sincosq3sgn  26425  sinq12ge0  26433  sincos6thpi  26441  sineq0  26449  cosord  26456  cos11  26458  sinord  26459  tanord1  26462  eff1olem  26473  logrnaddcl  26499  relogeftb  26509  relogoprlem  26516  logleb  26528  advlogexp  26580  logtayllem  26584  logtayl  26585  logtaylsum  26586  logtayl2  26587  recxpcl  26600  rpcxpcl  26601  cxple3  26626  cxpcom  26664  cxpcn3  26674  cxpeq  26683  relogbmul  26703  relogbcxp  26711  relogbf  26717  atanord  26853  atantayl  26863  birthdaylem2  26878  birthdaylem3  26879  cxp2limlem  26902  fsumharmonic  26938  zetacvg  26941  ftalem1  26999  ftalem4  27002  ftalem5  27003  basellem2  27008  basellem3  27009  basellem4  27010  vmappw  27042  sqf11  27065  mumul  27107  fsumdvdscom  27111  dvdsppwf1o  27112  dvdsflf1o  27113  musum  27117  muinv  27119  fsumdvdsmul  27121  1sgmprm  27126  vmalelog  27132  chtublem  27138  fsumvma  27140  vmasum  27143  logfac2  27144  chpval2  27145  logfaclbnd  27149  logexprlim  27152  mersenne  27154  dchrmulcl  27176  dchrinvcl  27180  dchrfi  27182  dchrghm  27183  dchrptlem1  27191  dchrsum2  27195  dchrsum  27196  pcbcctr  27203  bcmono  27204  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem5  27215  bposlem6  27216  bposlem7  27217  lgslem3  27226  lgscllem  27231  lgsval4a  27246  lgsneg  27248  lgsdir2  27257  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  gausslemma2dlem1a  27292  gausslemma2dlem3  27295  gausslemma2dlem6  27299  lgseisenlem3  27304  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2  27313  lgsquad3  27314  2lgslem1a1  27316  2lgslem1a  27318  2lgslem1c  27320  2sqlem2  27345  mul2sq  27346  2sqlem7  27351  2sqreultlem  27374  2sqreunnltlem  27377  2sqreunnltblem  27378  chebbnd1lem1  27396  vmadivsum  27409  rplogsumlem2  27412  dchrisum0lem1a  27413  rpvmasumlem  27414  dchrisumlem1  27416  dchrisumlem2  27417  dchrisumlem3  27418  dchrmusumlema  27420  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasum2if  27424  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrvmasumiflem2  27429  dchrisum0ff  27434  dchrisum0flblem1  27435  dchrisum0fno1  27438  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  mudivsum  27457  mulogsum  27459  mulog2sumlem1  27461  mulog2sumlem2  27462  mulog2sumlem3  27463  selberglem2  27473  selberg2  27478  chpdifbndlem1  27480  selberg3lem1  27484  pntrsumbnd2  27494  selbergr  27495  pntpbnd1  27513  pntpbnd2  27514  pntlemh  27526  pntlemj  27530  pntlemi  27531  pntlemf  27532  pntlemp  27537  ostth2lem1  27545  ostth1  27560  ostth2lem3  27562  ostth3  27565  noreson  27588  nosepon  27593  noextendseq  27595  nosupbnd1lem5  27640  noetasuplem4  27664  addscom  27896  negsdi  27979  om2noseqlt  28216  om2noseqf1o  28218  n0s0suc  28257  nnsge1  28258  n0sbday  28267  n0sfincut  28269  n0sltp1le  28278  bdayn0sf1o  28282  zaddscl  28305  elzn0s  28309  zsoring  28319  zseo  28332  zs12subscl  28374  remulscllem2  28388  istrkg2ld  28423  isismt  28497  eedimeq  28861  eqeefv  28866  brbtwn2  28868  colinearalglem1  28869  colinearalglem2  28870  colinearalg  28873  eleesub  28874  eleesubd  28875  axcgrrflx  28877  axcgrid  28879  axsegconlem2  28881  axsegconlem7  28886  axsegconlem9  28888  axsegconlem10  28889  axlowdimlem14  28918  axlowdimlem16  28920  axlowdimlem17  28921  axcontlem2  28928  axcontlem4  28930  axcontlem8  28934  axcontlem10  28936  structiedg0val  28985  upgr1eop  29078  numedglnl  29107  usgredg2v  29190  ushgredgedg  29192  ushgredgedgloop  29194  uspgr1eop  29210  usgr1eop  29213  uhgrissubgr  29238  umgrres1lem  29273  upgrres1  29276  nbuhgr  29306  edgnbusgreu  29330  nb3gr2nb  29347  uvtxnm1nbgr  29367  cusgrexilem2  29405  finsumvtxdg2ssteplem4  29512  vtxdgoddnumeven  29517  wlkeq  29597  uspgr2wlkeq  29609  wlksoneq1eq2  29626  upgrwlkdvdelem  29699  usgr2wlkspthlem1  29720  usgrn2cycl  29772  crctcshwlkn0lem3  29775  crctcshwlkn0lem6  29778  crctcshwlkn0lem7  29779  crctcshwlkn0  29784  wspthneq1eq2  29823  wwlkseq  29854  wwlksnext  29856  rusgrnumwlkg  29940  clwwlkccatlem  29951  clwwlkccat  29952  clwlkclwwlklem2a4  29959  clwlkclwwlklem2  29962  clwlkclwwlkf1lem3  29968  clwwisshclwwslemlem  29975  clwwisshclwws  29977  erclwwlkeqlen  29981  erclwwlkref  29982  clwwnisshclwwsn  30021  clwwlknccat  30025  erclwwlkneqlen  30030  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  clwlksndivn  30048  uhgr3cyclex  30144  eucrctshift  30205  eucrct2eupth  30207  frgreu  30230  frgr3v  30237  3vfriswmgr  30240  frgrncvvdeqlem3  30263  frgrregorufrg  30288  numclwwlk1lem2f1  30319  numclwwlk1lem2fo  30320  numclwlk1lem2  30332  numclwwlk3  30347  numclwwlk6  30352  frgrreg  30356  frgrregord013  30357  nsnlplig  30443  nsnlpligALT  30444  ablodivdiv4  30516  imsdval  30648  nmcvcn  30657  sspval  30685  lnoadd  30720  lnosub  30721  nmooge0  30729  nmoolb  30733  nmoub3i  30735  blocnilem  30766  blocni  30767  cncph  30781  ipasslem1  30793  ipasslem2  30794  ipasslem4  30796  ipasslem11  30802  ipblnfi  30817  phoeqi  30819  ubthlem1  30832  ubthlem3  30834  htthlem  30879  hvsub4  30999  his7  31052  his2sub2  31055  hial2eq2  31069  hhip  31139  hhph  31140  bcs2  31144  hhssabloi  31224  hhssnv  31226  ocorth  31253  shsel  31276  shsel3  31277  shscli  31279  chsupss  31304  shjval  31313  chjval  31314  shjcl  31318  chjcl  31319  shsleji  31332  chslej  31460  chsscon2  31464  chjcom  31468  chub1  31469  chdmj1  31491  spanunsni  31541  spanpr  31542  fh1  31580  fh2  31581  cm2j  31582  spansncvi  31614  5oalem1  31616  5oalem3  31618  5oalem5  31620  3oalem2  31625  pjcompi  31634  pjds3i  31675  hoeq  31722  hoadddi  31765  hoadddir  31766  hosubdi  31770  hosub4  31775  hoeq1  31792  hoeq2  31793  adjval2  31853  counop  31883  adjeq  31897  brafnmul  31913  lnopsubi  31936  hmops  31982  hmopm  31983  hmopd  31984  hmopco  31985  nmcopexi  31989  lnconi  31995  lnfnsubi  32008  nmcfnexi  32013  imaelshi  32020  nlelshi  32022  riesz3i  32024  riesz1  32027  cnlnadjlem2  32030  cnlnadjlem6  32034  adjbdln  32045  adjlnop  32048  adjmul  32054  adjadd  32055  nmopcoi  32057  rnbra  32069  cnvbramul  32077  kbass2  32079  kbass4  32081  kbass5  32082  kbass6  32083  leopadd  32094  leopmul2i  32097  leoptri  32098  dmdmd  32262  mddmd  32263  cvdmd  32299  superpos  32316  chrelati  32326  atcv0eq  32341  atomli  32344  atcvatlem  32347  atcvati  32348  atcvat2i  32349  chirredlem4  32355  atcvat3i  32358  atcvat4i  32359  mdsymlem2  32366  mdsymlem3  32367  mdsymlem5  32369  mdsymlem8  32372  dmdsym  32375  cdjreui  32394  cdj1i  32395  cdj3lem2b  32399  cdj3lem3  32400  cdj3lem3b  32402  cdj3i  32403  brabgaf  32569  prct  32671  fcobijfs  32679  fzsplit3  32749  bcm1n  32751  dpfrac1  32845  wrdres  32889  xrge0mulgnn0  32982  xrge0tsmsd  33028  cycpmco2  33088  isarchiofld  33151  resvval  33277  nsgqusf1olem2  33361  lbslsat  33588  ply1degltdimlem  33594  ply1degltdim  33595  ordtrestNEW  33887  mhmhmeotmd  33893  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0pluscn  33906  hasheuni  34051  sxval  34156  measvuni  34180  ddemeas  34202  br2base  34236  dya2iocucvr  34251  sxbrsigalem2  34253  sxbrsiga  34257  omssubadd  34267  eulerpartlemgc  34329  ballotlemfc0  34460  ballotlemfcc  34461  signstfvc  34541  signstres  34542  signsvfn  34549  bnj563  34709  bnj554  34865  bnj557  34867  bnj570  34871  bnj594  34878  bnj849  34891  bnj970  34913  bnj1118  34950  bnj1145  34959  bnj1190  34974  bnj1398  35000  bnj1417  35007  zltp1ne  35082  nnltp1ne  35083  nn0ltp1ne  35084  0nn0m1nnn0  35085  cusgr3cyclex  35108  derangsn  35142  derangen  35144  subfacp1lem5  35156  erdsze2lem1  35175  txpconn  35204  txsconn  35213  cvmliftphtlem  35289  satfdm  35341  satfun  35383  ex-sategoelel  35393  mrsubff1  35486  msubff  35502  msubff1  35528  msubvrs  35532  inffz  35702  bcprod  35710  bccolsum  35711  faclim  35718  dfon2lem4  35759  colineardim1  36034  btwnconn1lem4  36063  btwnconn1lem5  36064  btwnconn1lem6  36065  btwnconn1lem8  36067  btwnconn1lem9  36068  btwnconn1lem12  36071  btwnconn1lem13  36072  btwnconn1lem14  36073  outsideofeu  36104  funray  36113  lineintmo  36130  fwddifnp1  36138  hfun  36151  nn0prpw  36296  opnregcld  36303  cldregopn  36304  ivthALT  36308  onsucconni  36410  bj-nnfim1  36717  bj-nnfim2  36718  bj-2uplex  36995  bj-unexg  37011  bj-prexg  37012  bj-idres  37133  isbasisrelowllem1  37328  isbasisrelowllem2  37329  icoreclin  37330  relowlssretop  37336  exrecfnlem  37352  pibt2  37390  unccur  37582  phpreu  37583  finixpnum  37584  ltflcei  37587  cos2h  37590  lindsadd  37592  lindsdom  37593  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem13  37612  poimirlem14  37613  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem24  37623  poimirlem26  37625  poimirlem27  37626  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  heicant  37634  opnmbllem0  37635  mblfinlem1  37636  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  ovoliunnfl  37641  mbfresfi  37645  itg2addnclem  37650  itg2addnc  37653  itg2gt0cn  37654  ftc1cnnc  37671  ftc1anclem3  37674  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  ftc2nc  37681  indexa  37712  incsequz  37727  incsequz2  37728  geomcau  37738  sstotbnd2  37753  prdsbnd  37772  prdstotbnd  37773  prdsbnd2  37774  cntotbnd  37775  ismtyhmeolem  37783  ismtybndlem  37785  heibor1lem  37788  heiborlem3  37792  heiborlem6  37795  heibor  37800  bfplem1  37801  bfplem2  37802  elghomlem1OLD  37864  rngogrphom  37950  prnc  38046  ispridlc  38049  pridlc3  38052  mpobi123f  38141  mptbi12f  38145  antisymressn  38420  eqvreltr  38583  ax12indalem  38923  lsateln0  38973  atlatmstc  39297  hlatjidm  39347  llnneat  39493  lplnneat  39524  lplnnelln  39525  lvolneatN  39567  lvolnelln  39568  lvolnelpln  39569  dalem23  39675  snatpsubN  39729  linepsubN  39731  pmapsub  39747  pmapglbx  39748  paddasslem14  39812  polsubN  39886  pol1N  39889  2polvalN  39893  2polssN  39894  3polN  39895  2pmaplubN  39905  polatN  39910  2polatN  39911  pnonsingN  39912  polsubclN  39931  lautco  40076  cdlemefrs29cpre1  40377  dian0  41018  dia0eldmN  41019  dia1eldmN  41020  dia0  41031  dia1N  41032  dvhopaddN  41093  dib0  41143  dih0  41259  dih1  41265  dihglblem5apreN  41270  dihatexv2  41318  dochfN  41335  lcmineqlem1  42002  lcmineqlem17  42018  xppss12  42202  sumcubes  42286  dvdsexpnn  42306  remul01  42380  resubeqsub  42403  ricdrng1  42501  prjspeclsp  42585  ismrcd2  42672  nacsfix  42685  mzpaddmpt  42714  mzpmulmpt  42715  eq0rabdioph  42749  lerabdioph  42778  ltrabdioph  42781  nerabdioph  42782  dvdsrabdioph  42783  fiphp3d  42792  congneg  42942  jm2.22  42968  jm2.23  42969  jm2.15nn0  42976  jm3.1  42993  aomclem8  43034  lsmfgcl  43047  lmhmfgima  43057  lnmepi  43058  dgrsub2  43108  mpaaeu  43123  mendring  43161  proot1ex  43169  unielss  43191  onsucwordi  43261  oaabsb  43267  rp-oelim2  43281  nnoeomeqom  43285  cantnfresb  43297  oawordex2  43299  omcl3g  43307  ordsssucb  43308  tfsconcatrev  43321  onsucunipr  43345  onsucunitp  43346  oaun3lem1  43347  naddgeoa  43367  oaltom  43378  minregex2  43508  sssymdifcl  43545  relexp01min  43686  ntrclsiso  44040  ntrclsk3  44043  cvgdvgrat  44286  nznngen  44289  uzmptshftfval  44319  addrval  44439  subrval  44440  mulvval  44441  elpwgded  44538  eel2131  44687  eel3132  44688  el12  44699  sspwimp  44891  sspwimpcf  44893  suctrALTcf  44895  suctrALT3  44897  relpfrlem  44927  cnfex  45006  disjinfi  45170  infxrbnd2  45349  supminfxr  45444  climinf  45588  lptre2pt  45622  limcresiooub  45624  limcresioolb  45625  addlimc  45630  limclner  45633  limsuppnflem  45692  limsupmnfuzlem  45708  limsupvaluz2  45720  limsupresxr  45748  liminfresxr  45749  cnrefiisplem  45811  cncfdmsn  45872  iblspltprt  45955  itgspltprt  45961  dirkertrigeqlem3  46082  fourierdlem62  46150  fourierdlem80  46168  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem114  46202  sge0f1o  46364  hoidmvlelem2  46578  pimdecfgtioo  46699  smfliminflem  46812  fnresfnco  47026  fcores  47052  dfatcolem  47240  nn0resubcl  47293  zgeltp1eq  47294  eluzge0nn0  47297  fz0addcom  47302  elfzlble  47305  fzopredsuc  47308  subsubelfzo0  47311  ceilbi  47318  minusmod5ne  47334  submodlt  47335  mod0mul  47341  m1modmmod  47343  uniimafveqt  47366  fundcmpsurinjimaid  47396  icceuelpartlem  47420  iccpartnel  47423  elsprel  47460  fmtnodvds  47529  goldbachth  47532  fmtnoprmfac2  47552  prmdvdsfmtnof1  47572  2pwp1prm  47574  flsqrt  47578  lighneallem4  47595  dfodd6  47622  divgcdoddALTV  47667  opoeALTV  47668  opeoALTV  47669  omoeALTV  47670  omeoALTV  47671  epoo  47688  emoo  47689  epee  47690  emee  47691  evensumeven  47692  even3prm2  47704  mogoldbblem  47705  fpprmod  47712  dfwppr  47723  fpprwppr  47724  fpprwpprb  47725  gbepos  47743  gbegt5  47746  gbowgt5  47747  gboge9  47749  sbgoldbst  47763  nnsum3primesgbe  47777  bgoldbtbndlem1  47790  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  grimco  47873  isuspgrim0  47878  isuspgrimlem  47879  uhgrimisgrgriclem  47914  uhgrimisgrgric  47915  clnbgrgrim  47918  grimedg  47919  isgrtri  47926  cycl3grtri  47930  isubgr3stgrlem6  47954  isubgr3stgrlem7  47955  isubgr3stgrlem8  47956  uspgrlimlem2  47972  uspgrlimlem3  47973  uspgrlimlem4  47974  grlictr  47991  gpgusgralem  48031  gpgedg2ov  48041  gpgnbgrvtx0  48049  gpgnbgrvtx1  48050  gpg5nbgrvtx03star  48055  gpg5nbgr3star  48056  gpg5grlic  48068  2zrngmmgm  48224  2zrngnmrid  48228  2zrngnmlid2  48229  altgsumbc  48324  altgsumbcALT  48325  zlmodzxzadd  48330  zlmodzxzsub  48332  invginvrid  48339  ply1mulgsumlem2  48360  ply1mulgsum  48363  lincvalpr  48391  lindslinindimp2lem1  48431  ldepsprlem  48445  ldepspr  48446  lincresunit3lem3  48447  lincresunitlem1  48448  lincresunit3lem1  48452  lincresunit3  48454  elfzolborelfzop1  48492  zgtp1leeq  48494  flsubz  48495  nneom  48500  nn0ofldiv2  48505  rege1logbrege0  48531  nnpw2pb  48560  dignn0fr  48574  dignn0ldlem  48575  dignnld  48576  dignn0flhalflem1  48588  nn0sumshdiglemB  48593  nn0mulfsum  48597  rrx2plordisom  48696  ehl2eudis0lt  48699  itsclinecirc0in  48748  2itscp  48754  inlinecirc02plem  48759  mof0ALT  48812  i0oii  48892  resccat  49047