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  2754  sylan9eq  2790  sylan9ss  3972  ssconb  4117  ineqan12d  4197  ifpr  4669  disjtp2  4692  dfopg  4847  disjxiun  5116  breqan12d  5135  eusv1  5361  opelvvg  5695  opthprc  5718  relop  5830  dmpropg  6204  unixp  6271  tz7.7  6378  ordin  6382  onin  6383  ontri1  6386  onfr  6391  onelpss  6392  onsseleq  6393  oneltri  6395  ontr2  6400  onunel  6458  onun2  6461  funssres  6579  funtpg  6590  funtp  6592  resasplit  6747  fodmrnu  6797  f1un  6837  dffv2  6973  fvreseq0  7027  fvcofneq  7082  funopdmsn  7139  fprg  7144  fprb  7185  fconst2g  7194  isofrlem  7332  oveqan12d  7422  ov3  7568  ovg  7570  ovima0  7584  f1opw2  7660  off  7687  unexgOLD  7741  pwuncl  7762  epweon  7767  epweonALT  7768  sucexeloni  7801  ordunpr  7818  omun  7881  peano4  7886  fabexg  7932  f1oabexg  7936  fiun  7939  offres  7980  el2mpocsbcl  8082  curry1  8101  curry1val  8102  curry2  8104  curry2val  8106  soxp  8126  wexp  8127  xpord2pred  8142  poxp3  8147  poseq  8155  soseq  8156  suppfnss  8186  frrlem4  8286  frrlem11  8293  frrlem12  8294  fprlem1  8297  iunon  8351  onfununi  8353  tfrlem11  8400  tz7.48lem  8453  seqomeq12  8466  oacan  8558  oawordri  8560  oaass  8571  omord2  8577  omcan  8579  oen0  8596  oeordi  8597  oeord  8598  oecan  8599  oeworde  8603  oeordsuc  8604  oelimcl  8610  nnawordi  8631  nnaword  8637  nnmord  8642  oaabslem  8657  omabslem  8660  omsmo  8668  eldifsucnn  8674  naddcllem  8686  naddov2  8689  ertr  8732  erex  8741  brecop  8822  ecopovtrn  8832  ecovdi  8837  mapvalg  8848  pmvalg  8849  pmss12g  8881  elmapresaun  8892  boxcutc  8953  undom  9071  sbthlem7  9101  sbth  9105  sdomnsym  9110  sdomdomtr  9122  xpf1o  9151  xpen  9152  limenpsi  9164  pssnn  9180  pwssfi  9189  sbthfi  9211  php2  9220  php3  9221  phpeqd  9224  nndomog  9225  phpOLD  9229  php3OLD  9231  nndomogOLD  9233  onomeneq  9235  1sdomOLD  9255  ominfOLD  9265  isinf  9266  isinfOLD  9267  fineqvlem  9268  f1finf1o  9275  en1eqsnOLD  9279  dif1ennnALT  9281  findcard3  9288  findcard3OLD  9289  unblem2  9299  isfinite2  9304  unfilem1  9313  unfi2  9318  fodomfir  9338  unifi2  9355  f1opwfi  9366  fsuppxpfi  9395  fsuppunbi  9399  fsuppco2  9413  fsuppcor  9414  fival  9422  fiin  9432  ordiso  9528  ordtypelem10  9539  hartogslem1  9554  wofib  9557  brwdom3  9594  unwdomg  9596  xpwdomg  9597  sucprcreg  9613  preleqALT  9629  inf3lem6  9645  oemapval  9695  cantnf  9705  wemapwe  9709  cnfcom  9712  ttrcltr  9728  dfttrcl2  9736  frmin  9761  r111  9787  r1ord3g  9791  prwf  9823  r1pw  9857  rankprb  9863  rankxplim  9891  tcrank  9896  updjud  9946  finnum  9960  xpnum  9963  carduni  9993  nnsdomel  10002  fidomtri  10005  pr2nelemOLD  10015  infxpenlem  10025  fseqdom  10038  onssnum  10052  acndom2  10066  alephinit  10107  dfac5lem4  10138  dfac5lem4OLD  10140  kmlem6  10168  undjudom  10180  endjudisj  10181  djuen  10182  djucomen  10190  pwdjuen  10194  djudom1  10195  djuxpdom  10198  djufi  10199  cardadju  10207  nnadju  10210  nnadjuALT  10211  ficardadju  10212  ficardun  10213  ficardun2  10214  pwsdompw  10215  unctb  10216  ackbij2lem1  10230  ackbij1lem6  10236  ackbij1lem16  10246  ackbij1b  10250  ackbij2  10254  coflim  10273  cflim2  10275  cofsmo  10281  coftr  10285  sornom  10289  infpssrlem5  10319  fin4en1  10321  fin23lem23  10338  fin23lem28  10352  isf32lem2  10366  isf32lem4  10368  isf32lem7  10371  isf34lem7  10391  isf34lem6  10392  fin67  10407  isfin7-2  10408  fin1a2lem9  10420  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  zorn2lem6  10513  ttukeylem3  10523  brdom6disj  10544  carddom  10566  cardsdom  10567  domtri  10568  konigthlem  10580  iunctb  10586  alephadd  10589  alephmul  10590  pwcfsdom  10595  cfpwsdom  10596  fpwwe2lem12  10654  canthp1lem2  10665  pwfseqlem3  10672  pwfseqlem4a  10673  inar1  10787  tskcard  10793  tskuni  10795  grur1  10832  mulclpi  10905  addcompi  10906  mulcompi  10908  distrpi  10910  ltexpi  10914  ltapi  10915  ltmpi  10916  enqbreq2  10932  nqereu  10941  addpipq  10949  addpqnq  10950  mulpipq  10952  mulpqnq  10953  addpqf  10956  addclnq  10957  mulpqf  10958  mulclnq  10959  adderpq  10968  mulerpq  10969  ltsonq  10981  lterpq  10982  ltbtwnnq  10990  ltrnq  10991  genpv  11011  genpdm  11014  genpnnp  11017  mulclprlem  11031  distrlem1pr  11037  distrlem4pr  11038  prlem934  11045  addcanpr  11058  suplem1pr  11064  mulcmpblnr  11083  mulclsr  11096  mulasssr  11102  distrsr  11103  ltsosr  11106  1idsr  11110  00sr  11111  recexsrlem  11115  mulgt0sr  11117  addcnsr  11147  axmulf  11158  axmulass  11169  axdistr  11170  axcnre  11176  mulrid  11231  axltadd  11306  lenlt  11311  dedekind  11396  dedekindle  11397  resubcl  11545  subeqrev  11657  muladd  11667  mulsub  11678  mulsub2  11679  ltaddsub2  11710  leaddsub2  11712  leltadd  11719  ltaddpos2  11726  posdif  11728  addge02  11746  mullt0  11754  ltord1  11761  leord1  11762  eqord1  11763  recextlem1  11865  recex  11867  divmuldiv  11939  conjmul  11956  div2sub  12064  prodgt02  12087  lemul2  12092  lemul2a  12094  ltmulgt12  12100  lemulge12  12103  mulge0b  12110  mulle0b  12111  ltmuldiv2  12114  ltdivmul2  12117  lt2mul2div  12118  ledivmul2  12119  lemuldiv2  12121  ledivdiv  12129  lediv2  12130  ltdiv23  12131  lediv23  12132  supmul  12212  riotaneg  12219  negiso  12220  cju  12234  nnaddcl  12261  nnmulcl  12262  nnmtmip  12264  nnsub  12282  addltmul  12475  avgle1  12479  avgle2  12480  avgle  12481  nnrecl  12497  nn0nnaddcl  12530  nn0sub  12549  elz2  12604  zaddcl  12630  zsubcl  12632  znnsub  12636  znn0sub  12637  nzadd  12638  zmulcl  12639  zltp1le  12640  zleltp1  12641  nnleltp1  12646  nnltp1le  12647  nnaddm1cl  12648  nn0ltp1le  12649  nn0leltp1  12650  nn0ltlem1  12651  nn0lem1lt  12656  nnlem1lt  12657  nnltlem1  12658  zdiv  12661  zextle  12664  zextlt  12665  btwnnz  12667  prime  12672  nneo  12675  peano2uz2  12679  uzind  12683  fzind  12689  zriotaneg  12704  uzneg  12870  uztric  12874  uz11  12875  eluzp1m1  12876  eluzp1p1  12878  uzin  12890  uzwo  12925  indstr  12930  uz2mulcl  12940  supminf  12949  uzsupss  12954  zmax  12959  rebtwnz  12961  qre  12967  qaddcl  12979  qsubcl  12982  irradd  12987  elpqb  12990  rpnnen1lem5  12995  cnref1o  12999  rpaddcl  13029  rpmulcl  13030  rpmtmip  13031  rpdivcl  13032  max1  13199  max2  13201  min1  13203  min2  13204  z2ge  13212  qbtwnxr  13214  xaddf  13238  rexadd  13246  rexsub  13247  xnn0xaddcl  13249  xaddcom  13254  xnn0xadd0  13261  xnegdi  13262  rexmul  13285  supxrbnd2  13336  ixxin  13377  elicc2  13426  difreicc  13499  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  fzval2  13525  elfz1eq  13550  peano2fzr  13552  fzn  13555  fzsplit2  13564  fzaddel  13573  fzadd2  13574  fzsubel  13575  fzrev2  13603  fzrev3  13605  uzsplit  13611  fznuz  13624  uznfz  13625  fzrevral  13627  fzrevral3  13629  fzshftral  13630  elfz2nn0  13633  fznn0sub2  13650  fz0fzdiffz0  13652  elfzmlbp  13654  difelfzle  13656  difelfznle  13657  elfzouz2  13689  fzo0n  13696  fzouzsplit  13709  fzoun  13711  elfzo0le  13718  fzonmapblen  13723  fzofzim  13724  fzoaddel2  13734  eluzgtdifelfzo  13741  elfzodifsumelfzo  13745  ssfzoulel  13774  ubmelm1fzo  13777  fzofzp1b  13779  elfzonelfzo  13783  elfznelfzo  13786  fzostep1  13797  injresinjlem  13801  subfzo0  13803  flflp1  13822  divfl0  13839  flzadd  13841  flmulnn0  13842  fldivnn0le  13847  fldiv  13875  uzsup  13878  mulmod0  13892  modlt  13895  modmulnn  13904  zmodcl  13906  zmodfz  13908  zmodid2  13914  modcyc  13921  muladdmodid  13926  modmuladdnn0  13931  negmod  13932  addmodidr  13936  modadd2mod  13937  modaddmodup  13950  modaddmulmod  13954  modfzo0difsn  13959  modsumfzodifsn  13960  addmodlteq  13962  om2uzlti  13966  om2uzf1oi  13969  fzen2  13985  ssnn0fi  14001  fsuppmapnn0fiublem  14006  fsuppmapnn0fiub0  14009  seqshft2  14044  seqsplit  14051  seqcaopr2  14054  seqf1olem2  14058  expcllem  14088  expcl2lem  14089  1exp  14107  expge1  14115  expadd  14120  expmul  14123  expsub  14126  nn0sq11  14148  lt2sq  14149  le2sq  14150  expmordi  14183  leexp2  14187  leexp1a  14191  sumsqeq0  14195  bernneq  14245  bernneq2  14246  expnbnd  14248  digit2  14252  digit1  14253  facdiv  14303  facwordi  14305  faclbnd  14306  faclbnd3  14308  faclbnd4lem4  14312  faclbnd5  14314  faclbnd6  14315  facavg  14317  bcrpcl  14324  bccmpl  14325  bcval5  14334  hashen  14363  hasheqf1oi  14367  hashgadd  14393  hashdom  14395  hashsdom  14397  hashun  14398  hashunsnggt  14410  hashprg  14411  hashssdif  14428  hashxplem  14449  seqcoll  14480  tpf1o  14517  eqwrd  14573  ccatfval  14589  ccatlen  14591  ccat0  14592  elfzelfzccat  14596  ccatsymb  14598  ccatval21sw  14601  ccatrn  14605  lswccatn0lsw  14607  ccatalpha  14609  ccatrcl1  14610  ccats1alpha  14635  swrdnd  14670  swrdfv2  14677  swrdsbslen  14680  swrdspsleq  14681  swrdccat2  14685  pfxnd0  14704  addlenrevpfx  14706  pfxeq  14712  ccatpfx  14717  pfxccat1  14718  swrdswrdlem  14720  pfxswrd  14722  pfxccatin12lem4  14742  pfxccatin12lem1  14744  pfxccatin12lem2  14747  pfxccatin12lem3  14748  pfxccatin12  14749  pfxccat3  14750  swrdccat  14751  pfxccatpfx2  14753  pfxccat3a  14754  swrdccat3blem  14755  swrdccat3b  14756  revccat  14782  revrev  14783  cshwlen  14815  cshwidxmod  14819  cshwidxmodr  14820  cshweqdif2  14835  cshweqrep  14837  2cshwcshw  14842  s3eq3seq  14956  cotr2g  14993  trclun  15031  shftf  15096  seqshft  15102  crre  15131  crim  15132  readd  15143  resub  15144  remul2  15147  imadd  15151  imsub  15152  immul2  15154  ipcnval  15160  cjsub  15166  cjreim  15177  01sqrexlem6  15264  sqrtle  15277  sqrt11  15279  absreimsq  15309  absreim  15310  absmul  15311  sqabs  15324  absdiflt  15334  absdifle  15335  abssuble0  15345  absmax  15346  abs2difabs  15351  fzomaxdif  15360  rexanuz  15362  rexuz3  15365  rexuzre  15369  caubnd2  15374  limsupgre  15495  limsupbnd2  15497  climconst2  15562  lo1resb  15578  o1resb  15580  2clim  15586  climshftlem  15588  climshft  15590  climshft2  15596  cjcn2  15614  o1of2  15627  o1rlimmul  15633  climaddc1  15649  climmulc2  15651  climsubc1  15652  climsubc2  15653  lo1le  15666  climlec2  15673  isershft  15678  isercolllem1  15679  isercolllem3  15681  isercoll  15682  isercoll2  15683  climsup  15684  caurcvg  15691  caucvg  15693  iseraltlem1  15696  iseraltlem2  15697  iseralt  15699  summolem2a  15729  isumclim3  15773  mptfzshft  15792  fsumrev  15793  fsum0diag2  15797  fsumconst  15804  telfsumo2  15817  fsumparts  15820  o1fsum  15827  cvgcmp  15830  cvgcmpub  15831  cvgcmpce  15832  binomlem  15843  binom1p  15845  binom1dif  15847  bcxmas  15849  incexclem  15850  incexc  15851  incexc2  15852  isumshft  15853  isumsplit  15854  isumsup2  15860  climcndslem1  15863  climcndslem2  15864  climcnds  15865  supcvg  15870  expcnv  15878  geoserg  15880  pwdif  15882  geolim  15884  geoisum1  15893  geoisum1c  15894  cvgrat  15897  mertenslem1  15898  mertenslem2  15899  mertens  15900  ntrivcvgfvn0  15913  ntrivcvgmullem  15915  prodmolem2a  15948  prodmo  15950  fprodf1o  15960  fproddiv  15975  fprodeq0  15989  risefacval2  16024  fallfacval2  16025  fallfacval3  16026  rprisefaccl  16037  risefallfac  16038  fallfacfwd  16050  binomfallfaclem1  16053  binomfallfaclem2  16054  binomrisefac  16056  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  efcj  16106  fprodefsum  16109  efexp  16117  eftlub  16125  effsumlt  16127  efle  16134  reef11  16135  efieq  16179  sinsub  16184  cossub  16185  subsin  16187  sinmul  16188  cosmul  16189  addcos  16190  subcos  16191  rpnnen2lem10  16239  rpnnen2lem12  16241  ruclem8  16253  ruclem12  16257  sqrt2irr  16265  dvdssub2  16318  dvdsadd  16319  dvdsaddr  16320  dvdssub  16321  dvdssubr  16322  dvdsle  16327  alzdvds  16337  fzocongeq  16341  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  pwp1fsum  16408  divalglem4  16413  divalglem9  16418  divalgb  16421  divalgmod  16423  ndvdsadd  16427  smueqlem  16507  gcdaddm  16542  modgcd  16549  bezoutlem1  16556  dvdsgcd  16561  absmulgcd  16566  rpmulgcd  16574  rprpwr  16576  sqgcd  16579  dvdssqlem  16583  dvdssq  16584  nn0seqcvgd  16587  algrf  16590  algcvg  16593  lcmcllem  16613  lcmabs  16622  lcmgcd  16624  lcmdvds  16625  lcmgcdnn  16628  lcmf  16650  coprmgcdb  16666  coprmdvds  16670  coprmdvds2  16671  qredeq  16674  isprm3  16700  nprm  16705  oddprmgt2  16716  isprm5  16724  isprm7  16725  divgcdodd  16727  prmdvdsexp  16732  zgcdsq  16770  hashdvds  16792  phiprmpw  16793  crth  16795  phimullem  16796  modprm0  16823  coprimeprodsq  16826  coprimeprodsq2  16827  pythagtriplem2  16835  pythagtriplem19  16851  iserodd  16853  pcpremul  16861  pcmul  16869  pcexp  16877  pcdvdsb  16887  pcneg  16892  pc2dvds  16897  pc11  16898  pcmpt  16910  fldivp1  16915  pcfac  16917  infpnlem1  16928  prmunb  16932  prmreclem1  16934  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  1arithlem4  16944  1arith  16945  gzaddcl  16955  gzmulcl  16956  gzreim  16957  gzsubcl  16958  4sqlem1  16966  4sqlem4a  16969  4sqlem4  16970  4sqlem12  16974  ramlb  17037  prmgaplem4  17072  prmgaplem5  17073  prmgaplem6  17074  prmgaplem7  17075  prmgaplem8  17076  prmgapprmolem  17079  cshwshashlem2  17114  setsvalg  17183  ressval  17252  ressval3d  17265  restval  17438  pwsval  17498  xpsval  17582  ssclem  17830  rescval  17838  funcestrcsetclem9  18158  embedsetcestrclem  18167  lubel  18522  ipodrsima  18549  tsrss  18597  resmgmhm  18687  resmgmhm2  18688  mgmhmco  18690  submnd0  18739  mndinvmod  18740  xpsmnd0  18754  resmhm  18796  resmhm2  18797  mhmco  18799  frmdplusg  18830  frmdmnd  18835  efmndcl  18858  smndex1id  18887  mgm2nsgrplem1  18894  mgm2nsgrplem2  18895  mgm2nsgrplem3  18896  sgrp2nmndlem1  18899  sgrp2rid2  18902  dfgrp3  19020  mhmmnd  19045  mulgnngsum  19060  mulgnnsubcl  19067  mulgnn0z  19082  mulgnndir  19084  mulgmodid  19094  eqgfval  19157  cycsubgcl  19187  cycsubg2  19191  0ghm  19211  resghm  19213  resghm2  19214  ghmco  19217  ghmeql  19220  isgim  19243  gicsubgen  19260  cntzmhm  19322  symgcl  19364  symgextf1  19400  gsmsymgrfixlem1  19406  symgfixf1  19416  symgtrinv  19451  pmtrdifellem3  19457  mndodcongi  19522  odmod  19525  odf1  19541  odf1o1  19551  gexdvds  19563  sylow1lem1  19577  pgpssslw  19593  lsmub1  19636  lsmub2  19637  cntzrecd  19657  pj1ghm  19682  lsmhash  19684  efgred  19727  frgpup1  19754  ablsubadd23  19792  ablsubsub23  19803  mulgnn0di  19804  torsubg  19833  zaddablx  19851  gsumzaddlem  19900  gsumzadd  19901  gsumconst  19913  gsumzmhm  19916  telgsumfzslem  19967  dprdfadd  20001  dprd2dlem1  20022  ablsimpgfindlem1  20088  srgbinomlem3  20186  srgbinomlem4  20187  srgbinomlem  20188  gsummgp0  20276  gsumdixp  20277  xpsring1d  20291  unitnegcl  20355  isrnghm  20399  rnghmco  20415  dfrhm2  20432  rhmco  20459  c0rhm  20492  c0rnghm  20493  rhmimasubrng  20524  cntzsubrng  20525  issubrg3  20558  resrhm  20559  rhmeql  20561  rhmima  20562  isdomn4  20674  imadrhmcl  20755  fldsdrgfld  20756  abvres  20789  lmodfopne  20855  lspf  20929  lspcl  20931  0lmhm  20996  lmhmco  20999  lmhmeql  21011  islmim  21018  rngqiprngghm  21258  rngqiprnglin  21261  xrs1cmn  21372  xrsdsreval  21377  xrsdsreclb  21379  znfld  21519  znchr  21521  znunithash  21523  znrrg  21524  freshmansdream  21533  cnmsgnsubg  21535  zrhpsgnmhm  21542  evpmodpmf1o  21554  psgndiflemB  21558  psgndif  21560  phlssphl  21617  frlmval  21706  uvcfval  21742  frlmsslsp  21754  frlmup2  21757  lindfmm  21785  lmimlbs  21794  islindf4  21796  issubassa3  21824  psrbaglesupp  21880  psrcom  21926  resspsrmul  21934  mplsubrglem  21962  mplcoe3  21994  ltbval  21999  ltbwe  22000  evlslem4  22032  evlslem3  22036  psdmvr  22105  psropprmul  22171  coe1tmmul  22212  cply1mul  22232  gsummoncoe1  22244  lply1binomsc  22247  pf1ind  22291  mamufacex  22332  grpvlinv  22334  grpvrinv  22335  eqmat  22360  mat1dimcrng  22413  dmatcrng  22438  scmatf1  22467  m1detdiag  22533  mdetdiaglem  22534  mdet1  22537  mdetunilem9  22556  madulid  22581  gsummatr01lem4  22594  gsummatr01  22595  mat2pmatlin  22671  m2pmfzgsumcl  22684  monmatcollpw  22715  pmatcollpw3lem  22719  mp2pm2mplem4  22745  chpscmatgsummon  22781  chfacfscmulfsupp  22795  chfacfpmmulfsupp  22799  cayhamlem1  22802  cpmadugsumlemF  22812  clsval2  22986  innei  23061  ordtrest  23138  ordtrestixx  23158  isnrm2  23294  lpcls  23300  tgcmp  23337  cmpcld  23338  uncmp  23339  hauscmplem  23342  hauscmp  23343  1stcfb  23381  1stcrest  23389  kgencmp2  23482  1stckgenlem  23489  kgen2ss  23491  kgencn  23492  kgencn3  23494  txval  23500  txuni2  23501  txbasex  23502  txbas  23503  txtop  23505  ptbasin  23513  txtopon  23527  txcld  23539  txss12  23541  txbasval  23542  xkoccn  23555  txcnp  23556  ptcnplem  23557  upxp  23559  txcnmpt  23560  uptx  23561  txrest  23567  txdis  23568  txindislem  23569  txlly  23572  txnlly  23573  txcmp  23579  hausdiag  23581  txhaus  23583  tx1stc  23586  tx2ndc  23587  txkgen  23588  xkoptsub  23590  cnmpt21  23607  txconn  23625  qtopval  23631  hmeoco  23708  txhmeo  23739  xpstopnlem1  23745  fbun  23776  filss  23789  infil  23799  fbunfip  23805  filuni  23821  fmfnfmlem4  23893  ufldom  23898  flffval  23925  flfval  23926  txflf  23942  fcfval  23969  alexsubALTlem3  23985  tgpmulg  24029  subgtgp  24041  qustgplem  24057  tsmsfbas  24064  tsmsres  24080  tsmsmhm  24082  tsmsadd  24083  isxmet2d  24264  blin2  24366  comet  24450  met2ndci  24459  metcn  24480  txmetcn  24485  dscopn  24510  nrmmetd  24511  isngp3  24535  tngval  24576  nm1  24604  subrgnrg  24610  nrginvrcn  24629  rlmnvc  24640  nmo0  24672  nmoco  24674  nghmco  24675  nmotri  24676  0nghm  24678  isnmhm2  24689  0nmhm  24692  nmhmco  24693  nmhmplusg  24694  qtopbaslem  24695  remetdval  24726  bl2ioo  24729  reperflem  24756  iccntr  24759  icccmplem2  24761  icccmp  24763  reconnlem2  24765  xrge0gsumle  24771  xrge0tsms  24772  divcnOLD  24806  divcn  24808  cncfmet  24851  iccpnfcnv  24891  bndth  24906  copco  24967  pcopt  24971  pcopt2  24972  nmhmcn  25069  cmodscexp  25070  cphassr  25162  lmmbrf  25212  lmnn  25213  iscauf  25230  caucfil  25233  iscmet3lem1  25241  iscmet3lem2  25242  iscmet3  25243  cfilres  25246  caussi  25247  caubl  25258  caublcls  25259  bcthlem2  25275  bcthlem5  25278  cmsss  25301  lssbn  25302  ovolfioo  25418  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliunlem2  25454  ovoliunlem3  25455  ovoliun2  25457  ovolscalem1  25464  ovolicc2lem1  25468  ovolicc2lem4  25471  ovolicc2lem5  25472  inmbl  25493  voliunlem1  25501  volsup  25507  ioombl1lem4  25512  iccvolcl  25518  ioovolcl  25521  uniioovol  25530  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombllem6  25539  dyadf  25542  dyadovol  25544  dyadss  25545  dyadmbl  25551  opnmbllem  25552  volsup2  25556  volcn  25557  ismbf  25579  mbfima  25581  ismbf3d  25605  mbfadd  25612  mbfsub  25613  mbflimsup  25617  itg1mulc  25655  itg1sub  25660  itg1climres  25665  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfmul  25677  itg2const2  25692  itg2seq  25693  itg2uba  25694  itg2lea  25695  itg2eqa  25696  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  itg2cnlem1  25712  bddmulibl  25790  ellimc3  25830  dvaddbr  25890  dvcobr  25899  dvcobrOLD  25900  dvcjbr  25903  dvcnvlem  25930  c1lip1  25952  lhop  25971  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumrlimf  25981  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  tdeglem4  26015  deg1ge  26053  coe1mul3  26054  fta1g  26125  plyco0  26147  plyf  26153  ply1termlem  26158  plyeq0lem  26165  plypf1  26167  plymullem1  26169  plyaddlem  26170  plymullem  26171  coeeulem  26179  coeidlem  26192  plyco  26196  dgreq  26199  coefv0  26203  coeaddlem  26204  coemullem  26205  coemulhi  26209  coemulc  26210  plycn  26216  plycnOLD  26217  dgrlt  26222  dgrsub  26228  plycjlem  26232  plycj  26233  plycjOLD  26235  plyrecj  26237  plymul0or  26238  plyreres  26240  dvply1  26241  vieta1lem2  26269  plyexmo  26271  elqaalem2  26278  elqaalem3  26279  aareccl  26284  aalioulem1  26290  aalioulem3  26292  aaliou  26296  geolim3  26297  ulmcaulem  26353  ulmcau  26354  mtest  26363  dvradcnv  26380  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv2  26390  abelthlem6  26396  abelthlem8  26399  abelthlem9  26400  reeff1o  26407  reefgim  26410  sinperlem  26439  sincosq2sgn  26458  sincosq3sgn  26459  sinq12ge0  26467  sincos6thpi  26475  sineq0  26483  cosord  26490  cos11  26492  sinord  26493  tanord1  26496  eff1olem  26507  logrnaddcl  26533  relogeftb  26543  relogoprlem  26550  logleb  26562  advlogexp  26614  logtayllem  26618  logtayl  26619  logtaylsum  26620  logtayl2  26621  recxpcl  26634  rpcxpcl  26635  cxple3  26660  cxpcom  26698  cxpcn3  26708  cxpeq  26717  relogbmul  26737  relogbcxp  26745  relogbf  26751  atanord  26887  atantayl  26897  birthdaylem2  26912  birthdaylem3  26913  cxp2limlem  26936  fsumharmonic  26972  zetacvg  26975  ftalem1  27033  ftalem4  27036  ftalem5  27037  basellem2  27042  basellem3  27043  basellem4  27044  vmappw  27076  sqf11  27099  mumul  27141  fsumdvdscom  27145  dvdsppwf1o  27146  dvdsflf1o  27147  musum  27151  muinv  27153  fsumdvdsmul  27155  1sgmprm  27160  vmalelog  27166  chtublem  27172  fsumvma  27174  vmasum  27177  logfac2  27178  chpval2  27179  logfaclbnd  27183  logexprlim  27186  mersenne  27188  dchrmulcl  27210  dchrinvcl  27214  dchrfi  27216  dchrghm  27217  dchrptlem1  27225  dchrsum2  27229  dchrsum  27230  pcbcctr  27237  bcmono  27238  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem5  27249  bposlem6  27250  bposlem7  27251  lgslem3  27260  lgscllem  27265  lgsval4a  27280  lgsneg  27282  lgsdir2  27291  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  gausslemma2dlem1a  27326  gausslemma2dlem3  27329  gausslemma2dlem6  27333  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2  27347  lgsquad3  27348  2lgslem1a1  27350  2lgslem1a  27352  2lgslem1c  27354  2sqlem2  27379  mul2sq  27380  2sqlem7  27385  2sqreultlem  27408  2sqreunnltlem  27411  2sqreunnltblem  27412  chebbnd1lem1  27430  vmadivsum  27443  rplogsumlem2  27446  dchrisum0lem1a  27447  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasum2if  27458  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  dchrisum0ff  27468  dchrisum0flblem1  27469  dchrisum0fno1  27472  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  mudivsum  27491  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  selberglem2  27507  selberg2  27512  chpdifbndlem1  27514  selberg3lem1  27518  pntrsumbnd2  27528  selbergr  27529  pntpbnd1  27547  pntpbnd2  27548  pntlemh  27560  pntlemj  27564  pntlemi  27565  pntlemf  27566  pntlemp  27571  ostth2lem1  27579  ostth1  27594  ostth2lem3  27596  ostth3  27599  noreson  27622  nosepon  27627  noextendseq  27629  nosupbnd1lem5  27674  noetasuplem4  27698  addscom  27916  negsdi  27999  om2noseqlt  28222  om2noseqf1o  28224  n0s0suc  28262  nnsge1  28263  n0sbday  28271  zaddscl  28297  elzn0s  28301  zseo  28323  pw2bday  28335  remulscllem2  28350  istrkg2ld  28385  isismt  28459  eedimeq  28823  eqeefv  28828  brbtwn2  28830  colinearalglem1  28831  colinearalglem2  28832  colinearalg  28835  eleesub  28836  eleesubd  28837  axcgrrflx  28839  axcgrid  28841  axsegconlem2  28843  axsegconlem7  28848  axsegconlem9  28850  axsegconlem10  28851  axlowdimlem14  28880  axlowdimlem16  28882  axlowdimlem17  28883  axcontlem2  28890  axcontlem4  28892  axcontlem8  28896  axcontlem10  28898  structiedg0val  28947  upgr1eop  29040  numedglnl  29069  usgredg2v  29152  ushgredgedg  29154  ushgredgedgloop  29156  uspgr1eop  29172  usgr1eop  29175  uhgrissubgr  29200  umgrres1lem  29235  upgrres1  29238  nbuhgr  29268  edgnbusgreu  29292  nb3gr2nb  29309  uvtxnm1nbgr  29329  cusgrexilem2  29367  finsumvtxdg2ssteplem4  29474  vtxdgoddnumeven  29479  wlkeq  29560  uspgr2wlkeq  29572  wlksoneq1eq2  29590  upgrwlkdvdelem  29664  usgr2wlkspthlem1  29685  usgrn2cycl  29737  crctcshwlkn0lem3  29740  crctcshwlkn0lem6  29743  crctcshwlkn0lem7  29744  crctcshwlkn0  29749  wspthneq1eq2  29788  wwlkseq  29819  wwlksnext  29821  rusgrnumwlkg  29905  clwwlkccatlem  29916  clwwlkccat  29917  clwlkclwwlklem2a4  29924  clwlkclwwlklem2  29927  clwlkclwwlkf1lem3  29933  clwwisshclwwslemlem  29940  clwwisshclwws  29942  erclwwlkeqlen  29946  erclwwlkref  29947  clwwnisshclwwsn  29986  clwwlknccat  29990  erclwwlkneqlen  29995  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwlksndivn  30013  uhgr3cyclex  30109  eucrctshift  30170  eucrct2eupth  30172  frgreu  30195  frgr3v  30202  3vfriswmgr  30205  frgrncvvdeqlem3  30228  frgrregorufrg  30253  numclwwlk1lem2f1  30284  numclwwlk1lem2fo  30285  numclwlk1lem2  30297  numclwwlk3  30312  numclwwlk6  30317  frgrreg  30321  frgrregord013  30322  nsnlplig  30408  nsnlpligALT  30409  ablodivdiv4  30481  imsdval  30613  nmcvcn  30622  sspval  30650  lnoadd  30685  lnosub  30686  nmooge0  30694  nmoolb  30698  nmoub3i  30700  blocnilem  30731  blocni  30732  cncph  30746  ipasslem1  30758  ipasslem2  30759  ipasslem4  30761  ipasslem11  30767  ipblnfi  30782  phoeqi  30784  ubthlem1  30797  ubthlem3  30799  htthlem  30844  hvsub4  30964  his7  31017  his2sub2  31020  hial2eq2  31034  hhip  31104  hhph  31105  bcs2  31109  hhssabloi  31189  hhssnv  31191  ocorth  31218  shsel  31241  shsel3  31242  shscli  31244  chsupss  31269  shjval  31278  chjval  31279  shjcl  31283  chjcl  31284  shsleji  31297  chslej  31425  chsscon2  31429  chjcom  31433  chub1  31434  chdmj1  31456  spanunsni  31506  spanpr  31507  fh1  31545  fh2  31546  cm2j  31547  spansncvi  31579  5oalem1  31581  5oalem3  31583  5oalem5  31585  3oalem2  31590  pjcompi  31599  pjds3i  31640  hoeq  31687  hoadddi  31730  hoadddir  31731  hosubdi  31735  hosub4  31740  hoeq1  31757  hoeq2  31758  adjval2  31818  counop  31848  adjeq  31862  brafnmul  31878  lnopsubi  31901  hmops  31947  hmopm  31948  hmopd  31949  hmopco  31950  nmcopexi  31954  lnconi  31960  lnfnsubi  31973  nmcfnexi  31978  imaelshi  31985  nlelshi  31987  riesz3i  31989  riesz1  31992  cnlnadjlem2  31995  cnlnadjlem6  31999  adjbdln  32010  adjlnop  32013  adjmul  32019  adjadd  32020  nmopcoi  32022  rnbra  32034  cnvbramul  32042  kbass2  32044  kbass4  32046  kbass5  32047  kbass6  32048  leopadd  32059  leopmul2i  32062  leoptri  32063  dmdmd  32227  mddmd  32228  cvdmd  32264  superpos  32281  chrelati  32291  atcv0eq  32306  atomli  32309  atcvatlem  32312  atcvati  32313  atcvat2i  32314  chirredlem4  32320  atcvat3i  32323  atcvat4i  32324  mdsymlem2  32331  mdsymlem3  32332  mdsymlem5  32334  mdsymlem8  32337  dmdsym  32340  cdjreui  32359  cdj1i  32360  cdj3lem2b  32364  cdj3lem3  32365  cdj3lem3b  32367  cdj3i  32368  brabgaf  32534  prct  32638  fcobijfs  32646  fzsplit3  32716  bcm1n  32718  dpfrac1  32812  wrdres  32856  xrge0mulgnn0  32956  xrge0tsmsd  33002  xrge0omnd  33025  cycpmco2  33090  suborng  33283  isarchiofld  33285  resvval  33291  nsgqusf1olem2  33375  lbslsat  33602  ply1degltdimlem  33608  ply1degltdim  33609  ordtrestNEW  33898  mhmhmeotmd  33904  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0pluscn  33917  hasheuni  34062  sxval  34167  measvuni  34191  ddemeas  34213  br2base  34247  dya2iocucvr  34262  sxbrsigalem2  34264  sxbrsiga  34268  omssubadd  34278  eulerpartlemgc  34340  ballotlemfc0  34471  ballotlemfcc  34472  signstfvc  34552  signstres  34553  signsvfn  34560  bnj563  34720  bnj554  34876  bnj557  34878  bnj570  34882  bnj594  34889  bnj849  34902  bnj970  34924  bnj1118  34961  bnj1145  34970  bnj1190  34985  bnj1398  35011  bnj1417  35018  zltp1ne  35078  nnltp1ne  35079  nn0ltp1ne  35080  0nn0m1nnn0  35081  cusgr3cyclex  35104  derangsn  35138  derangen  35140  subfacp1lem5  35152  erdsze2lem1  35171  txpconn  35200  txsconn  35209  cvmliftphtlem  35285  satfdm  35337  satfun  35379  ex-sategoelel  35389  mrsubff1  35482  msubff  35498  msubff1  35524  msubvrs  35528  inffz  35693  bcprod  35701  bccolsum  35702  faclim  35709  dfon2lem4  35750  colineardim1  36025  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem12  36062  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeu  36095  funray  36104  lineintmo  36121  fwddifnp1  36129  hfun  36142  nn0prpw  36287  opnregcld  36294  cldregopn  36295  ivthALT  36299  onsucconni  36401  bj-nnfim1  36708  bj-nnfim2  36709  bj-2uplex  36986  bj-unexg  37002  bj-prexg  37003  bj-idres  37124  isbasisrelowllem1  37319  isbasisrelowllem2  37320  icoreclin  37321  relowlssretop  37327  exrecfnlem  37343  pibt2  37381  unccur  37573  phpreu  37574  finixpnum  37575  ltflcei  37578  cos2h  37581  lindsadd  37583  lindsdom  37584  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  heicant  37625  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  ovoliunnfl  37632  mbfresfi  37636  itg2addnclem  37641  itg2addnc  37644  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  indexa  37703  incsequz  37718  incsequz2  37719  geomcau  37729  sstotbnd2  37744  prdsbnd  37763  prdstotbnd  37764  prdsbnd2  37765  cntotbnd  37766  ismtyhmeolem  37774  ismtybndlem  37776  heibor1lem  37779  heiborlem3  37783  heiborlem6  37786  heibor  37791  bfplem1  37792  bfplem2  37793  elghomlem1OLD  37855  rngogrphom  37941  prnc  38037  ispridlc  38040  pridlc3  38043  mpobi123f  38132  mptbi12f  38136  antisymressn  38408  eqvreltr  38571  ax12indalem  38909  lsateln0  38959  atlatmstc  39283  hlatjidm  39333  llnneat  39479  lplnneat  39510  lplnnelln  39511  lvolneatN  39553  lvolnelln  39554  lvolnelpln  39555  dalem23  39661  snatpsubN  39715  linepsubN  39717  pmapsub  39733  pmapglbx  39734  paddasslem14  39798  polsubN  39872  pol1N  39875  2polvalN  39879  2polssN  39880  3polN  39881  2pmaplubN  39891  polatN  39896  2polatN  39897  pnonsingN  39898  polsubclN  39917  lautco  40062  cdlemefrs29cpre1  40363  dian0  41004  dia0eldmN  41005  dia1eldmN  41006  dia0  41017  dia1N  41018  dvhopaddN  41079  dib0  41129  dih0  41245  dih1  41251  dihglblem5apreN  41256  dihatexv2  41304  dochfN  41321  lcmineqlem1  41988  lcmineqlem17  42004  factwoffsmonot  42201  xppss12  42226  sumcubes  42309  dvdsexpnn  42329  remul01  42397  resubeqsub  42419  ricdrng1  42498  prjspeclsp  42582  ismrcd2  42669  nacsfix  42682  mzpaddmpt  42711  mzpmulmpt  42712  eq0rabdioph  42746  lerabdioph  42775  ltrabdioph  42778  nerabdioph  42779  dvdsrabdioph  42780  fiphp3d  42789  congneg  42940  jm2.22  42966  jm2.23  42967  jm2.15nn0  42974  jm3.1  42991  aomclem8  43032  lsmfgcl  43045  lmhmfgima  43055  lnmepi  43056  dgrsub2  43106  mpaaeu  43121  mendring  43159  proot1ex  43167  unielss  43189  onsucwordi  43259  oaabsb  43265  rp-oelim2  43279  nnoeomeqom  43283  cantnfresb  43295  oawordex2  43297  omcl3g  43305  ordsssucb  43306  tfsconcatrev  43319  onsucunipr  43343  onsucunitp  43344  oaun3lem1  43345  naddgeoa  43365  oaltom  43376  minregex2  43506  sssymdifcl  43543  relexp01min  43684  ntrclsiso  44038  ntrclsk3  44041  cvgdvgrat  44285  nznngen  44288  uzmptshftfval  44318  addrval  44438  subrval  44439  mulvval  44440  elpwgded  44537  eel2131  44686  eel3132  44687  el12  44698  sspwimp  44890  sspwimpcf  44892  suctrALTcf  44894  suctrALT3  44896  relpfrlem  44926  cnfex  45000  disjinfi  45164  infxrbnd2  45344  supminfxr  45439  climinf  45583  lptre2pt  45617  limcresiooub  45619  limcresioolb  45620  addlimc  45625  limclner  45628  limsuppnflem  45687  limsupmnfuzlem  45703  limsupvaluz2  45715  limsupresxr  45743  liminfresxr  45744  cnrefiisplem  45806  cncfdmsn  45867  iblspltprt  45950  itgspltprt  45956  dirkertrigeqlem3  46077  fourierdlem62  46145  fourierdlem80  46163  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem114  46197  sge0f1o  46359  hoidmvlelem2  46573  pimdecfgtioo  46694  smfliminflem  46807  fnresfnco  47018  fcores  47044  dfatcolem  47232  nn0resubcl  47285  zgeltp1eq  47286  eluzge0nn0  47289  fz0addcom  47294  elfzlble  47297  fzopredsuc  47300  subsubelfzo0  47303  ceilbi  47310  minusmod5ne  47326  submodlt  47327  uniimafveqt  47343  fundcmpsurinjimaid  47373  icceuelpartlem  47397  iccpartnel  47400  elsprel  47437  fmtnodvds  47506  goldbachth  47509  fmtnoprmfac2  47529  prmdvdsfmtnof1  47549  2pwp1prm  47551  flsqrt  47555  lighneallem4  47572  dfodd6  47599  divgcdoddALTV  47644  opoeALTV  47645  opeoALTV  47646  omoeALTV  47647  omeoALTV  47648  epoo  47665  emoo  47666  epee  47667  emee  47668  evensumeven  47669  even3prm2  47681  mogoldbblem  47682  fpprmod  47689  dfwppr  47700  fpprwppr  47701  fpprwpprb  47702  gbepos  47720  gbegt5  47723  gbowgt5  47724  gboge9  47726  sbgoldbst  47740  nnsum3primesgbe  47754  bgoldbtbndlem1  47767  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  grimco  47850  isuspgrim0  47855  isuspgrimlem  47856  uhgrimisgrgriclem  47891  uhgrimisgrgric  47892  clnbgrgrim  47895  grimedg  47896  isgrtri  47903  cycl3grtri  47907  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  isubgr3stgrlem8  47933  uspgrlimlem2  47949  uspgrlimlem3  47950  uspgrlimlem4  47951  grlictr  47968  gpgusgralem  48008  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  gpg5grlic  48041  2zrngmmgm  48175  2zrngnmrid  48179  2zrngnmlid2  48180  altgsumbc  48275  altgsumbcALT  48276  zlmodzxzadd  48281  zlmodzxzsub  48283  invginvrid  48290  ply1mulgsumlem2  48311  ply1mulgsum  48314  lincvalpr  48342  lindslinindimp2lem1  48382  ldepsprlem  48396  ldepspr  48397  lincresunit3lem3  48398  lincresunitlem1  48399  lincresunit3lem1  48403  lincresunit3  48405  elfzolborelfzop1  48443  zgtp1leeq  48445  flsubz  48446  mod0mul  48447  m1modmmod  48449  nneom  48455  nn0ofldiv2  48460  rege1logbrege0  48486  nnpw2pb  48515  dignn0fr  48529  dignn0ldlem  48530  dignnld  48531  dignn0flhalflem1  48543  nn0sumshdiglemB  48548  nn0mulfsum  48552  rrx2plordisom  48651  ehl2eudis0lt  48654  itsclinecirc0in  48703  2itscp  48709  inlinecirc02plem  48714  mof0ALT  48766  i0oii  48842  resccat  48989