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  2379  nfeqf  2385  eqeqan12dALT  2755  sylan9eq  2791  sylan9ss  3947  ssconb  4094  ineqan12d  4174  ifpr  4650  disjtp2  4673  dfopg  4827  disjxiun  5095  breqan12d  5114  eusv1  5336  opelvvg  5665  opthprc  5688  relop  5799  dmpropg  6173  unixp  6240  tz7.7  6343  ordin  6347  onin  6348  ontri1  6351  onfr  6356  onelpss  6357  onsseleq  6358  oneltri  6360  ontr2  6365  onunel  6424  onun2  6427  funssres  6536  funtpg  6547  funtp  6549  resasplit  6704  fodmrnu  6754  f1un  6794  dffv2  6929  fvreseq0  6983  fvcofneq  7038  funopdmsn  7095  fprg  7100  fprb  7140  fconst2g  7149  isofrlem  7286  oveqan12d  7377  ov3  7521  ovg  7523  ovima0  7537  f1opw2  7613  off  7640  unexgOLD  7694  pwuncl  7715  epweon  7720  epweonALT  7721  sucexeloni  7754  ordunpr  7768  omun  7830  peano4  7834  fabexg  7880  f1oabexg  7884  fiun  7887  offres  7927  el2mpocsbcl  8027  curry1  8046  curry1val  8047  curry2  8049  curry2val  8051  soxp  8071  wexp  8072  xpord2pred  8087  poxp3  8092  poseq  8100  soseq  8101  suppfnss  8131  frrlem4  8231  frrlem11  8238  frrlem12  8239  fprlem1  8242  iunon  8271  onfununi  8273  tfrlem11  8319  tz7.48lem  8372  seqomeq12  8385  oacan  8475  oawordri  8477  oaass  8488  omord2  8494  omcan  8496  oen0  8514  oeordi  8515  oeord  8516  oecan  8517  oeworde  8521  oeordsuc  8522  oelimcl  8528  nnawordi  8549  nnaword  8555  nnmord  8560  oaabslem  8575  omabslem  8578  omsmo  8586  eldifsucnn  8592  naddcllem  8604  naddov2  8607  ertr  8650  erex  8659  brecop  8747  ecopovtrn  8757  ecovdi  8762  mapvalg  8773  pmvalg  8774  pmss12g  8807  elmapresaun  8818  boxcutc  8879  undom  8993  sbthlem7  9021  sbth  9025  sdomnsym  9030  sdomdomtr  9038  xpf1o  9067  xpen  9068  limenpsi  9080  pssnn  9093  pwssfi  9101  sbthfi  9123  php2  9132  php3  9133  phpeqd  9136  nndomog  9137  onomeneq  9138  isinf  9165  fineqvlem  9166  f1finf1o  9173  dif1ennnALT  9177  findcard3  9183  unblem2  9193  isfinite2  9198  unfilem1  9205  unfi2  9210  fodomfir  9228  unifi2  9245  f1opwfi  9256  fsuppxpfi  9288  fsuppunbi  9292  fsuppco2  9306  fsuppcor  9307  fival  9315  fiin  9325  ordiso  9421  ordtypelem10  9432  hartogslem1  9447  wofib  9450  brwdom3  9487  unwdomg  9489  xpwdomg  9490  sucprcreg  9509  preleqALT  9526  inf3lem6  9542  oemapval  9592  cantnf  9602  wemapwe  9606  cnfcom  9609  ttrcltr  9625  dfttrcl2  9633  frmin  9661  r111  9687  r1ord3g  9691  prwf  9723  r1pw  9757  rankprb  9763  rankxplim  9791  tcrank  9796  updjud  9846  finnum  9860  xpnum  9863  carduni  9893  nnsdomel  9902  fidomtri  9905  infxpenlem  9923  fseqdom  9936  onssnum  9950  acndom2  9964  alephinit  10005  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem6  10066  undjudom  10078  endjudisj  10079  djuen  10080  djucomen  10088  pwdjuen  10092  djudom1  10093  djuxpdom  10096  djufi  10097  cardadju  10105  nnadju  10108  nnadjuALT  10109  ficardadju  10110  ficardun  10111  ficardun2  10112  pwsdompw  10113  unctb  10114  ackbij2lem1  10128  ackbij1lem6  10134  ackbij1lem16  10144  ackbij1b  10148  ackbij2  10152  coflim  10171  cflim2  10173  cofsmo  10179  coftr  10183  sornom  10187  infpssrlem5  10217  fin4en1  10219  fin23lem23  10236  fin23lem28  10250  isf32lem2  10264  isf32lem4  10266  isf32lem7  10269  isf34lem7  10289  isf34lem6  10290  fin67  10305  isfin7-2  10306  fin1a2lem9  10318  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  zorn2lem6  10411  ttukeylem3  10421  brdom6disj  10442  carddom  10464  cardsdom  10465  domtri  10466  konigthlem  10479  iunctb  10485  alephadd  10488  alephmul  10489  pwcfsdom  10494  cfpwsdom  10495  fpwwe2lem12  10553  canthp1lem2  10564  pwfseqlem3  10571  pwfseqlem4a  10572  inar1  10686  tskcard  10692  tskuni  10694  grur1  10731  mulclpi  10804  addcompi  10805  mulcompi  10807  distrpi  10809  ltexpi  10813  ltapi  10814  ltmpi  10815  enqbreq2  10831  nqereu  10840  addpipq  10848  addpqnq  10849  mulpipq  10851  mulpqnq  10852  addpqf  10855  addclnq  10856  mulpqf  10857  mulclnq  10858  adderpq  10867  mulerpq  10868  ltsonq  10880  lterpq  10881  ltbtwnnq  10889  ltrnq  10890  genpv  10910  genpdm  10913  genpnnp  10916  mulclprlem  10930  distrlem1pr  10936  distrlem4pr  10937  prlem934  10944  addcanpr  10957  suplem1pr  10963  mulcmpblnr  10982  mulclsr  10995  mulasssr  11001  distrsr  11002  ltsosr  11005  1idsr  11009  00sr  11010  recexsrlem  11014  mulgt0sr  11016  addcnsr  11046  axmulf  11057  axmulass  11068  axdistr  11069  axcnre  11075  mulrid  11130  axltadd  11206  lenlt  11211  dedekind  11296  dedekindle  11297  resubcl  11445  subeqrev  11559  muladd  11569  mulsub  11580  mulsub2  11581  ltaddsub2  11612  leaddsub2  11614  leltadd  11621  ltaddpos2  11628  posdif  11630  addge02  11648  mullt0  11656  ltord1  11663  leord1  11664  eqord1  11665  recextlem1  11767  recex  11769  divmuldiv  11841  conjmul  11858  div2sub  11966  prodgt02  11989  lemul2  11994  lemul2a  11996  ltmulgt12  12002  lemulge12  12005  mulge0b  12012  mulle0b  12013  ltmuldiv2  12016  ltdivmul2  12019  lt2mul2div  12020  ledivmul2  12021  lemuldiv2  12023  ledivdiv  12031  lediv2  12032  ltdiv23  12033  lediv23  12034  supmul  12114  riotaneg  12121  negiso  12122  cju  12141  nnaddcl  12168  nnmulcl  12169  nnmtmip  12171  nnsub  12189  addltmul  12377  avgle1  12381  avgle2  12382  avgle  12383  nnrecl  12399  nn0nnaddcl  12432  nn0sub  12451  elz2  12506  zaddcl  12531  zsubcl  12533  znnsub  12537  znn0sub  12538  nzadd  12539  zmulcl  12540  zltp1le  12541  zleltp1  12542  nnleltp1  12547  nnltp1le  12548  nnaddm1cl  12549  nn0ltp1le  12550  nn0leltp1  12551  nn0ltlem1  12552  nn0lem1lt  12557  nnlem1lt  12558  nnltlem1  12559  zdiv  12562  zextle  12565  zextlt  12566  btwnnz  12568  prime  12573  nneo  12576  peano2uz2  12580  uzind  12584  fzind  12590  zriotaneg  12605  uzneg  12771  uztric  12775  uz11  12776  eluzp1m1  12777  eluzp1p1  12779  uzin  12787  uzwo  12824  indstr  12829  uz2mulcl  12839  supminf  12848  uzsupss  12853  zmax  12858  rebtwnz  12860  qre  12866  qaddcl  12878  qsubcl  12881  irradd  12886  elpqb  12889  rpnnen1lem5  12894  cnref1o  12898  rpaddcl  12929  rpmulcl  12930  rpmtmip  12931  rpdivcl  12932  max1  13100  max2  13102  min1  13104  min2  13105  z2ge  13113  qbtwnxr  13115  xaddf  13139  rexadd  13147  rexsub  13148  xnn0xaddcl  13150  xaddcom  13155  xnn0xadd0  13162  xnegdi  13163  rexmul  13186  supxrbnd2  13237  ixxin  13278  elicc2  13327  difreicc  13400  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  fzval2  13426  elfz1eq  13451  peano2fzr  13453  fzn  13456  fzsplit2  13465  fzaddel  13474  fzadd2  13475  fzsubel  13476  fzrev2  13504  fzrev3  13506  uzsplit  13512  fznuz  13525  uznfz  13526  fzrevral  13528  fzrevral3  13530  fzshftral  13531  elfz2nn0  13534  fznn0sub2  13551  fz0fzdiffz0  13553  elfzmlbp  13555  difelfzle  13557  difelfznle  13558  elfzouz2  13590  fzo0n  13597  fzouzsplit  13610  fzoun  13612  elfzo0le  13619  fzonmapblen  13624  fzofzim  13625  fzoaddel2  13636  eluzgtdifelfzo  13643  elfzodifsumelfzo  13647  ssfzoulel  13676  ubmelm1fzo  13679  fzofzp1b  13681  elfzonelfzo  13685  elfznelfzo  13689  fzostep1  13702  injresinjlem  13706  subfzo0  13708  flflp1  13727  divfl0  13744  flzadd  13746  flmulnn0  13747  fldivnn0le  13752  fldiv  13780  uzsup  13783  mulmod0  13797  modlt  13800  modmulnn  13809  zmodcl  13811  zmodfz  13813  zmodid2  13819  modcyc  13826  muladdmodid  13833  modmuladdnn0  13838  negmod  13839  addmodidr  13843  modadd2mod  13844  modaddmodup  13857  modaddmulmod  13861  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  om2uzlti  13873  om2uzf1oi  13876  fzen2  13892  ssnn0fi  13908  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub0  13916  seqshft2  13951  seqsplit  13958  seqcaopr2  13961  seqf1olem2  13965  expcllem  13995  expcl2lem  13996  1exp  14014  expge1  14022  expadd  14027  expmul  14030  expsub  14033  nn0sq11  14055  lt2sq  14056  le2sq  14057  expmordi  14090  leexp2  14094  leexp1a  14098  sumsqeq0  14102  bernneq  14152  bernneq2  14153  expnbnd  14155  digit2  14159  digit1  14160  facdiv  14210  facwordi  14212  faclbnd  14213  faclbnd3  14215  faclbnd4lem4  14219  faclbnd5  14221  faclbnd6  14222  facavg  14224  bcrpcl  14231  bccmpl  14232  bcval5  14241  hashen  14270  hasheqf1oi  14274  hashgadd  14300  hashdom  14302  hashsdom  14304  hashun  14305  hashunsnggt  14317  hashprg  14318  hashssdif  14335  hashxplem  14356  seqcoll  14387  tpf1o  14424  eqwrd  14480  ccatfval  14496  ccatlen  14498  ccat0  14499  elfzelfzccat  14503  ccatsymb  14506  ccatval21sw  14509  ccatrn  14513  lswccatn0lsw  14515  ccatalpha  14517  ccatrcl1  14518  ccats1alpha  14543  swrdnd  14578  swrdfv2  14585  swrdsbslen  14588  swrdspsleq  14589  swrdccat2  14593  pfxnd0  14612  pfxeq  14619  ccatpfx  14624  pfxccat1  14625  swrdswrdlem  14627  pfxswrd  14629  pfxccatin12lem4  14649  pfxccatin12lem1  14651  pfxccatin12lem2  14654  pfxccatin12lem3  14655  pfxccatin12  14656  pfxccat3  14657  swrdccat  14658  pfxccatpfx2  14660  pfxccat3a  14661  swrdccat3blem  14662  swrdccat3b  14663  revccat  14689  revrev  14690  cshwlen  14722  cshwidxmod  14726  cshwidxmodr  14727  cshweqdif2  14742  cshweqrep  14744  2cshwcshw  14748  s3eq3seq  14862  cotr2g  14899  trclun  14937  shftf  15002  seqshft  15008  crre  15037  crim  15038  readd  15049  resub  15050  remul2  15053  imadd  15057  imsub  15058  immul2  15060  ipcnval  15066  cjsub  15072  cjreim  15083  01sqrexlem6  15170  sqrtle  15183  sqrt11  15185  absreimsq  15215  absreim  15216  absmul  15217  sqabs  15230  absdiflt  15241  absdifle  15242  abssuble0  15252  absmax  15253  abs2difabs  15258  fzomaxdif  15267  rexanuz  15269  rexuz3  15272  rexuzre  15276  caubnd2  15281  limsupgre  15404  limsupbnd2  15406  climconst2  15471  lo1resb  15487  o1resb  15489  2clim  15495  climshftlem  15497  climshft  15499  climshft2  15505  cjcn2  15523  o1of2  15536  o1rlimmul  15542  climaddc1  15558  climmulc2  15560  climsubc1  15561  climsubc2  15562  lo1le  15575  climlec2  15582  isershft  15587  isercolllem1  15588  isercolllem3  15590  isercoll  15591  isercoll2  15592  climsup  15593  caurcvg  15600  caucvg  15602  iseraltlem1  15605  iseraltlem2  15606  iseralt  15608  summolem2a  15638  isumclim3  15682  mptfzshft  15701  fsumrev  15702  fsum0diag2  15706  fsumconst  15713  telfsumo2  15726  fsumparts  15729  o1fsum  15736  cvgcmp  15739  cvgcmpub  15740  cvgcmpce  15741  binomlem  15752  binom1p  15754  binom1dif  15756  bcxmas  15758  incexclem  15759  incexc  15760  incexc2  15761  isumshft  15762  isumsplit  15763  isumsup2  15769  climcndslem1  15772  climcndslem2  15773  climcnds  15774  supcvg  15779  expcnv  15787  geoserg  15789  pwdif  15791  geolim  15793  geoisum1  15802  geoisum1c  15803  cvgrat  15806  mertenslem1  15807  mertenslem2  15808  mertens  15809  ntrivcvgfvn0  15822  ntrivcvgmullem  15824  prodmolem2a  15857  prodmo  15859  fprodf1o  15869  fproddiv  15884  fprodeq0  15898  risefacval2  15933  fallfacval2  15934  fallfacval3  15935  rprisefaccl  15946  risefallfac  15947  fallfacfwd  15959  binomfallfaclem1  15962  binomfallfaclem2  15963  binomrisefac  15965  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  efcj  16015  fprodefsum  16018  efexp  16026  eftlub  16034  effsumlt  16036  efle  16043  reef11  16044  efieq  16088  sinsub  16093  cossub  16094  subsin  16096  sinmul  16097  cosmul  16098  addcos  16099  subcos  16100  rpnnen2lem10  16148  rpnnen2lem12  16150  ruclem8  16162  ruclem12  16166  sqrt2irr  16174  dvdssub2  16228  dvdsadd  16229  dvdsaddr  16230  dvdssub  16231  dvdssubr  16232  dvdsle  16237  alzdvds  16247  fzocongeq  16251  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  pwp1fsum  16318  divalglem4  16323  divalglem9  16328  divalgb  16331  divalgmod  16333  ndvdsadd  16337  smueqlem  16417  gcdaddm  16452  modgcd  16459  bezoutlem1  16466  dvdsgcd  16471  absmulgcd  16476  rpmulgcd  16484  rprpwr  16486  sqgcd  16489  dvdssqlem  16493  dvdssq  16494  nn0seqcvgd  16497  algrf  16500  algcvg  16503  lcmcllem  16523  lcmabs  16532  lcmgcd  16534  lcmdvds  16535  lcmgcdnn  16538  lcmf  16560  coprmgcdb  16576  coprmdvds  16580  coprmdvds2  16581  qredeq  16584  isprm3  16610  nprm  16615  oddprmgt2  16626  isprm5  16634  isprm7  16635  divgcdodd  16637  prmdvdsexp  16642  zgcdsq  16680  hashdvds  16702  phiprmpw  16703  crth  16705  phimullem  16706  modprm0  16733  coprimeprodsq  16736  coprimeprodsq2  16737  pythagtriplem2  16745  pythagtriplem19  16761  iserodd  16763  pcpremul  16771  pcmul  16779  pcexp  16787  pcdvdsb  16797  pcneg  16802  pc2dvds  16807  pc11  16808  pcmpt  16820  fldivp1  16825  pcfac  16827  infpnlem1  16838  prmunb  16842  prmreclem1  16844  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  1arithlem4  16854  1arith  16855  gzaddcl  16865  gzmulcl  16866  gzreim  16867  gzsubcl  16868  4sqlem1  16876  4sqlem4a  16879  4sqlem4  16880  4sqlem12  16884  ramlb  16947  prmgaplem4  16982  prmgaplem5  16983  prmgaplem6  16984  prmgaplem7  16985  prmgaplem8  16986  prmgapprmolem  16989  cshwshashlem2  17024  setsvalg  17093  ressval  17160  ressval3d  17173  restval  17346  pwsval  17406  xpsval  17491  ssclem  17743  rescval  17751  funcestrcsetclem9  18071  embedsetcestrclem  18080  lubel  18437  ipodrsima  18464  tsrss  18512  chnrdss  18540  resmgmhm  18636  resmgmhm2  18637  mgmhmco  18639  submnd0  18688  mndinvmod  18689  xpsmnd0  18703  resmhm  18745  resmhm2  18746  mhmco  18748  frmdplusg  18779  frmdmnd  18784  efmndcl  18807  smndex1id  18836  mgm2nsgrplem1  18843  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  sgrp2nmndlem1  18848  sgrp2rid2  18851  dfgrp3  18969  mhmmnd  18994  mulgnngsum  19009  mulgnnsubcl  19016  mulgnn0z  19031  mulgnndir  19033  mulgmodid  19043  eqgfval  19105  cycsubgcl  19135  cycsubg2  19139  0ghm  19159  resghm  19161  resghm2  19162  ghmco  19165  ghmeql  19168  isgim  19191  gicsubgen  19208  cntzmhm  19270  symgcl  19314  symgextf1  19350  gsmsymgrfixlem1  19356  symgfixf1  19366  symgtrinv  19401  pmtrdifellem3  19407  mndodcongi  19472  odmod  19475  odf1  19491  odf1o1  19501  gexdvds  19513  sylow1lem1  19527  pgpssslw  19543  lsmub1  19586  lsmub2  19587  cntzrecd  19607  pj1ghm  19632  lsmhash  19634  efgred  19677  frgpup1  19704  ablsubadd23  19742  ablsubsub23  19753  mulgnn0di  19754  torsubg  19783  zaddablx  19801  gsumzaddlem  19850  gsumzadd  19851  gsumconst  19863  gsumzmhm  19866  telgsumfzslem  19917  dprdfadd  19951  dprd2dlem1  19972  ablsimpgfindlem1  20038  srgbinomlem3  20163  srgbinomlem4  20164  srgbinomlem  20165  gsummgp0  20253  gsumdixp  20254  xpsring1d  20269  unitnegcl  20333  isrnghm  20377  rnghmco  20393  dfrhm2  20410  rhmco  20434  c0rhm  20467  c0rnghm  20468  rhmimasubrng  20499  cntzsubrng  20500  issubrg3  20533  resrhm  20534  rhmeql  20536  rhmima  20537  isdomn4  20649  imadrhmcl  20730  fldsdrgfld  20731  abvres  20764  suborng  20809  lmodfopne  20851  lspf  20925  lspcl  20927  0lmhm  20992  lmhmco  20995  lmhmeql  21007  islmim  21014  rngqiprngghm  21254  rngqiprnglin  21257  xrsdsreval  21366  xrsdsreclb  21368  xrs1cmn  21397  xrge0omnd  21400  znfld  21515  znchr  21517  znunithash  21519  znrrg  21520  freshmansdream  21529  cnmsgnsubg  21532  zrhpsgnmhm  21539  evpmodpmf1o  21551  psgndiflemB  21555  psgndif  21557  phlssphl  21614  frlmval  21703  uvcfval  21739  frlmsslsp  21751  frlmup2  21754  lindfmm  21782  lmimlbs  21791  islindf4  21793  issubassa3  21821  psrbaglesupp  21878  psrcom  21923  resspsrmul  21931  mplsubrglem  21959  mplcoe3  21993  ltbval  21998  ltbwe  21999  evlslem4  22031  evlslem3  22035  psdmvr  22112  psropprmul  22178  coe1tmmul  22219  cply1mul  22240  gsummoncoe1  22252  lply1binomsc  22255  pf1ind  22299  mamufacex  22340  grpvlinv  22342  grpvrinv  22343  eqmat  22368  mat1dimcrng  22421  dmatcrng  22446  scmatf1  22475  m1detdiag  22541  mdetdiaglem  22542  mdet1  22545  mdetunilem9  22564  madulid  22589  gsummatr01lem4  22602  gsummatr01  22603  mat2pmatlin  22679  m2pmfzgsumcl  22692  monmatcollpw  22723  pmatcollpw3lem  22727  mp2pm2mplem4  22753  chpscmatgsummon  22789  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  cayhamlem1  22810  cpmadugsumlemF  22820  clsval2  22994  innei  23069  ordtrest  23146  ordtrestixx  23166  isnrm2  23302  lpcls  23308  tgcmp  23345  cmpcld  23346  uncmp  23347  hauscmplem  23350  hauscmp  23351  1stcfb  23389  1stcrest  23397  kgencmp2  23490  1stckgenlem  23497  kgen2ss  23499  kgencn  23500  kgencn3  23502  txval  23508  txuni2  23509  txbasex  23510  txbas  23511  txtop  23513  ptbasin  23521  txtopon  23535  txcld  23547  txss12  23549  txbasval  23550  xkoccn  23563  txcnp  23564  ptcnplem  23565  upxp  23567  txcnmpt  23568  uptx  23569  txrest  23575  txdis  23576  txindislem  23577  txlly  23580  txnlly  23581  txcmp  23587  hausdiag  23589  txhaus  23591  tx1stc  23594  tx2ndc  23595  txkgen  23596  xkoptsub  23598  cnmpt21  23615  txconn  23633  qtopval  23639  hmeoco  23716  txhmeo  23747  xpstopnlem1  23753  fbun  23784  filss  23797  infil  23807  fbunfip  23813  filuni  23829  fmfnfmlem4  23901  ufldom  23906  flffval  23933  flfval  23934  txflf  23950  fcfval  23977  alexsubALTlem3  23993  tgpmulg  24037  subgtgp  24049  qustgplem  24065  tsmsfbas  24072  tsmsres  24088  tsmsmhm  24090  tsmsadd  24091  isxmet2d  24271  blin2  24373  comet  24457  met2ndci  24466  metcn  24487  txmetcn  24492  dscopn  24517  nrmmetd  24518  isngp3  24542  tngval  24583  nm1  24611  subrgnrg  24617  nrginvrcn  24636  rlmnvc  24647  nmo0  24679  nmoco  24681  nghmco  24682  nmotri  24683  0nghm  24685  isnmhm2  24696  0nmhm  24699  nmhmco  24700  nmhmplusg  24701  qtopbaslem  24702  remetdval  24733  bl2ioo  24736  reperflem  24763  iccntr  24766  icccmplem2  24768  icccmp  24770  reconnlem2  24772  xrge0gsumle  24778  xrge0tsms  24779  divcnOLD  24813  divcn  24815  cncfmet  24858  iccpnfcnv  24898  bndth  24913  copco  24974  pcopt  24978  pcopt2  24979  nmhmcn  25076  cmodscexp  25077  cphassr  25168  lmmbrf  25218  lmnn  25219  iscauf  25236  caucfil  25239  iscmet3lem1  25247  iscmet3lem2  25248  iscmet3  25249  cfilres  25252  caussi  25253  caubl  25264  caublcls  25265  bcthlem2  25281  bcthlem5  25284  cmsss  25307  lssbn  25308  ovolfioo  25424  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliunlem2  25460  ovoliunlem3  25461  ovoliun2  25463  ovolscalem1  25470  ovolicc2lem1  25474  ovolicc2lem4  25477  ovolicc2lem5  25478  inmbl  25499  voliunlem1  25507  volsup  25513  ioombl1lem4  25518  iccvolcl  25524  ioovolcl  25527  uniioovol  25536  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  dyadf  25548  dyadovol  25550  dyadss  25551  dyadmbl  25557  opnmbllem  25558  volsup2  25562  volcn  25563  ismbf  25585  mbfima  25587  ismbf3d  25611  mbfadd  25618  mbfsub  25619  mbflimsup  25623  itg1mulc  25661  itg1sub  25666  itg1climres  25671  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfmul  25683  itg2const2  25698  itg2seq  25699  itg2uba  25700  itg2lea  25701  itg2eqa  25702  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  itg2cnlem1  25718  bddmulibl  25796  ellimc3  25836  dvaddbr  25896  dvcobr  25905  dvcobrOLD  25906  dvcjbr  25909  dvcnvlem  25936  c1lip1  25958  lhop  25977  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumrlimf  25987  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  tdeglem4  26021  deg1ge  26059  coe1mul3  26060  fta1g  26131  plyco0  26153  plyf  26159  ply1termlem  26164  plyeq0lem  26171  plypf1  26173  plymullem1  26175  plyaddlem  26176  plymullem  26177  coeeulem  26185  coeidlem  26198  plyco  26202  dgreq  26205  coefv0  26209  coeaddlem  26210  coemullem  26211  coemulhi  26215  coemulc  26216  plycn  26222  plycnOLD  26223  dgrlt  26228  dgrsub  26234  plycjlem  26238  plycj  26239  plycjOLD  26241  plyrecj  26243  plymul0or  26244  plyreres  26246  dvply1  26247  vieta1lem2  26275  plyexmo  26277  elqaalem2  26284  elqaalem3  26285  aareccl  26290  aalioulem1  26296  aalioulem3  26298  aaliou  26302  geolim3  26303  ulmcaulem  26359  ulmcau  26360  mtest  26369  dvradcnv  26386  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv2  26396  abelthlem6  26402  abelthlem8  26405  abelthlem9  26406  reeff1o  26413  reefgim  26416  sinperlem  26445  sincosq2sgn  26464  sincosq3sgn  26465  sinq12ge0  26473  sincos6thpi  26481  sineq0  26489  cosord  26496  cos11  26498  sinord  26499  tanord1  26502  eff1olem  26513  logrnaddcl  26539  relogeftb  26549  relogoprlem  26556  logleb  26568  advlogexp  26620  logtayllem  26624  logtayl  26625  logtaylsum  26626  logtayl2  26627  recxpcl  26640  rpcxpcl  26641  cxple3  26666  cxpcom  26704  cxpcn3  26714  cxpeq  26723  relogbmul  26743  relogbcxp  26751  relogbf  26757  atanord  26893  atantayl  26903  birthdaylem2  26918  birthdaylem3  26919  cxp2limlem  26942  fsumharmonic  26978  zetacvg  26981  ftalem1  27039  ftalem4  27042  ftalem5  27043  basellem2  27048  basellem3  27049  basellem4  27050  vmappw  27082  sqf11  27105  mumul  27147  fsumdvdscom  27151  dvdsppwf1o  27152  dvdsflf1o  27153  musum  27157  muinv  27159  fsumdvdsmul  27161  1sgmprm  27166  vmalelog  27172  chtublem  27178  fsumvma  27180  vmasum  27183  logfac2  27184  chpval2  27185  logfaclbnd  27189  logexprlim  27192  mersenne  27194  dchrmulcl  27216  dchrinvcl  27220  dchrfi  27222  dchrghm  27223  dchrptlem1  27231  dchrsum2  27235  dchrsum  27236  pcbcctr  27243  bcmono  27244  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem5  27255  bposlem6  27256  bposlem7  27257  lgslem3  27266  lgscllem  27271  lgsval4a  27286  lgsneg  27288  lgsdir2  27297  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  gausslemma2dlem6  27339  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2  27353  lgsquad3  27354  2lgslem1a1  27356  2lgslem1a  27358  2lgslem1c  27360  2sqlem2  27385  mul2sq  27386  2sqlem7  27391  2sqreultlem  27414  2sqreunnltlem  27417  2sqreunnltblem  27418  chebbnd1lem1  27436  vmadivsum  27449  rplogsumlem2  27452  dchrisum0lem1a  27453  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  dchrisum0ff  27474  dchrisum0flblem1  27475  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  mudivsum  27497  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  selberglem2  27513  selberg2  27518  chpdifbndlem1  27520  selberg3lem1  27524  pntrsumbnd2  27534  selbergr  27535  pntpbnd1  27553  pntpbnd2  27554  pntlemh  27566  pntlemj  27570  pntlemi  27571  pntlemf  27572  pntlemp  27577  ostth2lem1  27585  ostth1  27600  ostth2lem3  27602  ostth3  27605  noreson  27628  nosepon  27633  noextendseq  27635  nosupbnd1lem5  27680  noetasuplem4  27704  addscom  27962  negsdi  28046  onles  28264  addonbday  28275  om2noseqlt  28295  om2noseqf1o  28297  n0s0suc  28338  nnsge1  28339  n0bday  28348  n0fincut  28351  n0ltsp1le  28361  bdayn0sf1o  28366  zaddscl  28390  elzn0s  28394  zsoring  28405  zseo  28418  bdayfinbndlem1  28463  z12subscl  28475  remulscllem2  28497  istrkg2ld  28532  isismt  28606  eedimeq  28971  eqeefv  28976  brbtwn2  28978  colinearalglem1  28979  colinearalglem2  28980  colinearalg  28983  eleesub  28984  eleesubd  28985  axcgrrflx  28987  axcgrid  28989  axsegconlem2  28991  axsegconlem7  28996  axsegconlem9  28998  axsegconlem10  28999  axlowdimlem14  29028  axlowdimlem16  29030  axlowdimlem17  29031  axcontlem2  29038  axcontlem4  29040  axcontlem8  29044  axcontlem10  29046  structiedg0val  29095  upgr1eop  29188  numedglnl  29217  usgredg2v  29300  ushgredgedg  29302  ushgredgedgloop  29304  uspgr1eop  29320  usgr1eop  29323  uhgrissubgr  29348  umgrres1lem  29383  upgrres1  29386  nbuhgr  29416  edgnbusgreu  29440  nb3gr2nb  29457  uvtxnm1nbgr  29477  cusgrexilem2  29515  finsumvtxdg2ssteplem4  29622  vtxdgoddnumeven  29627  wlkeq  29707  uspgr2wlkeq  29719  wlksoneq1eq2  29736  upgrwlkdvdelem  29809  usgr2wlkspthlem1  29830  usgrn2cycl  29882  crctcshwlkn0lem3  29885  crctcshwlkn0lem6  29888  crctcshwlkn0lem7  29889  crctcshwlkn0  29894  wspthneq1eq2  29933  wwlkseq  29964  wwlksnext  29966  rusgrnumwlkg  30053  clwwlkccatlem  30064  clwwlkccat  30065  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  clwlkclwwlkf1lem3  30081  clwwisshclwwslemlem  30088  clwwisshclwws  30090  erclwwlkeqlen  30094  erclwwlkref  30095  clwwnisshclwwsn  30134  clwwlknccat  30138  erclwwlkneqlen  30143  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwlksndivn  30161  uhgr3cyclex  30257  eucrctshift  30318  eucrct2eupth  30320  frgreu  30343  frgr3v  30350  3vfriswmgr  30353  frgrncvvdeqlem3  30376  frgrregorufrg  30401  numclwwlk1lem2f1  30432  numclwwlk1lem2fo  30433  numclwlk1lem2  30445  numclwwlk3  30460  numclwwlk6  30465  frgrreg  30469  frgrregord013  30470  nsnlplig  30556  nsnlpligALT  30557  ablodivdiv4  30629  imsdval  30761  nmcvcn  30770  sspval  30798  lnoadd  30833  lnosub  30834  nmooge0  30842  nmoolb  30846  nmoub3i  30848  blocnilem  30879  blocni  30880  cncph  30894  ipasslem1  30906  ipasslem2  30907  ipasslem4  30909  ipasslem11  30915  ipblnfi  30930  phoeqi  30932  ubthlem1  30945  ubthlem3  30947  htthlem  30992  hvsub4  31112  his7  31165  his2sub2  31168  hial2eq2  31182  hhip  31252  hhph  31253  bcs2  31257  hhssabloi  31337  hhssnv  31339  ocorth  31366  shsel  31389  shsel3  31390  shscli  31392  chsupss  31417  shjval  31426  chjval  31427  shjcl  31431  chjcl  31432  shsleji  31445  chslej  31573  chsscon2  31577  chjcom  31581  chub1  31582  chdmj1  31604  spanunsni  31654  spanpr  31655  fh1  31693  fh2  31694  cm2j  31695  spansncvi  31727  5oalem1  31729  5oalem3  31731  5oalem5  31733  3oalem2  31738  pjcompi  31747  pjds3i  31788  hoeq  31835  hoadddi  31878  hoadddir  31879  hosubdi  31883  hosub4  31888  hoeq1  31905  hoeq2  31906  adjval2  31966  counop  31996  adjeq  32010  brafnmul  32026  lnopsubi  32049  hmops  32095  hmopm  32096  hmopd  32097  hmopco  32098  nmcopexi  32102  lnconi  32108  lnfnsubi  32121  nmcfnexi  32126  imaelshi  32133  nlelshi  32135  riesz3i  32137  riesz1  32140  cnlnadjlem2  32143  cnlnadjlem6  32147  adjbdln  32158  adjlnop  32161  adjmul  32167  adjadd  32168  nmopcoi  32170  rnbra  32182  cnvbramul  32190  kbass2  32192  kbass4  32194  kbass5  32195  kbass6  32196  leopadd  32207  leopmul2i  32210  leoptri  32211  dmdmd  32375  mddmd  32376  cvdmd  32412  superpos  32429  chrelati  32439  atcv0eq  32454  atomli  32457  atcvatlem  32460  atcvati  32461  atcvat2i  32462  chirredlem4  32468  atcvat3i  32471  atcvat4i  32472  mdsymlem2  32479  mdsymlem3  32480  mdsymlem5  32482  mdsymlem8  32485  dmdsym  32488  cdjreui  32507  cdj1i  32508  cdj3lem2b  32512  cdj3lem3  32513  cdj3lem3b  32515  cdj3i  32516  brabgaf  32684  prct  32792  fcobijfs  32800  fzsplit3  32873  bcm1n  32875  dpfrac1  32973  wrdres  33017  xrge0mulgnn0  33097  xrge0tsmsd  33155  cycpmco2  33215  isarchiofld  33281  resvval  33410  nsgqusf1olem2  33495  lbslsat  33773  ply1degltdimlem  33779  ply1degltdim  33780  ordtrestNEW  34078  mhmhmeotmd  34084  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0pluscn  34097  hasheuni  34242  sxval  34347  measvuni  34371  ddemeas  34393  br2base  34426  dya2iocucvr  34441  sxbrsigalem2  34443  sxbrsiga  34447  omssubadd  34457  eulerpartlemgc  34519  ballotlemfc0  34650  ballotlemfcc  34651  signstfvc  34731  signstres  34732  signsvfn  34739  bnj563  34899  bnj554  35055  bnj557  35057  bnj570  35061  bnj594  35068  bnj849  35081  bnj970  35103  bnj1118  35140  bnj1145  35149  bnj1190  35164  bnj1398  35190  bnj1417  35197  r1omfi  35261  zltp1ne  35304  nnltp1ne  35305  nn0ltp1ne  35306  0nn0m1nnn0  35307  cusgr3cyclex  35330  derangsn  35364  derangen  35366  subfacp1lem5  35378  erdsze2lem1  35397  txpconn  35426  txsconn  35435  cvmliftphtlem  35511  satfdm  35563  satfun  35605  ex-sategoelel  35615  mrsubff1  35708  msubff  35724  msubff1  35750  msubvrs  35754  inffz  35924  bcprod  35932  bccolsum  35933  faclim  35940  dfon2lem4  35978  colineardim1  36255  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem12  36292  btwnconn1lem13  36293  btwnconn1lem14  36294  outsideofeu  36325  funray  36334  lineintmo  36351  fwddifnp1  36359  hfun  36372  nn0prpw  36517  opnregcld  36524  cldregopn  36525  ivthALT  36529  onsucconni  36631  bj-nnfim1  36945  bj-nnfim2  36946  bj-2uplex  37223  bj-unexg  37239  bj-prexg  37240  bj-idres  37361  isbasisrelowllem1  37556  isbasisrelowllem2  37557  icoreclin  37558  relowlssretop  37564  exrecfnlem  37580  pibt2  37618  unccur  37800  phpreu  37801  finixpnum  37802  ltflcei  37805  cos2h  37808  lindsadd  37810  lindsdom  37811  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem13  37830  poimirlem14  37831  poimirlem15  37832  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem24  37841  poimirlem26  37843  poimirlem27  37844  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  heicant  37852  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  ovoliunnfl  37859  mbfresfi  37863  itg2addnclem  37868  itg2addnc  37871  itg2gt0cn  37872  ftc1cnnc  37889  ftc1anclem3  37892  ftc1anclem5  37894  ftc1anclem6  37895  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  ftc2nc  37899  indexa  37930  incsequz  37945  incsequz2  37946  geomcau  37956  sstotbnd2  37971  prdsbnd  37990  prdstotbnd  37991  prdsbnd2  37992  cntotbnd  37993  ismtyhmeolem  38001  ismtybndlem  38003  heibor1lem  38006  heiborlem3  38010  heiborlem6  38013  heibor  38018  bfplem1  38019  bfplem2  38020  elghomlem1OLD  38082  rngogrphom  38168  prnc  38264  ispridlc  38267  pridlc3  38270  mpobi123f  38359  mptbi12f  38363  antisymressn  38703  eqvreltr  38860  ax12indalem  39201  lsateln0  39251  atlatmstc  39575  hlatjidm  39625  llnneat  39770  lplnneat  39801  lplnnelln  39802  lvolneatN  39844  lvolnelln  39845  lvolnelpln  39846  dalem23  39952  snatpsubN  40006  linepsubN  40008  pmapsub  40024  pmapglbx  40025  paddasslem14  40089  polsubN  40163  pol1N  40166  2polvalN  40170  2polssN  40171  3polN  40172  2pmaplubN  40182  polatN  40187  2polatN  40188  pnonsingN  40189  polsubclN  40208  lautco  40353  cdlemefrs29cpre1  40654  dian0  41295  dia0eldmN  41296  dia1eldmN  41297  dia0  41308  dia1N  41309  dvhopaddN  41370  dib0  41420  dih0  41536  dih1  41542  dihglblem5apreN  41547  dihatexv2  41595  dochfN  41612  lcmineqlem1  42279  lcmineqlem17  42295  xppss12  42481  sumcubes  42564  dvdsexpnn  42584  remul01  42658  resubeqsub  42681  ricdrng1  42779  prjspeclsp  42851  ismrcd2  42937  nacsfix  42950  mzpaddmpt  42979  mzpmulmpt  42980  eq0rabdioph  43014  lerabdioph  43043  ltrabdioph  43046  nerabdioph  43047  dvdsrabdioph  43048  fiphp3d  43057  congneg  43207  jm2.22  43233  jm2.23  43234  jm2.15nn0  43241  jm3.1  43258  aomclem8  43299  lsmfgcl  43312  lmhmfgima  43322  lnmepi  43323  dgrsub2  43373  mpaaeu  43388  mendring  43426  proot1ex  43434  unielss  43456  onsucwordi  43526  oaabsb  43532  rp-oelim2  43546  nnoeomeqom  43550  cantnfresb  43562  oawordex2  43564  omcl3g  43572  ordsssucb  43573  tfsconcatrev  43586  onsucunipr  43610  onsucunitp  43611  oaun3lem1  43612  naddgeoa  43632  oaltom  43642  minregex2  43772  sssymdifcl  43809  relexp01min  43950  ntrclsiso  44304  ntrclsk3  44307  cvgdvgrat  44550  nznngen  44553  uzmptshftfval  44583  addrval  44702  subrval  44703  mulvval  44704  elpwgded  44801  eel2131  44950  eel3132  44951  el12  44962  sspwimp  45154  sspwimpcf  45156  suctrALTcf  45158  suctrALT3  45160  relpfrlem  45190  cnfex  45269  disjinfi  45432  infxrbnd2  45609  supminfxr  45704  climinf  45848  lptre2pt  45880  limcresiooub  45882  limcresioolb  45883  addlimc  45888  limclner  45891  limsuppnflem  45950  limsupmnfuzlem  45966  limsupvaluz2  45978  limsupresxr  46006  liminfresxr  46007  cnrefiisplem  46069  cncfdmsn  46130  iblspltprt  46213  itgspltprt  46219  dirkertrigeqlem3  46340  fourierdlem62  46408  fourierdlem80  46426  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem114  46460  sge0f1o  46622  hoidmvlelem2  46836  pimdecfgtioo  46957  smfliminflem  47070  fnresfnco  47283  fcores  47309  dfatcolem  47497  nn0resubcl  47550  zgeltp1eq  47551  eluzge0nn0  47554  fz0addcom  47559  elfzlble  47562  fzopredsuc  47565  subsubelfzo0  47568  ceilbi  47575  minusmod5ne  47591  submodlt  47592  mod0mul  47598  m1modmmod  47600  uniimafveqt  47623  fundcmpsurinjimaid  47653  icceuelpartlem  47677  iccpartnel  47680  elsprel  47717  fmtnodvds  47786  goldbachth  47789  fmtnoprmfac2  47809  prmdvdsfmtnof1  47829  2pwp1prm  47831  flsqrt  47835  lighneallem4  47852  dfodd6  47879  divgcdoddALTV  47924  opoeALTV  47925  opeoALTV  47926  omoeALTV  47927  omeoALTV  47928  epoo  47945  emoo  47946  epee  47947  emee  47948  evensumeven  47949  even3prm2  47961  mogoldbblem  47962  fpprmod  47969  dfwppr  47980  fpprwppr  47981  fpprwpprb  47982  gbepos  48000  gbegt5  48003  gbowgt5  48004  gboge9  48006  sbgoldbst  48020  nnsum3primesgbe  48034  bgoldbtbndlem1  48047  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  grimco  48131  isuspgrim0  48136  isuspgrimlem  48137  uhgrimisgrgriclem  48172  uhgrimisgrgric  48173  clnbgrgrim  48176  grimedg  48177  isgrtri  48185  cycl3grtri  48189  isubgr3stgrlem6  48213  isubgr3stgrlem7  48214  isubgr3stgrlem8  48215  uspgrlimlem2  48231  uspgrlimlem3  48232  uspgrlimlem4  48233  grlictr  48257  gpgusgralem  48298  gpgedg2ov  48308  gpgnbgrvtx0  48316  gpgnbgrvtx1  48317  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  gpg5grlic  48336  2zrngmmgm  48494  2zrngnmrid  48498  2zrngnmlid2  48499  altgsumbc  48594  altgsumbcALT  48595  zlmodzxzadd  48600  zlmodzxzsub  48602  invginvrid  48609  ply1mulgsumlem2  48629  ply1mulgsum  48632  lincvalpr  48660  lindslinindimp2lem1  48700  ldepsprlem  48714  ldepspr  48715  lincresunit3lem3  48716  lincresunitlem1  48717  lincresunit3lem1  48721  lincresunit3  48723  elfzolborelfzop1  48761  zgtp1leeq  48763  flsubz  48764  nneom  48769  nn0ofldiv2  48774  rege1logbrege0  48800  nnpw2pb  48829  dignn0fr  48843  dignn0ldlem  48844  dignnld  48845  dignn0flhalflem1  48857  nn0sumshdiglemB  48862  nn0mulfsum  48866  rrx2plordisom  48965  ehl2eudis0lt  48968  itsclinecirc0in  49017  2itscp  49023  inlinecirc02plem  49028  mof0ALT  49081  i0oii  49161  resccat  49315