Theorem syl2an 607

Description: A double syllogism inference. For an implication-only version, see syl2im 41. (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 591	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 604	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anr  608  anim12i  624  anim12ii  629  bi2anan9  649  syl3an132  1182  mp3an3an  1491  ax13  2409  nfeqf  2415  eqeqan12dALT  2784  sylan9eq  2820  sylan9ss  3952  ssconb  4098  ineqan12d  4177  ifpr  4655  disjtp2  4678  dfopg  4831  disjxiun  5101  breqan12d  5120  eusv1  5352  opelvvg  5692  opthprc  5715  relop  5826  dmpropg  6205  unixp  6272  tz7.7  6375  ordin  6380  onin  6381  ontri1  6384  onfr  6389  onelpss  6390  onsseleq  6391  oneltri  6393  ontr2  6398  onunel  6457  onun2  6460  funssres  6569  funtpg  6580  funtp  6582  resasplit  6738  fodmrnu  6790  f1un  6831  dffv2  6966  fvreseq0  7023  fvcofneq  7078  funopdmsn  7137  fprg  7142  fprb  7182  fconst2g  7191  isofrlem  7328  oveqan12d  7419  ov3  7563  ovg  7565  ovima0  7579  f1opw2  7655  off  7682  unexgOLD  7736  pwuncl  7757  epweon  7762  epweonALT  7763  sucexeloni  7796  ordunpr  7810  omun  7872  peano4  7877  fabexg  7923  f1oabexg  7926  fiun  7928  offres  7968  el2mpocsbcl  8068  curry1  8087  curry1val  8088  curry2  8090  curry2val  8092  soxp  8113  wexp  8114  xpord2pred  8129  poxp3  8134  poseq  8142  soseq  8143  suppfnss  8173  frrlem4  8274  frrlem11  8281  frrlem12  8282  fprlem1  8285  iunon  8314  onfununi  8316  tfrlem11  8363  tz7.48lem  8416  seqomeq12  8429  oacan  8521  oawordri  8523  oaass  8534  omord2  8540  omcan  8542  oen0  8560  oeordi  8561  oeord  8562  oecan  8563  oeworde  8567  oeordsuc  8568  oelimcl  8574  nnawordi  8595  nnaword  8601  nnmord  8606  oaabslem  8621  omabslem  8624  omsmo  8632  eldifsucnn  8638  naddcllem  8650  naddov2  8653  ertr  8698  erex  8707  brecop  8796  ecopovtrn  8806  ecovdi  8811  mapvalg  8821  pmvalg  8822  pmss12g  8855  elmapresaun  8866  boxcutc  8927  undom  9041  sbthlem7  9069  sbth  9073  sdomnsym  9078  sdomdomtr  9086  xpf1o  9115  xpen  9116  limenpsi  9128  pssnn  9141  pwssfi  9149  sbthfi  9171  php2  9180  php3  9181  phpeqd  9184  nndomog  9185  onomeneq  9186  isinf  9213  fineqvlem  9214  f1finf1o  9221  dif1ennnALT  9225  findcard3  9231  unblem2  9241  isfinite2  9246  unfilem1  9253  unfi2  9258  fodomfir  9275  unifi2  9290  f1opwfi  9301  fsuppxpfi  9333  fsuppunbi  9337  fsuppco2  9351  fsuppcor  9352  fival  9360  fiin  9370  ordiso  9466  ordtypelem10  9477  hartogslem1  9492  wofib  9495  brwdom3  9532  unwdomg  9534  xpwdomg  9535  sucprcregOLD  9557  preleqALT  9574  inf3lem6  9590  oemapval  9640  cantnf  9650  wemapwe  9654  cnfcom  9657  ttrcltr  9673  dfttrcl2  9681  frmin  9709  r111  9735  r1ord3g  9739  prwf  9771  r1pw  9805  rankprb  9811  rankxplim  9839  tcrank  9844  updjud  9908  finnum  9922  xpnum  9925  carduni  9955  nnsdomel  9964  fidomtri  9967  infxpenlem  9985  fseqdom  9998  onssnum  10012  acndom2  10026  alephinit  10067  dfac5lem4  10098  kmlem6  10127  undjudom  10139  endjudisj  10140  djuen  10141  djucomen  10149  pwdjuen  10153  djudom1  10154  djuxpdom  10157  djufi  10158  cardadju  10166  nnadju  10169  nnadjuALT  10170  ficardadju  10171  ficardun  10172  ficardun2  10173  pwsdompw  10174  unctb  10175  ackbij2lem1  10189  ackbij1lem6  10195  ackbij1lem16  10205  ackbij1b  10209  ackbij2  10213  coflim  10233  cflim2  10235  cofsmo  10241  coftr  10245  sornom  10249  infpssrlem5  10279  fin4en1  10281  fin23lem23  10298  fin23lem28  10312  isf32lem2  10326  isf32lem4  10328  isf32lem7  10331  isf34lem7  10351  isf34lem6  10352  fin67  10367  isfin7-2  10368  fin1a2lem9  10380  domtriomlem  10414  axdc3lem2  10423  axdc3lem4  10425  axdc4lem  10427  zorn2lem6  10473  ttukeylem3  10483  brdom6disj  10504  carddom  10526  cardsdom  10527  domtri  10528  konigthlem  10541  iunctb  10547  alephadd  10550  alephmul  10551  pwcfsdom  10556  cfpwsdom  10557  fpwwe2lem12  10615  canthp1lem2  10626  pwfseqlem3  10633  pwfseqlem4a  10634  inar1  10748  tskcard  10754  tskuni  10756  grur1  10793  mulclpi  10866  addcompi  10867  mulcompi  10869  distrpi  10871  ltexpi  10875  ltapi  10876  ltmpi  10877  enqbreq2  10893  nqereu  10902  addpipq  10910  addpqnq  10911  mulpipq  10913  mulpqnq  10914  addpqf  10917  addclnq  10918  mulpqf  10919  mulclnq  10920  adderpq  10929  mulerpq  10930  ltsonq  10942  lterpq  10943  ltbtwnnq  10951  ltrnq  10952  genpv  10972  genpdm  10975  genpnnp  10978  mulclprlem  10992  distrlem1pr  10998  distrlem4pr  10999  prlem934  11006  addcanpr  11019  suplem1pr  11025  mulcmpblnr  11044  mulclsr  11057  mulasssr  11063  distrsr  11064  ltsosr  11067  1idsr  11071  00sr  11072  recexsrlem  11076  mulgt0sr  11078  addcnsr  11108  axmulf  11119  axmulass  11130  axdistr  11131  axcnre  11137  mulrid  11194  axltadd  11271  lenlt  11276  dedekind  11361  dedekindle  11362  resubcl  11510  subeqrev  11624  muladd  11634  mulsub  11645  mulsub2  11646  ltaddsub2  11677  leaddsub2  11679  leltadd  11686  ltaddpos2  11693  posdif  11695  addge02  11713  mullt0  11721  ltord1  11728  leord1  11729  eqord1  11730  recextlem1  11832  recex  11834  divmuldiv  11903  conjmul  11920  div2sub  12028  prodgt02  12051  lemul2  12056  lemul2a  12058  ltmulgt12  12063  lemulge12  12066  mulge0b  12073  mulle0b  12074  ltmuldiv2  12077  ltdivmul2  12080  lt2mul2div  12081  ledivmul2  12082  lemuldiv2  12084  ledivdiv  12092  lediv2  12093  ltdiv23  12094  lediv23  12095  supmul  12175  riotaneg  12182  negiso  12183  cju  12202  nnaddcl  12244  nnmulcl  12245  nnmtmip  12250  nnsub  12268  addltmul  12468  avgle1  12472  avgle2  12473  avgle  12474  nnrecl  12490  nn0nnaddcl  12523  nn0sub  12542  elz2  12597  zaddcl  12622  zsubcl  12624  znnsub  12628  znn0sub  12629  nzadd  12630  zmulcl  12631  zltp1le  12632  zleltp1  12633  nnleltp1  12639  nnltp1le  12640  nnaddm1cl  12641  nn0ltp1le  12642  nn0leltp1  12643  nn0ltlem1  12644  nn0lem1lt  12649  nnlem1lt  12650  nnltlem1  12651  zdiv  12654  zextle  12657  zextlt  12658  btwnnz  12660  prime  12665  nneo  12668  peano2uz2  12672  uzind  12676  fzind  12682  zriotaneg  12697  uzneg  12870  uztric  12874  uz11  12875  eluzp1m1  12876  eluzp1p1  12878  uzin  12886  uzwo  12923  indstr  12928  uz2mulcl  12938  supminf  12947  uzsupss  12952  zmax  12957  rebtwnz  12959  qre  12965  qaddcl  12977  qsubcl  12980  irradd  12985  elpqb  12988  rpnnen1lem5  12993  cnref1o  12997  rpaddcl  13028  rpmulcl  13029  rpmtmip  13030  rpdivcl  13031  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  13526  elfz1eq  13551  peano2fzr  13553  fzn  13556  fzsplit2  13565  fzaddel  13574  fzadd2  13575  fzsubel  13576  fzrev2  13604  fzrev3  13606  uzsplit  13612  fznuz  13625  uznfz  13626  fzrevral  13628  fzrevral3  13630  fzshftral  13631  elfz2nn0  13634  fznn0sub2  13651  fz0fzdiffz0  13653  elfzmlbp  13655  difelfzle  13657  difelfznle  13658  elfzouz2  13691  fzo0n  13698  fzouzsplit  13711  fzoun  13713  elfzo0le  13720  fzonmapblen  13725  fzofzim  13726  fzoaddel2  13737  eluzgtdifelfzo  13744  elfzodifsumelfzo  13748  ssfzoulel  13777  ubmelm1fzo  13780  fzofzp1b  13782  elfzonelfzo  13786  elfznelfzo  13790  fzostep1  13803  injresinjlem  13807  subfzo0  13809  flflp1  13828  divfl0  13845  flzadd  13847  flmulnn0  13848  fldivnn0le  13853  fldiv  13881  uzsup  13884  mulmod0  13898  modlt  13901  modmulnn  13910  zmodcl  13912  zmodfz  13914  zmodid2  13920  modcyc  13927  muladdmodid  13934  modmuladdnn0  13939  negmod  13940  addmodidr  13944  modadd2mod  13945  modaddmodup  13958  modaddmulmod  13962  modfzo0difsn  13967  modsumfzodifsn  13968  addmodlteq  13970  om2uzlti  13974  om2uzf1oi  13977  fzen2  13993  ssnn0fi  14009  fsuppmapnn0fiublem  14014  fsuppmapnn0fiub0  14017  seqshft2  14052  seqsplit  14059  seqcaopr2  14062  seqf1olem2  14066  expcllem  14096  expcl2lem  14097  1exp  14115  expge1  14123  expadd  14128  expmul  14131  expsub  14134  nn0sq11  14156  lt2sq  14157  le2sq  14158  expmordi  14191  leexp2  14195  leexp1a  14199  sumsqeq0  14203  bernneq  14253  bernneq2  14254  expnbnd  14256  digit2  14260  digit1  14261  facdiv  14311  facwordi  14313  faclbnd  14314  faclbnd3  14316  faclbnd4lem4  14320  faclbnd5  14322  faclbnd6  14323  facavg  14325  bcrpcl  14332  bccmpl  14333  bcval5  14342  hashen  14371  hasheqf1oi  14375  hashgadd  14401  hashdom  14403  hashsdom  14405  hashun  14406  hashunsnggt  14418  hashprg  14419  hashssdif  14437  hashxplem  14458  seqcoll  14489  tpf1o  14526  eqwrd  14582  ccatfval  14598  ccatlen  14600  ccat0  14601  elfzelfzccat  14605  ccatsymb  14608  ccatval21sw  14611  ccatrn  14615  lswccatn0lsw  14617  ccatalpha  14619  ccatrcl1  14620  ccats1alpha  14645  swrdnd  14680  swrdfv2  14687  swrdsbslen  14690  swrdspsleq  14691  swrdccat2  14695  pfxnd0  14714  pfxeq  14721  ccatpfx  14726  pfxccat1  14727  swrdswrdlem  14729  pfxswrd  14731  pfxccatin12lem4  14751  pfxccatin12lem1  14753  pfxccatin12lem2  14756  pfxccatin12lem3  14757  pfxccatin12  14758  pfxccat3  14759  swrdccat  14760  pfxccatpfx2  14762  pfxccat3a  14763  swrdccat3blem  14764  swrdccat3b  14765  revccat  14791  revrev  14792  cshwlen  14824  cshwidxmod  14828  cshwidxmodr  14829  cshweqdif2  14844  cshweqrep  14846  2cshwcshw  14850  s3eq3seq  14964  cotr2g  15001  trclun  15039  shftf  15104  seqshft  15110  crre  15153  crim  15154  readd  15165  resub  15166  remul2  15169  imadd  15173  imsub  15174  immul2  15176  ipcnval  15182  cjsub  15188  cjreim  15199  01sqrexlem6  15286  sqrtle  15299  sqrt11  15301  absreimsq  15331  absreim  15332  absmul  15333  sqabs  15346  absdiflt  15357  absdifle  15358  abssuble0  15368  absmax  15369  abs2difabs  15374  fzomaxdif  15383  rexanuz  15385  rexuz3  15388  rexuzre  15392  caubnd2  15397  limsupgre  15520  limsupbnd2  15522  climconst2  15587  lo1resb  15603  o1resb  15605  2clim  15611  climshftlem  15613  climshft  15615  climshft2  15621  cjcn2  15639  o1of2  15652  o1rlimmul  15658  climaddc1  15674  climmulc2  15676  climsubc1  15677  climsubc2  15678  lo1le  15691  climlec2  15698  isershft  15703  isercolllem1  15704  isercolllem3  15706  isercoll  15707  isercoll2  15708  climsup  15709  caurcvg  15716  caucvg  15718  iseraltlem1  15721  iseraltlem2  15722  iseralt  15724  summolem2a  15754  isumclim3  15798  mptfzshft  15817  fsumrev  15818  fsum0diag2  15822  fsumconst  15829  telfsumo2  15843  fsumparts  15846  o1fsum  15853  cvgcmp  15856  cvgcmpub  15857  cvgcmpce  15858  binomlem  15871  binom1p  15873  binom1dif  15875  bcxmas  15877  incexclem  15878  incexc  15879  incexc2  15880  isumshft  15881  isumsplit  15882  isumsup2  15888  climcndslem1  15891  climcndslem2  15892  climcnds  15893  supcvg  15898  expcnv  15906  geoserg  15908  pwdif  15910  geolim  15912  geoisum1  15921  geoisum1c  15922  cvgrat  15925  mertenslem1  15926  mertenslem2  15927  mertens  15928  ntrivcvgfvn0  15941  ntrivcvgmullem  15943  prodmolem2a  15976  prodmo  15978  fprodf1o  15988  fproddiv  16003  fprodeq0  16017  risefacval2  16052  fallfacval2  16053  fallfacval3  16054  rprisefaccl  16065  risefallfac  16066  fallfacfwd  16078  binomfallfaclem1  16081  binomfallfaclem2  16082  binomrisefac  16084  bpolycl  16094  bpolysum  16095  bpolydiflem  16096  fsumkthpow  16098  efcj  16134  fprodefsum  16137  efexp  16145  eftlub  16153  effsumlt  16155  efle  16162  reef11  16163  efieq  16207  sinsub  16212  cossub  16213  subsin  16215  sinmul  16216  cosmul  16217  addcos  16218  subcos  16219  rpnnen2lem10  16267  rpnnen2lem12  16269  ruclem8  16281  ruclem12  16285  sqrt2irr  16293  dvdssub2  16347  dvdsadd  16348  dvdsaddr  16349  dvdssub  16350  dvdssubr  16351  dvdsle  16356  alzdvds  16366  fzocongeq  16370  odd2np1  16387  opoe  16409  omoe  16410  opeo  16411  omeo  16412  pwp1fsum  16437  divalglem4  16442  divalglem9  16447  divalgb  16450  divalgmod  16452  ndvdsadd  16456  smueqlem  16536  gcdaddm  16571  modgcd  16578  bezoutlem1  16585  dvdsgcd  16590  absmulgcd  16595  rpmulgcd  16603  rprpwr  16605  sqgcd  16608  dvdssqlem  16612  dvdssq  16613  nn0seqcvgd  16616  algrf  16619  algcvg  16622  lcmcllem  16642  lcmabs  16651  lcmgcd  16653  lcmdvds  16654  lcmgcdnn  16657  lcmf  16679  coprmgcdb  16695  coprmdvds  16699  coprmdvds2  16700  qredeq  16703  isprm3  16729  nprm  16734  oddprmgt2  16746  isprm5  16754  isprm7  16755  divgcdodd  16757  prmdvdsexp  16762  zgcdsq  16800  hashdvds  16822  phiprmpw  16823  crth  16825  phimullem  16826  modprm0  16853  coprimeprodsq  16856  coprimeprodsq2  16857  pythagtriplem2  16865  pythagtriplem19  16881  iserodd  16883  pcpremul  16891  pcmul  16899  pcexp  16907  pcdvdsb  16917  pcneg  16922  pc2dvds  16927  pc11  16928  pcmpt  16940  fldivp1  16945  pcfac  16947  infpnlem1  16958  prmunb  16962  prmreclem1  16964  prmreclem3  16966  prmreclem4  16967  prmreclem5  16968  1arithlem4  16974  1arith  16975  gzaddcl  16985  gzmulcl  16986  gzreim  16987  gzsubcl  16988  4sqlem1  16996  4sqlem4a  16999  4sqlem4  17000  4sqlem12  17004  ramlb  17067  prmgaplem4  17102  prmgaplem5  17103  prmgaplem6  17104  prmgaplem7  17105  prmgaplem8  17106  prmgapprmolem  17109  cshwshashlem2  17144  setsvalg  17214  ressval  17281  ressval3d  17294  restval  17467  pwsval  17527  xpsval  17612  ssclem  17864  rescval  17872  funcestrcsetclem9  18192  embedsetcestrclem  18201  lubel  18558  ipodrsima  18585  tsrss  18633  chnrdss  18661  resmgmhm  18757  resmgmhm2  18758  mgmhmco  18760  submnd0  18809  mndinvmod  18810  xpsmnd0  18824  resmhm  18867  resmhm2  18868  mhmco  18870  frmdplusg  18901  frmdmnd  18906  efmndcl  18929  smndex1id  18961  mgm2nsgrplem1  18968  mgm2nsgrplem2  18969  mgm2nsgrplem3  18970  sgrp2nmndlem1  18973  sgrp2rid2  18976  dfgrp3  19093  mhmmnd  19118  mulgnngsum  19133  mulgnnsubcl  19140  mulgnn0z  19155  mulgnndir  19157  mulgmodid  19167  eqgfval  19232  cycsubgcl  19265  cycsubg2  19269  0ghm  19288  resghm  19290  resghm2  19291  ghmco  19294  ghmeql  19297  isgim  19320  gicsubgen  19337  cntzmhm  19399  symgcl  19443  symgextf1  19479  gsmsymgrfixlem1  19485  symgfixf1  19495  symgtrinv  19530  pmtrdifellem3  19536  mndodcongi  19601  odmod  19604  odf1  19620  odf1o1  19630  gexdvds  19642  sylow1lem1  19656  pgpssslw  19672  lsmub1  19715  lsmub2  19716  cntzrecd  19736  pj1ghm  19761  lsmhash  19763  efgred  19806  frgpup1  19833  ablsubadd23  19871  ablsubsub23  19882  mulgnn0di  19883  torsubg  19912  zaddablx  19930  gsumzaddlem  19979  gsumzadd  19980  gsumconst  19992  gsumzmhm  19995  telgsumfzslem  20046  dprdfadd  20080  dprd2dlem1  20101  ablsimpgfindlem1  20167  srgbinomlem3  20298  srgbinomlem4  20299  srgbinomlem  20300  gsummgp0  20387  gsumdixp  20388  xpsring1d  20403  unitnegcl  20467  isrnghm  20511  rnghmco  20527  dfrhm2  20544  rhmco  20571  c0rhm  20607  c0rnghm  20608  rhmimasubrng  20639  cntzsubrng  20640  issubrg3  20673  resrhm  20674  rhmeql  20676  rhmima  20677  isdomn4  20788  imadrhmcl  20866  fldsdrgfld  20867  abvres  20900  suborng  20945  lmodfopne  20987  lspf  21061  lspcl  21063  0lmhm  21127  lmhmco  21130  lmhmeql  21142  islmim  21149  rngqiprngghm  21398  rngqiprnglin  21401  xrsdsreval  21519  xrsdsreclb  21521  xrs1cmn  21549  xrge0omnd  21552  znfld  21667  znchr  21669  znunithash  21671  znrrg  21672  freshmansdream  21681  cnmsgnsubg  21684  zrhpsgnmhm  21691  evpmodpmf1o  21703  psgndiflemB  21707  psgndif  21709  phlssphl  21766  frlmval  21855  uvcfval  21891  frlmsslsp  21903  frlmup2  21906  lindfmm  21934  lmimlbs  21943  islindf4  21945  issubassa3  21973  psrbaglesupp  22029  psrcom  22074  resspsrmul  22082  mplsubrglem  22110  mplcoe3  22146  ltbval  22151  ltbwe  22152  evlslem4  22184  evlslem3  22188  psdmvr  22289  psropprmul  22354  coe1tmmul  22395  cply1mul  22413  gsummoncoe1  22425  lply1binomsc  22428  pf1ind  22472  mamufacex  22510  grpvlinv  22512  grpvrinv  22513  eqmat  22538  mat1dimcrng  22591  dmatcrng  22616  scmatf1  22645  m1detdiag  22711  mdetdiaglem  22712  mdet1  22715  mdetunilem9  22734  madulid  22759  gsummatr01lem4  22772  gsummatr01  22773  mat2pmatlin  22849  m2pmfzgsumcl  22862  monmatcollpw  22893  pmatcollpw3lem  22897  mp2pm2mplem4  22923  chpscmatgsummon  22959  chfacfscmulfsupp  22973  chfacfpmmulfsupp  22977  cayhamlem1  22980  cpmadugsumlemF  22990  clsval2  23164  innei  23239  ordtrest  23316  ordtrestixx  23336  isnrm2  23472  lpcls  23478  tgcmp  23515  cmpcld  23516  uncmp  23517  hauscmplem  23520  hauscmp  23521  1stcfb  23559  1stcrest  23567  kgencmp2  23660  1stckgenlem  23667  kgen2ss  23669  kgencn  23670  kgencn3  23672  txval  23678  txuni2  23679  txbasex  23680  txbas  23681  txtop  23683  ptbasin  23691  txtopon  23705  txcld  23717  txss12  23719  txbasval  23720  xkoccn  23733  txcnp  23734  ptcnplem  23735  upxp  23737  txcnmpt  23738  uptx  23739  txrest  23745  txdis  23746  txindislem  23747  txlly  23750  txnlly  23751  txcmp  23757  hausdiag  23759  txhaus  23761  tx1stc  23764  tx2ndc  23765  txkgen  23766  xkoptsub  23768  cnmpt21  23785  txconn  23803  qtopval  23809  hmeoco  23886  txhmeo  23917  xpstopnlem1  23923  fbun  23954  filss  23967  infil  23977  fbunfip  23983  filuni  23999  fmfnfmlem4  24071  ufldom  24076  flffval  24103  flfval  24104  txflf  24120  fcfval  24147  alexsubALTlem3  24163  tgpmulg  24207  subgtgp  24219  qustgplem  24235  tsmsfbas  24242  tsmsres  24258  tsmsmhm  24260  tsmsadd  24261  isxmet2d  24441  blin2  24543  comet  24627  met2ndci  24636  metcn  24657  txmetcn  24662  dscopn  24687  nrmmetd  24688  isngp3  24712  tngval  24753  nm1  24781  subrgnrg  24787  nrginvrcn  24806  rlmnvc  24817  nmo0  24849  nmoco  24851  nghmco  24852  nmotri  24853  0nghm  24855  isnmhm2  24866  0nmhm  24869  nmhmco  24870  nmhmplusg  24871  qtopbaslem  24872  remetdval  24903  bl2ioo  24906  reperflem  24933  iccntr  24936  icccmplem2  24938  icccmp  24940  reconnlem2  24942  xrge0gsumle  24948  xrge0tsms  24949  divcn  24984  cncfmet  25025  iccpnfcnv  25060  bndth  25074  copco  25134  pcopt  25138  pcopt2  25139  nmhmcn  25236  cmodscexp  25237  cphassr  25328  lmmbrf  25378  lmnn  25379  iscauf  25396  caucfil  25399  iscmet3lem1  25407  iscmet3lem2  25408  iscmet3  25409  cfilres  25412  caussi  25413  caubl  25424  caublcls  25425  bcthlem2  25441  bcthlem5  25444  cmsss  25467  lssbn  25468  ovolfioo  25583  ovollb2lem  25604  ovolunlem1a  25612  ovoliunlem1  25618  ovoliunlem2  25619  ovoliunlem3  25620  ovoliun2  25622  ovolscalem1  25629  ovolicc2lem1  25633  ovolicc2lem4  25636  ovolicc2lem5  25637  inmbl  25658  voliunlem1  25666  volsup  25672  ioombl1lem4  25677  iccvolcl  25683  ioovolcl  25686  uniioovol  25695  uniioombllem3a  25700  uniioombllem3  25701  uniioombllem4  25702  uniioombllem5  25703  uniioombllem6  25704  dyadf  25707  dyadovol  25709  dyadss  25710  dyadmbl  25716  opnmbllem  25717  volsup2  25721  volcn  25722  ismbf  25744  mbfima  25746  ismbf3d  25770  mbfadd  25777  mbfsub  25778  mbflimsup  25782  itg1mulc  25820  itg1sub  25825  itg1climres  25830  mbfi1fseqlem1  25831  mbfi1fseqlem3  25833  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfmul  25842  itg2const2  25857  itg2seq  25858  itg2uba  25859  itg2lea  25860  itg2eqa  25861  itg2splitlem  25864  itg2split  25865  itg2monolem1  25866  itg2i1fseqle  25870  itg2i1fseq  25871  itg2i1fseq2  25872  itg2addlem  25874  itg2cnlem1  25877  bddmulibl  25955  ellimc3  25995  dvaddbr  26054  dvcobr  26062  dvcjbr  26065  dvcnvlem  26092  c1lip1  26113  lhop  26132  dvfsumle  26137  dvfsumabs  26139  dvfsumrlimf  26141  dvfsumlem1  26142  dvfsumlem2  26143  dvfsumlem3  26144  dvfsumlem4  26145  dvfsum2  26150  tdeglem4  26174  deg1ge  26212  coe1mul3  26213  fta1g  26284  plyco0  26306  plyf  26312  ply1termlem  26317  plyeq0lem  26324  plypf1  26326  plymullem1  26328  plyaddlem  26329  plymullem  26330  coeeulem  26338  coeidlem  26351  plyco  26355  dgreq  26358  coefv0  26362  coeaddlem  26363  coemullem  26364  coemulhi  26368  coemulc  26369  plycn  26375  dgrlt  26380  dgrsub  26386  plycjlem  26390  plycj  26391  plycjOLD  26393  plyrecj  26395  plymul0or  26396  plyreres  26401  dvply1  26402  vieta1lem2  26429  plyexmo  26431  elqaalem2  26438  elqaalem3  26439  aareccl  26444  aalioulem1  26450  aalioulem3  26452  aaliou  26456  geolim3  26457  ulmcaulem  26511  ulmcau  26512  mtest  26521  dvradcnv  26538  psercn2  26540  pserdvlem2  26545  pserdv2  26547  abelthlem6  26553  abelthlem8  26556  abelthlem9  26557  reeff1o  26564  reefgim  26567  sinperlem  26599  sincosq2sgn  26618  sincosq3sgn  26619  sinq12ge0  26627  sincos6thpi  26635  sineq0  26643  cosord  26650  cos11  26652  sinord  26653  tanord1  26656  eff1olem  26667  logrnaddcl  26693  relogeftb  26703  relogoprlem  26710  logleb  26722  advlogexp  26774  logtayllem  26778  logtayl  26779  logtaylsum  26780  logtayl2  26781  recxpcl  26794  rpcxpcl  26795  cxple3  26820  cxpcom  26858  cxpcn3  26867  cxpeq  26876  relogbmul  26896  relogbcxp  26904  relogbf  26910  atanord  27046  atantayl  27056  birthdaylem2  27071  birthdaylem3  27072  cxp2limlem  27094  fsumharmonic  27130  zetacvg  27133  ftalem1  27191  ftalem4  27194  ftalem5  27195  basellem2  27200  basellem3  27201  basellem4  27202  vmappw  27234  sqf11  27257  mumul  27299  fsumdvdscom  27303  dvdsppwf1o  27304  dvdsflf1o  27305  musum  27309  muinv  27311  fsumdvdsmul  27313  1sgmprm  27317  vmalelog  27323  chtublem  27329  fsumvma  27331  vmasum  27334  logfac2  27335  chpval2  27336  logfaclbnd  27340  logexprlim  27343  mersenne  27345  dchrmulcl  27367  dchrinvcl  27371  dchrfi  27373  dchrghm  27374  dchrptlem1  27382  dchrsum2  27386  dchrsum  27387  pcbcctr  27394  bcmono  27395  bposlem1  27402  bposlem2  27403  bposlem3  27404  bposlem5  27406  bposlem6  27407  bposlem7  27408  lgslem3  27417  lgscllem  27422  lgsval4a  27437  lgsneg  27439  lgsdir2  27448  lgsdir  27450  lgsdilem2  27451  lgsdi  27452  lgsne0  27453  gausslemma2dlem1a  27483  gausslemma2dlem3  27486  gausslemma2dlem6  27490  lgseisenlem3  27495  lgseisenlem4  27496  lgsquadlem1  27498  lgsquadlem2  27499  lgsquad2  27504  lgsquad3  27505  2lgslem1a1  27507  2lgslem1a  27509  2lgslem1c  27511  2sqlem2  27536  mul2sq  27537  2sqlem7  27542  2sqreultlem  27565  2sqreunnltlem  27568  2sqreunnltblem  27569  chebbnd1lem1  27587  vmadivsum  27600  rplogsumlem2  27603  dchrisum0lem1a  27604  rpvmasumlem  27605  dchrisumlem1  27607  dchrisumlem2  27608  dchrisumlem3  27609  dchrmusumlema  27611  dchrmusum2  27612  dchrvmasumlem1  27613  dchrvmasum2lem  27614  dchrvmasum2if  27615  dchrvmasumlem2  27616  dchrvmasumlem3  27617  dchrvmasumiflem1  27619  dchrvmasumiflem2  27620  dchrisum0ff  27625  dchrisum0flblem1  27626  dchrisum0fno1  27629  rpvmasum2  27630  dchrisum0re  27631  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0lem3  27637  mudivsum  27648  mulogsum  27650  mulog2sumlem1  27652  mulog2sumlem2  27653  mulog2sumlem3  27654  selberglem2  27664  selberg2  27669  chpdifbndlem1  27671  selberg3lem1  27675  pntrsumbnd2  27685  selbergr  27686  pntpbnd1  27704  pntpbnd2  27705  pntlemh  27717  pntlemj  27721  pntlemi  27722  pntlemf  27723  pntlemp  27728  ostth2lem1  27736  ostth1  27751  ostth2lem3  27753  ostth3  27756  noreson  27778  nosepon  27783  noextendseq  27785  nosupbnd1lem5  27830  noetasuplem4  27854  addscom  28113  negsdi  28197  onles  28415  addonbday  28426  om2noseqlt  28446  om2noseqf1o  28448  n0s0suc  28489  nnsge1  28490  n0bday  28499  n0fincut  28502  n0ltsp1le  28512  bdayn0sf1o  28517  zaddscl  28541  elzn0s  28545  zsoring  28556  zseo  28569  bdayfinbndlem1  28614  z12subscl  28626  remulscllem2  28648  istrkg2ld  28683  isismt  28757  eedimeq  29153  eqeefv  29158  brbtwn2  29160  colinearalglem1  29161  colinearalglem2  29162  colinearalg  29165  eleesub  29166  eleesubd  29167  axcgrrflx  29169  axcgrid  29171  axsegconlem2  29173  axsegconlem7  29178  axsegconlem9  29180  axsegconlem10  29181  axlowdimlem14  29210  axlowdimlem16  29212  axlowdimlem17  29213  axcontlem2  29220  axcontlem4  29222  axcontlem8  29226  axcontlem10  29228  structiedg0val  29277  upgr1eop  29370  numedglnl  29399  usgredg2v  29482  ushgredgedg  29484  ushgredgedgloop  29486  uspgr1eop  29502  usgr1eop  29505  uhgrissubgr  29530  umgrres1lem  29565  upgrres1  29568  nbuhgr  29598  edgnbusgreu  29622  nb3gr2nb  29639  uvtxnm1nbgr  29659  cusgrexilem2  29697  finsumvtxdg2ssteplem4  29803  vtxdgoddnumeven  29808  wlkeq  29888  uspgr2wlkeq  29900  wlksoneq1eq2  29917  upgrwlkdvdelem  29990  usgr2wlkspthlem1  30011  usgrn2cycl  30063  crctcshwlkn0lem3  30066  crctcshwlkn0lem6  30069  crctcshwlkn0lem7  30070  crctcshwlkn0  30075  wspthneq1eq2  30114  wwlkseq  30145  wwlksnext  30147  rusgrnumwlkg  30234  clwwlkccatlem  30245  clwwlkccat  30246  clwlkclwwlklem2a4  30253  clwlkclwwlklem2  30256  clwlkclwwlkf1lem3  30262  clwwisshclwwslemlem  30269  clwwisshclwws  30271  erclwwlkeqlen  30275  erclwwlkref  30276  clwwnisshclwwsn  30315  clwwlknccat  30319  erclwwlkneqlen  30324  hashecclwwlkn1  30333  umgrhashecclwwlk  30334  clwlksndivn  30342  uhgr3cyclex  30438  eucrctshift  30499  eucrct2eupth  30501  frgreu  30524  frgr3v  30531  3vfriswmgr  30534  frgrncvvdeqlem3  30557  frgrregorufrg  30582  numclwwlk1lem2f1  30613  numclwwlk1lem2fo  30614  numclwlk1lem2  30626  numclwwlk3  30641  numclwwlk6  30646  frgrreg  30650  frgrregord013  30651  nsnlplig  30738  nsnlpligALT  30739  ablodivdiv4  30811  imsdval  30943  nmcvcn  30952  sspval  30980  lnoadd  31015  lnosub  31016  nmooge0  31024  nmoolb  31028  nmoub3i  31030  blocnilem  31061  blocni  31062  cncph  31076  ipasslem1  31088  ipasslem2  31089  ipasslem4  31091  ipasslem11  31097  ipblnfi  31112  phoeqi  31114  ubthlem1  31127  ubthlem3  31129  htthlem  31174  hvsub4  31294  his7  31347  his2sub2  31350  hial2eq2  31364  hhip  31434  hhph  31435  bcs2  31439  hhssabloi  31519  hhssnv  31521  ocorth  31548  shsel  31571  shsel3  31572  shscli  31574  chsupss  31599  shjval  31608  chjval  31609  shjcl  31613  chjcl  31614  shsleji  31627  chslej  31755  chsscon2  31759  chjcom  31763  chub1  31764  chdmj1  31786  spanunsni  31836  spanpr  31837  fh1  31875  fh2  31876  cm2j  31877  spansncvi  31909  5oalem1  31911  5oalem3  31913  5oalem5  31915  3oalem2  31920  pjcompi  31929  pjds3i  31970  hoeq  32017  hoadddi  32060  hoadddir  32061  hosubdi  32065  hosub4  32070  hoeq1  32087  hoeq2  32088  adjval2  32148  counop  32178  adjeq  32192  brafnmul  32208  lnopsubi  32231  hmops  32277  hmopm  32278  hmopd  32279  hmopco  32280  nmcopexi  32284  lnconi  32290  lnfnsubi  32303  nmcfnexi  32308  imaelshi  32315  nlelshi  32317  riesz3i  32319  riesz1  32322  cnlnadjlem2  32325  cnlnadjlem6  32329  adjbdln  32340  adjlnop  32343  adjmul  32349  adjadd  32350  nmopcoi  32352  rnbra  32364  cnvbramul  32372  kbass2  32374  kbass4  32376  kbass5  32377  kbass6  32378  leopadd  32389  leopmul2i  32392  leoptri  32393  dmdmd  32557  mddmd  32558  cvdmd  32594  superpos  32611  chrelati  32621  atcv0eq  32636  atomli  32639  atcvatlem  32642  atcvati  32643  atcvat2i  32644  chirredlem4  32650  atcvat3i  32653  atcvat4i  32654  mdsymlem2  32661  mdsymlem3  32662  mdsymlem5  32664  mdsymlem8  32667  dmdsym  32670  cdjreui  32689  cdj1i  32690  cdj3lem2b  32694  cdj3lem3  32695  cdj3lem3b  32697  cdj3i  32698  brabgaf  32859  prct  32966  fcobijfs  32974  fzsplit3  33046  bcm1n  33048  dpfrac1  33119  wrdres  33163  xrge0mulgnn0  33243  xrge0tsmsd  33301  cycpmco2  33361  isarchiofld  33427  resvval  33559  nsgqusf1olem2  33634  esplyfvaln  33876  lbslsat  33918  ply1degltdimlem  33924  ply1degltdim  33925  ordtrestNEW  34223  mhmhmeotmd  34229  xrge0iifcnv  34235  xrge0iifiso  34237  xrge0pluscn  34242  hasheuni  34387  sxval  34492  measvuni  34516  ddemeas  34538  br2base  34571  dya2iocucvr  34586  sxbrsigalem2  34588  sxbrsiga  34592  omssubadd  34602  eulerpartlemgc  34664  ballotlemfc0  34795  ballotlemfcc  34796  signstfvc  34873  signstres  34874  signsvfn  34881  bnj563  35044  bnj554  35199  bnj557  35201  bnj570  35205  bnj594  35212  bnj849  35225  bnj970  35247  bnj1118  35284  bnj1145  35293  bnj1190  35308  bnj1398  35334  bnj1417  35341  r1omfi  35408  zltp1ne  35467  nnltp1ne  35468  nn0ltp1ne  35469  0nn0m1nnn0  35470  cusgr3cyclex  35494  derangsn  35528  derangen  35530  subfacp1lem5  35542  erdsze2lem1  35561  txpconn  35590  txsconn  35599  cvmliftphtlem  35675  satfdm  35727  satfun  35769  ex-sategoelel  35779  mrsubff1  35872  msubff  35888  msubff1  35914  msubvrs  35918  inffz  36088  bcprod  36096  bccolsum  36097  faclim  36104  dfon2lem4  36142  colineardim1  36419  btwnconn1lem4  36448  btwnconn1lem5  36449  btwnconn1lem6  36450  btwnconn1lem8  36452  btwnconn1lem9  36453  btwnconn1lem12  36456  btwnconn1lem13  36457  btwnconn1lem14  36458  outsideofeu  36489  funray  36498  lineintmo  36515  fwddifnp1  36523  hfun  36536  nmulprop  36548  nn0prpw  36691  opnregcld  36698  cldregopn  36699  ivthALT  36703  onsucconni  36805  mh-inf3f1  36909  bj-nnfim1  37223  bj-nnfim2  37224  bj-nnfbd0  37230  bj-2uplex  37514  bj-unexg  37530  bj-prexg  37531  bj-idres  37659  isbasisrelowllem1  37856  isbasisrelowllem2  37857  icoreclin  37858  relowlssretop  37864  exrecfnlem  37880  pibt2  37918  unccur  38109  phpreu  38110  finixpnum  38111  ltflcei  38114  cos2h  38117  lindsadd  38119  lindsdom  38120  lindsenlbs  38121  matunitlindflem1  38122  matunitlindflem2  38123  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem13  38139  poimirlem14  38140  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem24  38150  poimirlem26  38152  poimirlem27  38153  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  poimirlem32  38158  heicant  38161  opnmbllem0  38162  mblfinlem1  38163  mblfinlem2  38164  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  ovoliunnfl  38168  mbfresfi  38172  itg2addnclem  38177  itg2addnc  38180  itg2gt0cn  38181  ftc1cnnc  38198  ftc1anclem3  38201  ftc1anclem5  38203  ftc1anclem6  38204  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  ftc2nc  38208  indexa  38239  incsequz  38254  incsequz2  38255  geomcau  38265  sstotbnd2  38280  prdsbnd  38299  prdstotbnd  38300  prdsbnd2  38301  cntotbnd  38302  ismtyhmeolem  38310  ismtybndlem  38312  heibor1lem  38315  heiborlem3  38319  heiborlem6  38322  heibor  38327  bfplem1  38328  bfplem2  38329  elghomlem1OLD  38391  rngogrphom  38477  prnc  38573  ispridlc  38576  pridlc3  38579  mpobi123f  38668  mptbi12f  38672  antisymressn  39040  eqvreltr  39197  ax12indalem  39576  lsateln0  39626  atlatmstc  39950  hlatjidm  40000  llnneat  40145  lplnneat  40176  lplnnelln  40177  lvolneatN  40219  lvolnelln  40220  lvolnelpln  40221  dalem23  40327  snatpsubN  40381  linepsubN  40383  pmapsub  40399  pmapglbx  40400  paddasslem14  40464  polsubN  40538  pol1N  40541  2polvalN  40545  2polssN  40546  3polN  40547  2pmaplubN  40557  polatN  40562  2polatN  40563  pnonsingN  40564  polsubclN  40583  lautco  40728  cdlemefrs29cpre1  41029  dian0  41670  dia0eldmN  41671  dia1eldmN  41672  dia0  41683  dia1N  41684  dvhopaddN  41745  dib0  41795  dih0  41911  dih1  41917  dihglblem5apreN  41922  dihatexv2  41970  dochfN  41987  lcmineqlem1  42653  lcmineqlem17  42669  xppss12  42855  sumcubes  42929  dvdsexpnn  42949  remul01  43023  resubeqsub  43046  ricdrng1  43153  prjspeclsp  43201  ismrcd2  43287  nacsfix  43300  mzpaddmpt  43329  mzpmulmpt  43330  eq0rabdioph  43364  lerabdioph  43389  ltrabdioph  43392  nerabdioph  43393  dvdsrabdioph  43394  fiphp3d  43403  congneg  43553  jm2.22  43579  jm2.23  43580  jm2.15nn0  43587  jm3.1  43604  aomclem8  43645  lsmfgcl  43658  lmhmfgima  43668  lnmepi  43669  dgrsub2  43719  mpaaeu  43734  mendring  43772  proot1ex  43780  unielss  43802  onsucwordi  43872  oaabsb  43878  rp-oelim2  43892  nnoeomeqom  43896  cantnfresb  43908  oawordex2  43910  omcl3g  43918  ordsssucb  43919  tfsconcatrev  43932  onsucunipr  43956  onsucunitp  43957  oaun3lem1  43958  naddgeoa  43978  oaltom  43988  minregex2  44118  sssymdifcl  44155  relexp01min  44296  ntrclsiso  44650  ntrclsk3  44653  cvgdvgrat  44882  nznngen  44885  uzmptshftfval  44915  addrval  45033  subrval  45034  mulvval  45035  elpwgded  45132  eel2131  45281  eel3132  45282  el12  45293  sspwimp  45485  sspwimpcf  45487  suctrALTcf  45489  suctrALT3  45491  relpfrlem  45521  hashnnm  45589  cnfex  45607  disjinfi  45769  infxrbnd2  45943  supminfxr  46037  climinf  46181  lptre2pt  46213  limcresiooub  46215  limcresioolb  46216  addlimc  46221  limclner  46224  limsuppnflem  46283  limsupmnfuzlem  46299  limsupvaluz2  46311  limsupresxr  46339  liminfresxr  46340  cnrefiisplem  46402  cncfdmsn  46463  iblspltprt  46546  itgspltprt  46552  dirkertrigeqlem3  46673  fourierdlem62  46741  fourierdlem80  46759  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem114  46793  sge0f1o  46955  hoidmvlelem2  47169  pimdecfgtioo  47290  smfliminflem  47403  fnresfnco  47634  fcores  47660  dfatcolem  47848  nn0resubcl  47901  zgeltp1eq  47902  eluzge0nn0  47905  fz0addcom  47910  elfzlble  47913  fzopredsuc  47917  subsubelfzo0  47920  ceilbi  47930  flmrecm1  47936  minusmod5ne  47948  submodlt  47949  mod0mul  47955  m1modmmod  47957  muldvdsfacm1  47980  uniimafveqt  47986  fundcmpsurinjimaid  48016  icceuelpartlem  48040  iccpartnel  48043  elsprel  48080  nprmmul2  48133  nprmmul3  48134  fmtnodvds  48152  goldbachth  48155  fmtnoprmfac2  48175  prmdvdsfmtnof1  48195  2pwp1prm  48197  flsqrt  48201  lighneallem4  48218  dfodd6  48258  divgcdoddALTV  48303  opoeALTV  48304  opeoALTV  48305  omoeALTV  48306  omeoALTV  48307  epoo  48324  emoo  48325  epee  48326  emee  48327  evensumeven  48328  even3prm2  48340  mogoldbblem  48341  fpprmod  48348  dfwppr  48359  fpprwppr  48360  fpprwpprb  48361  gbepos  48379  gbegt5  48382  gbowgt5  48383  gboge9  48385  sbgoldbst  48399  nnsum3primesgbe  48413  bgoldbtbndlem1  48426  bgoldbtbndlem2  48427  bgoldbtbndlem3  48428  grimco  48510  isuspgrim0  48515  isuspgrimlem  48516  uhgrimisgrgriclem  48551  uhgrimisgrgric  48552  clnbgrgrim  48555  grimedg  48556  isgrtri  48564  cycl3grtri  48568  isubgr3stgrlem6  48592  isubgr3stgrlem7  48593  isubgr3stgrlem8  48594  uspgrlimlem2  48610  uspgrlimlem3  48611  uspgrlimlem4  48612  grlictr  48636  gpgusgralem  48677  gpgedg2ov  48687  gpgnbgrvtx0  48695  gpgnbgrvtx1  48696  gpg5nbgrvtx03star  48701  gpg5nbgr3star  48702  gpg5grlic  48715  2zrngmmgm  48873  2zrngnmrid  48877  2zrngnmlid2  48878  altgsumbc  48984  altgsumbcALT  48985  zlmodzxzadd  48990  zlmodzxzsub  48992  invginvrid  48999  ply1mulgsumlem2  49019  ply1mulgsum  49022  lincvalpr  49050  lindslinindimp2lem1  49090  ldepsprlem  49104  ldepspr  49105  lincresunit3lem3  49106  lincresunitlem1  49107  lincresunit3lem1  49111  lincresunit3  49113  elfzolborelfzop1  49151  zgtp1leeq  49153  flsubz  49154  nneom  49159  nn0ofldiv2  49164  rege1logbrege0  49190  nnpw2pb  49219  dignn0fr  49233  dignn0ldlem  49234  dignnld  49235  dignn0flhalflem1  49247  nn0sumshdiglemB  49252  nn0mulfsum  49256  rrx2plordisom  49355  ehl2eudis0lt  49358  itsclinecirc0in  49407  2itscp  49413  inlinecirc02plem  49418  mof0ALT  49470  i0oii  49550  resccat  49704