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  mp3an3an  1469  ax13  2380  nfeqf  2386  eqeqan12dALT  2759  sylan9eq  2797  sylan9ss  3997  ssconb  4142  ineqan12d  4222  ifpr  4693  disjtp2  4716  dfopg  4871  disjxiun  5140  breqan12d  5159  eusv1  5391  opelvvg  5726  opthprc  5749  relop  5861  dmpropg  6235  unixp  6302  tz7.7  6410  ordin  6414  onin  6415  ontri1  6418  onfr  6423  onelpss  6424  onsseleq  6425  ontr2  6431  onunel  6489  onun2  6492  funssres  6610  funtpg  6621  funtp  6623  resasplit  6778  fodmrnu  6828  f1un  6868  dffv2  7004  fvreseq0  7058  fvcofneq  7113  funopdmsn  7170  fprg  7175  fprb  7214  fconst2g  7223  isofrlem  7360  oveqan12d  7450  ov3  7596  ovg  7598  ovima0  7612  f1opw2  7688  off  7715  unexgOLD  7769  pwuncl  7790  epweon  7795  epweonALT  7796  sucexeloni  7829  ordunpr  7846  omun  7909  peano4  7914  fabexg  7960  f1oabexg  7964  fiun  7967  offres  8008  el2mpocsbcl  8110  curry1  8129  curry1val  8130  curry2  8132  curry2val  8134  soxp  8154  wexp  8155  xpord2pred  8170  poxp3  8175  poseq  8183  soseq  8184  suppfnss  8214  frrlem4  8314  frrlem11  8321  frrlem12  8322  fprlem1  8325  iunon  8379  onfununi  8381  tfrlem11  8428  tz7.48lem  8481  seqomeq12  8494  oacan  8586  oawordri  8588  oaass  8599  omord2  8605  omcan  8607  oen0  8624  oeordi  8625  oeord  8626  oecan  8627  oeworde  8631  oeordsuc  8632  oelimcl  8638  nnawordi  8659  nnaword  8665  nnmord  8670  oaabslem  8685  omabslem  8688  omsmo  8696  eldifsucnn  8702  naddcllem  8714  naddov2  8717  ertr  8760  erex  8769  brecop  8850  ecopovtrn  8860  ecovdi  8865  mapvalg  8876  pmvalg  8877  pmss12g  8909  elmapresaun  8920  boxcutc  8981  undom  9099  sbthlem7  9129  sbth  9133  sdomnsym  9138  sdomdomtr  9150  xpf1o  9179  xpen  9180  limenpsi  9192  pssnn  9208  pwssfi  9217  sbthfi  9239  php2  9248  php3  9249  phpeqd  9252  nndomog  9253  phplem4OLD  9257  phpOLD  9259  php3OLD  9261  nndomogOLD  9263  onomeneq  9265  1sdomOLD  9285  ominfOLD  9295  isinf  9296  isinfOLD  9297  fineqvlem  9298  f1finf1o  9305  en1eqsnOLD  9309  dif1ennnALT  9311  findcard3  9318  findcard3OLD  9319  unblem2  9329  isfinite2  9334  unfilem1  9343  unfi2  9348  fodomfir  9368  unifi2  9385  f1opwfi  9396  fsuppxpfi  9425  fsuppunbi  9429  fsuppco2  9443  fsuppcor  9444  fival  9452  fiin  9462  ordiso  9556  ordtypelem10  9567  hartogslem1  9582  wofib  9585  brwdom3  9622  unwdomg  9624  xpwdomg  9625  sucprcreg  9641  preleqALT  9657  inf3lem6  9673  oemapval  9723  cantnf  9733  wemapwe  9737  cnfcom  9740  ttrcltr  9756  dfttrcl2  9764  frmin  9789  r111  9815  r1ord3g  9819  prwf  9851  r1pw  9885  rankprb  9891  rankxplim  9919  tcrank  9924  updjud  9974  finnum  9988  xpnum  9991  carduni  10021  nnsdomel  10030  fidomtri  10033  pr2nelemOLD  10043  infxpenlem  10053  fseqdom  10066  onssnum  10080  acndom2  10094  alephinit  10135  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem6  10196  undjudom  10208  endjudisj  10209  djuen  10210  djucomen  10218  pwdjuen  10222  djudom1  10223  djuxpdom  10226  djufi  10227  cardadju  10235  nnadju  10238  nnadjuALT  10239  ficardadju  10240  ficardun  10241  ficardun2  10242  pwsdompw  10243  unctb  10244  ackbij2lem1  10258  ackbij1lem6  10264  ackbij1lem16  10274  ackbij1b  10278  ackbij2  10282  coflim  10301  cflim2  10303  cofsmo  10309  coftr  10313  sornom  10317  infpssrlem5  10347  fin4en1  10349  fin23lem23  10366  fin23lem28  10380  isf32lem2  10394  isf32lem4  10396  isf32lem7  10399  isf34lem7  10419  isf34lem6  10420  fin67  10435  isfin7-2  10436  fin1a2lem9  10448  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  zorn2lem6  10541  ttukeylem3  10551  brdom6disj  10572  carddom  10594  cardsdom  10595  domtri  10596  konigthlem  10608  iunctb  10614  alephadd  10617  alephmul  10618  pwcfsdom  10623  cfpwsdom  10624  fpwwe2lem12  10682  canthp1lem2  10693  pwfseqlem3  10700  pwfseqlem4a  10701  inar1  10815  tskcard  10821  tskuni  10823  grur1  10860  mulclpi  10933  addcompi  10934  mulcompi  10936  distrpi  10938  ltexpi  10942  ltapi  10943  ltmpi  10944  enqbreq2  10960  nqereu  10969  addpipq  10977  addpqnq  10978  mulpipq  10980  mulpqnq  10981  addpqf  10984  addclnq  10985  mulpqf  10986  mulclnq  10987  adderpq  10996  mulerpq  10997  ltsonq  11009  lterpq  11010  ltbtwnnq  11018  ltrnq  11019  genpv  11039  genpdm  11042  genpnnp  11045  mulclprlem  11059  distrlem1pr  11065  distrlem4pr  11066  prlem934  11073  addcanpr  11086  suplem1pr  11092  mulcmpblnr  11111  mulclsr  11124  mulasssr  11130  distrsr  11131  ltsosr  11134  1idsr  11138  00sr  11139  recexsrlem  11143  mulgt0sr  11145  addcnsr  11175  axmulf  11186  axmulass  11197  axdistr  11198  axcnre  11204  mulrid  11259  axltadd  11334  lenlt  11339  dedekind  11424  dedekindle  11425  resubcl  11573  subeqrev  11685  muladd  11695  mulsub  11706  mulsub2  11707  ltaddsub2  11738  leaddsub2  11740  leltadd  11747  ltaddpos2  11754  posdif  11756  addge02  11774  mullt0  11782  ltord1  11789  leord1  11790  eqord1  11791  recextlem1  11893  recex  11895  divmuldiv  11967  conjmul  11984  div2sub  12092  prodgt02  12115  lemul2  12120  lemul2a  12122  ltmulgt12  12128  lemulge12  12131  mulge0b  12138  mulle0b  12139  ltmuldiv2  12142  ltdivmul2  12145  lt2mul2div  12146  ledivmul2  12147  lemuldiv2  12149  ledivdiv  12157  lediv2  12158  ltdiv23  12159  lediv23  12160  supmul  12240  riotaneg  12247  negiso  12248  cju  12262  nnaddcl  12289  nnmulcl  12290  nnmtmip  12292  nnsub  12310  addltmul  12502  avgle1  12506  avgle2  12507  avgle  12508  nnrecl  12524  nn0nnaddcl  12557  nn0sub  12576  elz2  12631  zaddcl  12657  zsubcl  12659  znnsub  12663  znn0sub  12664  nzadd  12665  zmulcl  12666  zltp1le  12667  zleltp1  12668  nnleltp1  12673  nnltp1le  12674  nnaddm1cl  12675  nn0ltp1le  12676  nn0leltp1  12677  nn0ltlem1  12678  nn0lem1lt  12683  nnlem1lt  12684  nnltlem1  12685  zdiv  12688  zextle  12691  zextlt  12692  btwnnz  12694  prime  12699  nneo  12702  peano2uz2  12706  uzind  12710  fzind  12716  zriotaneg  12731  uzneg  12898  uztric  12902  uz11  12903  eluzp1m1  12904  eluzp1p1  12906  uzin  12918  uzwo  12953  indstr  12958  uz2mulcl  12968  supminf  12977  uzsupss  12982  zmax  12987  rebtwnz  12989  qre  12995  qaddcl  13007  qsubcl  13010  irradd  13015  elpqb  13018  rpnnen1lem5  13023  cnref1o  13027  rpaddcl  13057  rpmulcl  13058  rpmtmip  13059  rpdivcl  13060  max1  13227  max2  13229  min1  13231  min2  13232  z2ge  13240  qbtwnxr  13242  xaddf  13266  rexadd  13274  rexsub  13275  xnn0xaddcl  13277  xaddcom  13282  xnn0xadd0  13289  xnegdi  13290  rexmul  13313  supxrbnd2  13364  ixxin  13404  elicc2  13452  difreicc  13524  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzval2  13550  elfz1eq  13575  peano2fzr  13577  fzn  13580  fzsplit2  13589  fzaddel  13598  fzadd2  13599  fzsubel  13600  fzrev2  13628  fzrev3  13630  uzsplit  13636  fznuz  13649  uznfz  13650  fzrevral  13652  fzrevral3  13654  fzshftral  13655  elfz2nn0  13658  fznn0sub2  13675  fz0fzdiffz0  13677  elfzmlbp  13679  difelfzle  13681  difelfznle  13682  elfzouz2  13714  fzo0n  13721  fzouzsplit  13734  fzoun  13736  elfzo0le  13743  fzonmapblen  13748  fzofzim  13749  fzoaddel2  13759  eluzgtdifelfzo  13766  elfzodifsumelfzo  13770  ssfzoulel  13799  ubmelm1fzo  13802  fzofzp1b  13804  elfzonelfzo  13808  elfznelfzo  13811  fzostep1  13822  injresinjlem  13826  subfzo0  13828  flflp1  13847  divfl0  13864  flzadd  13866  flmulnn0  13867  fldivnn0le  13872  fldiv  13900  uzsup  13903  mulmod0  13917  modlt  13920  modmulnn  13929  zmodcl  13931  zmodfz  13933  zmodid2  13939  modcyc  13946  muladdmodid  13951  modmuladdnn0  13956  negmod  13957  addmodidr  13961  modadd2mod  13962  modaddmodup  13975  modaddmulmod  13979  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  om2uzlti  13991  om2uzf1oi  13994  fzen2  14010  ssnn0fi  14026  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub0  14034  seqshft2  14069  seqsplit  14076  seqcaopr2  14079  seqf1olem2  14083  expcllem  14113  expcl2lem  14114  1exp  14132  expge1  14140  expadd  14145  expmul  14148  expsub  14151  nn0sq11  14172  lt2sq  14173  le2sq  14174  expmordi  14207  leexp2  14211  leexp1a  14215  sumsqeq0  14218  bernneq  14268  bernneq2  14269  expnbnd  14271  digit2  14275  digit1  14276  facdiv  14326  facwordi  14328  faclbnd  14329  faclbnd3  14331  faclbnd4lem4  14335  faclbnd5  14337  faclbnd6  14338  facavg  14340  bcrpcl  14347  bccmpl  14348  bcval5  14357  hashen  14386  hasheqf1oi  14390  hashgadd  14416  hashdom  14418  hashsdom  14420  hashun  14421  hashunsnggt  14433  hashprg  14434  hashssdif  14451  hashxplem  14472  seqcoll  14503  tpf1o  14540  eqwrd  14595  ccatfval  14611  ccatlen  14613  ccat0  14614  elfzelfzccat  14618  ccatsymb  14620  ccatval21sw  14623  ccatrn  14627  lswccatn0lsw  14629  ccatalpha  14631  ccatrcl1  14632  ccats1alpha  14657  swrdnd  14692  swrdfv2  14699  swrdsbslen  14702  swrdspsleq  14703  swrdccat2  14707  pfxnd0  14726  addlenrevpfx  14728  pfxeq  14734  ccatpfx  14739  pfxccat1  14740  swrdswrdlem  14742  pfxswrd  14744  pfxccatin12lem4  14764  pfxccatin12lem1  14766  pfxccatin12lem2  14769  pfxccatin12lem3  14770  pfxccatin12  14771  pfxccat3  14772  swrdccat  14773  pfxccatpfx2  14775  pfxccat3a  14776  swrdccat3blem  14777  swrdccat3b  14778  revccat  14804  revrev  14805  cshwlen  14837  cshwidxmod  14841  cshwidxmodr  14842  cshweqdif2  14857  cshweqrep  14859  2cshwcshw  14864  s3eq3seq  14978  cotr2g  15015  trclun  15053  shftf  15118  seqshft  15124  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  15356  absdifle  15357  abssuble0  15367  absmax  15368  abs2difabs  15373  fzomaxdif  15382  rexanuz  15384  rexuz3  15387  rexuzre  15391  caubnd2  15396  limsupgre  15517  limsupbnd2  15519  climconst2  15584  lo1resb  15600  o1resb  15602  2clim  15608  climshftlem  15610  climshft  15612  climshft2  15618  cjcn2  15636  o1of2  15649  o1rlimmul  15655  climaddc1  15671  climmulc2  15673  climsubc1  15674  climsubc2  15675  lo1le  15688  climlec2  15695  isershft  15700  isercolllem1  15701  isercolllem3  15703  isercoll  15704  isercoll2  15705  climsup  15706  caurcvg  15713  caucvg  15715  iseraltlem1  15718  iseraltlem2  15719  iseralt  15721  summolem2a  15751  isumclim3  15795  mptfzshft  15814  fsumrev  15815  fsum0diag2  15819  fsumconst  15826  telfsumo2  15839  fsumparts  15842  o1fsum  15849  cvgcmp  15852  cvgcmpub  15853  cvgcmpce  15854  binomlem  15865  binom1p  15867  binom1dif  15869  bcxmas  15871  incexclem  15872  incexc  15873  incexc2  15874  isumshft  15875  isumsplit  15876  isumsup2  15882  climcndslem1  15885  climcndslem2  15886  climcnds  15887  supcvg  15892  expcnv  15900  geoserg  15902  pwdif  15904  geolim  15906  geoisum1  15915  geoisum1c  15916  cvgrat  15919  mertenslem1  15920  mertenslem2  15921  mertens  15922  ntrivcvgfvn0  15935  ntrivcvgmullem  15937  prodmolem2a  15970  prodmo  15972  fprodf1o  15982  fproddiv  15997  fprodeq0  16011  risefacval2  16046  fallfacval2  16047  fallfacval3  16048  rprisefaccl  16059  risefallfac  16060  fallfacfwd  16072  binomfallfaclem1  16075  binomfallfaclem2  16076  binomrisefac  16078  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  efcj  16128  fprodefsum  16131  efexp  16137  eftlub  16145  effsumlt  16147  efle  16154  reef11  16155  efieq  16199  sinsub  16204  cossub  16205  subsin  16207  sinmul  16208  cosmul  16209  addcos  16210  subcos  16211  rpnnen2lem10  16259  rpnnen2lem12  16261  ruclem8  16273  ruclem12  16277  sqrt2irr  16285  dvdssub2  16338  dvdsadd  16339  dvdsaddr  16340  dvdssub  16341  dvdssubr  16342  dvdsle  16347  alzdvds  16357  fzocongeq  16361  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  pwp1fsum  16428  divalglem4  16433  divalglem9  16438  divalgb  16441  divalgmod  16443  ndvdsadd  16447  smueqlem  16527  gcdaddm  16562  modgcd  16569  bezoutlem1  16576  dvdsgcd  16581  absmulgcd  16586  rpmulgcd  16594  rprpwr  16596  sqgcd  16599  dvdssqlem  16603  dvdssq  16604  nn0seqcvgd  16607  algrf  16610  algcvg  16613  lcmcllem  16633  lcmabs  16642  lcmgcd  16644  lcmdvds  16645  lcmgcdnn  16648  lcmf  16670  coprmgcdb  16686  coprmdvds  16690  coprmdvds2  16691  qredeq  16694  isprm3  16720  nprm  16725  oddprmgt2  16736  isprm5  16744  isprm7  16745  divgcdodd  16747  prmdvdsexp  16752  zgcdsq  16790  hashdvds  16812  phiprmpw  16813  crth  16815  phimullem  16816  modprm0  16843  coprimeprodsq  16846  coprimeprodsq2  16847  pythagtriplem2  16855  pythagtriplem19  16871  iserodd  16873  pcpremul  16881  pcmul  16889  pcexp  16897  pcdvdsb  16907  pcneg  16912  pc2dvds  16917  pc11  16918  pcmpt  16930  fldivp1  16935  pcfac  16937  infpnlem1  16948  prmunb  16952  prmreclem1  16954  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  1arithlem4  16964  1arith  16965  gzaddcl  16975  gzmulcl  16976  gzreim  16977  gzsubcl  16978  4sqlem1  16986  4sqlem4a  16989  4sqlem4  16990  4sqlem12  16994  ramlb  17057  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  prmgaplem7  17095  prmgaplem8  17096  prmgapprmolem  17099  cshwshashlem2  17134  setsvalg  17203  ressval  17277  ressval3d  17292  restval  17471  pwsval  17531  xpsval  17615  ssclem  17863  rescval  17871  funcestrcsetclem9  18193  embedsetcestrclem  18202  lubel  18559  ipodrsima  18586  tsrss  18634  resmgmhm  18724  resmgmhm2  18725  mgmhmco  18727  submnd0  18776  mndinvmod  18777  xpsmnd0  18791  resmhm  18833  resmhm2  18834  mhmco  18836  frmdplusg  18867  frmdmnd  18872  efmndcl  18895  smndex1id  18924  mgm2nsgrplem1  18931  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2nmndlem1  18936  sgrp2rid2  18939  dfgrp3  19057  mhmmnd  19082  mulgnngsum  19097  mulgnnsubcl  19104  mulgnn0z  19119  mulgnndir  19121  mulgmodid  19131  eqgfval  19194  cycsubgcl  19224  cycsubg2  19228  0ghm  19248  resghm  19250  resghm2  19251  ghmco  19254  ghmeql  19257  isgim  19280  gicsubgen  19297  cntzmhm  19359  symgcl  19402  symgextf1  19439  gsmsymgrfixlem1  19445  symgfixf1  19455  symgtrinv  19490  pmtrdifellem3  19496  mndodcongi  19561  odmod  19564  odf1  19580  odf1o1  19590  gexdvds  19602  sylow1lem1  19616  pgpssslw  19632  lsmub1  19675  lsmub2  19676  cntzrecd  19696  pj1ghm  19721  lsmhash  19723  efgred  19766  frgpup1  19793  ablsubadd23  19831  ablsubsub23  19842  mulgnn0di  19843  torsubg  19872  zaddablx  19890  gsumzaddlem  19939  gsumzadd  19940  gsumconst  19952  gsumzmhm  19955  telgsumfzslem  20006  dprdfadd  20040  dprd2dlem1  20061  ablsimpgfindlem1  20127  srgbinomlem3  20225  srgbinomlem4  20226  srgbinomlem  20227  gsummgp0  20315  gsumdixp  20316  xpsring1d  20330  unitnegcl  20397  isrnghm  20441  rnghmco  20457  dfrhm2  20474  rhmco  20501  c0rhm  20534  c0rnghm  20535  rhmimasubrng  20566  cntzsubrng  20567  issubrg3  20600  resrhm  20601  rhmeql  20603  rhmima  20604  isdomn4  20716  imadrhmcl  20798  fldsdrgfld  20799  abvres  20832  lmodfopne  20898  lspf  20972  lspcl  20974  0lmhm  21039  lmhmco  21042  lmhmeql  21054  islmim  21061  rngqiprngghm  21309  rngqiprnglin  21312  xrs1cmn  21424  xrsdsreval  21429  xrsdsreclb  21431  znfld  21579  znchr  21581  znunithash  21583  znrrg  21584  freshmansdream  21593  cnmsgnsubg  21595  zrhpsgnmhm  21602  evpmodpmf1o  21614  psgndiflemB  21618  psgndif  21620  phlssphl  21677  frlmval  21768  uvcfval  21804  frlmsslsp  21816  frlmup2  21819  lindfmm  21847  lmimlbs  21856  islindf4  21858  issubassa3  21886  psrbaglesupp  21942  psrcom  21988  resspsrmul  21996  mplsubrglem  22024  mplcoe3  22056  ltbval  22061  ltbwe  22062  evlslem4  22100  evlslem3  22104  psdmvr  22173  psropprmul  22239  coe1tmmul  22280  cply1mul  22300  gsummoncoe1  22312  lply1binomsc  22315  pf1ind  22359  mamufacex  22400  grpvlinv  22402  grpvrinv  22403  eqmat  22430  mat1dimcrng  22483  dmatcrng  22508  scmatf1  22537  m1detdiag  22603  mdetdiaglem  22604  mdet1  22607  mdetunilem9  22626  madulid  22651  gsummatr01lem4  22664  gsummatr01  22665  mat2pmatlin  22741  m2pmfzgsumcl  22754  monmatcollpw  22785  pmatcollpw3lem  22789  mp2pm2mplem4  22815  chpscmatgsummon  22851  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  cayhamlem1  22872  cpmadugsumlemF  22882  clsval2  23058  innei  23133  ordtrest  23210  ordtrestixx  23230  isnrm2  23366  lpcls  23372  tgcmp  23409  cmpcld  23410  uncmp  23411  hauscmplem  23414  hauscmp  23415  1stcfb  23453  1stcrest  23461  kgencmp2  23554  1stckgenlem  23561  kgen2ss  23563  kgencn  23564  kgencn3  23566  txval  23572  txuni2  23573  txbasex  23574  txbas  23575  txtop  23577  ptbasin  23585  txtopon  23599  txcld  23611  txss12  23613  txbasval  23614  xkoccn  23627  txcnp  23628  ptcnplem  23629  upxp  23631  txcnmpt  23632  uptx  23633  txrest  23639  txdis  23640  txindislem  23641  txlly  23644  txnlly  23645  txcmp  23651  hausdiag  23653  txhaus  23655  tx1stc  23658  tx2ndc  23659  txkgen  23660  xkoptsub  23662  cnmpt21  23679  txconn  23697  qtopval  23703  hmeoco  23780  txhmeo  23811  xpstopnlem1  23817  fbun  23848  filss  23861  infil  23871  fbunfip  23877  filuni  23893  fmfnfmlem4  23965  ufldom  23970  flffval  23997  flfval  23998  txflf  24014  fcfval  24041  alexsubALTlem3  24057  tgpmulg  24101  subgtgp  24113  qustgplem  24129  tsmsfbas  24136  tsmsres  24152  tsmsmhm  24154  tsmsadd  24155  isxmet2d  24337  blin2  24439  comet  24526  met2ndci  24535  metcn  24556  txmetcn  24561  dscopn  24586  nrmmetd  24587  isngp3  24611  tngval  24652  nm1  24688  subrgnrg  24694  nrginvrcn  24713  rlmnvc  24724  nmo0  24756  nmoco  24758  nghmco  24759  nmotri  24760  0nghm  24762  isnmhm2  24773  0nmhm  24776  nmhmco  24777  nmhmplusg  24778  qtopbaslem  24779  remetdval  24810  bl2ioo  24813  reperflem  24840  iccntr  24843  icccmplem2  24845  icccmp  24847  reconnlem2  24849  xrge0gsumle  24855  xrge0tsms  24856  divcnOLD  24890  divcn  24892  cncfmet  24935  iccpnfcnv  24975  bndth  24990  copco  25051  pcopt  25055  pcopt2  25056  nmhmcn  25153  cmodscexp  25154  cphassr  25246  lmmbrf  25296  lmnn  25297  iscauf  25314  caucfil  25317  iscmet3lem1  25325  iscmet3lem2  25326  iscmet3  25327  cfilres  25330  caussi  25331  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem5  25362  cmsss  25385  lssbn  25386  ovolfioo  25502  ovollb2lem  25523  ovolunlem1a  25531  ovoliunlem1  25537  ovoliunlem2  25538  ovoliunlem3  25539  ovoliun2  25541  ovolscalem1  25548  ovolicc2lem1  25552  ovolicc2lem4  25555  ovolicc2lem5  25556  inmbl  25577  voliunlem1  25585  volsup  25591  ioombl1lem4  25596  iccvolcl  25602  ioovolcl  25605  uniioovol  25614  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  dyadf  25626  dyadovol  25628  dyadss  25629  dyadmbl  25635  opnmbllem  25636  volsup2  25640  volcn  25641  ismbf  25663  mbfima  25665  ismbf3d  25689  mbfadd  25696  mbfsub  25697  mbflimsup  25701  itg1mulc  25739  itg1sub  25744  itg1climres  25749  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfmul  25761  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2lea  25779  itg2eqa  25780  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  itg2cnlem1  25796  bddmulibl  25874  ellimc3  25914  dvaddbr  25974  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvcnvlem  26014  c1lip1  26036  lhop  26055  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumrlimf  26065  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  tdeglem4  26099  deg1ge  26137  coe1mul3  26138  fta1g  26209  plyco0  26231  plyf  26237  ply1termlem  26242  plyeq0lem  26249  plypf1  26251  plymullem1  26253  plyaddlem  26254  plymullem  26255  coeeulem  26263  coeidlem  26276  plyco  26280  dgreq  26283  coefv0  26287  coeaddlem  26288  coemullem  26289  coemulhi  26293  coemulc  26294  plycn  26300  plycnOLD  26301  dgrlt  26306  dgrsub  26312  plycjlem  26316  plycj  26317  plycjOLD  26319  plyrecj  26321  plymul0or  26322  plyreres  26324  dvply1  26325  vieta1lem2  26353  plyexmo  26355  elqaalem2  26362  elqaalem3  26363  aareccl  26368  aalioulem1  26374  aalioulem3  26376  aaliou  26380  geolim3  26381  ulmcaulem  26437  ulmcau  26438  mtest  26447  dvradcnv  26464  psercn2  26466  psercn2OLD  26467  pserdvlem2  26472  pserdv2  26474  abelthlem6  26480  abelthlem8  26483  abelthlem9  26484  reeff1o  26491  reefgim  26494  sinperlem  26522  sincosq2sgn  26541  sincosq3sgn  26542  sinq12ge0  26550  sincos6thpi  26558  sineq0  26566  cosord  26573  cos11  26575  sinord  26576  tanord1  26579  eff1olem  26590  logrnaddcl  26616  relogeftb  26626  relogoprlem  26633  logleb  26645  advlogexp  26697  logtayllem  26701  logtayl  26702  logtaylsum  26703  logtayl2  26704  recxpcl  26717  rpcxpcl  26718  cxple3  26743  cxpcom  26781  cxpcn3  26791  cxpeq  26800  relogbmul  26820  relogbcxp  26828  relogbf  26834  atanord  26970  atantayl  26980  birthdaylem2  26995  birthdaylem3  26996  cxp2limlem  27019  fsumharmonic  27055  zetacvg  27058  ftalem1  27116  ftalem4  27119  ftalem5  27120  basellem2  27125  basellem3  27126  basellem4  27127  vmappw  27159  sqf11  27182  mumul  27224  fsumdvdscom  27228  dvdsppwf1o  27229  dvdsflf1o  27230  musum  27234  muinv  27236  fsumdvdsmul  27238  1sgmprm  27243  vmalelog  27249  chtublem  27255  fsumvma  27257  vmasum  27260  logfac2  27261  chpval2  27262  logfaclbnd  27266  logexprlim  27269  mersenne  27271  dchrmulcl  27293  dchrinvcl  27297  dchrfi  27299  dchrghm  27300  dchrptlem1  27308  dchrsum2  27312  dchrsum  27313  pcbcctr  27320  bcmono  27321  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem5  27332  bposlem6  27333  bposlem7  27334  lgslem3  27343  lgscllem  27348  lgsval4a  27363  lgsneg  27365  lgsdir2  27374  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  gausslemma2dlem6  27416  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2  27430  lgsquad3  27431  2lgslem1a1  27433  2lgslem1a  27435  2lgslem1c  27437  2sqlem2  27462  mul2sq  27463  2sqlem7  27468  2sqreultlem  27491  2sqreunnltlem  27494  2sqreunnltblem  27495  chebbnd1lem1  27513  vmadivsum  27526  rplogsumlem2  27529  dchrisum0lem1a  27530  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  dchrisum0ff  27551  dchrisum0flblem1  27552  dchrisum0fno1  27555  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  mudivsum  27574  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  selberglem2  27590  selberg2  27595  chpdifbndlem1  27597  selberg3lem1  27601  pntrsumbnd2  27611  selbergr  27612  pntpbnd1  27630  pntpbnd2  27631  pntlemh  27643  pntlemj  27647  pntlemi  27648  pntlemf  27649  pntlemp  27654  ostth2lem1  27662  ostth1  27677  ostth2lem3  27679  ostth3  27682  noreson  27705  nosepon  27710  noextendseq  27712  nosupbnd1lem5  27757  noetasuplem4  27781  addscom  27999  negsdi  28082  om2noseqlt  28305  om2noseqf1o  28307  n0s0suc  28345  nnsge1  28346  n0sbday  28354  zaddscl  28380  elzn0s  28384  zseo  28406  pw2bday  28418  remulscllem2  28433  istrkg2ld  28468  isismt  28542  eedimeq  28913  eqeefv  28918  brbtwn2  28920  colinearalglem1  28921  colinearalglem2  28922  colinearalg  28925  eleesub  28926  eleesubd  28927  axcgrrflx  28929  axcgrid  28931  axsegconlem2  28933  axsegconlem7  28938  axsegconlem9  28940  axsegconlem10  28941  axlowdimlem14  28970  axlowdimlem16  28972  axlowdimlem17  28973  axcontlem2  28980  axcontlem4  28982  axcontlem8  28986  axcontlem10  28988  structiedg0val  29039  upgr1eop  29132  numedglnl  29161  usgredg2v  29244  ushgredgedg  29246  ushgredgedgloop  29248  uspgr1eop  29264  usgr1eop  29267  uhgrissubgr  29292  umgrres1lem  29327  upgrres1  29330  nbuhgr  29360  edgnbusgreu  29384  nb3gr2nb  29401  uvtxnm1nbgr  29421  cusgrexilem2  29459  finsumvtxdg2ssteplem4  29566  vtxdgoddnumeven  29571  wlkeq  29652  uspgr2wlkeq  29664  wlksoneq1eq2  29682  upgrwlkdvdelem  29756  usgr2wlkspthlem1  29777  usgrn2cycl  29829  crctcshwlkn0lem3  29832  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  crctcshwlkn0  29841  wspthneq1eq2  29880  wwlkseq  29911  wwlksnext  29913  rusgrnumwlkg  29997  clwwlkccatlem  30008  clwwlkccat  30009  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  clwlkclwwlkf1lem3  30025  clwwisshclwwslemlem  30032  clwwisshclwws  30034  erclwwlkeqlen  30038  erclwwlkref  30039  clwwnisshclwwsn  30078  clwwlknccat  30082  erclwwlkneqlen  30087  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwlksndivn  30105  uhgr3cyclex  30201  eucrctshift  30262  eucrct2eupth  30264  frgreu  30287  frgr3v  30294  3vfriswmgr  30297  frgrncvvdeqlem3  30320  frgrregorufrg  30345  numclwwlk1lem2f1  30376  numclwwlk1lem2fo  30377  numclwlk1lem2  30389  numclwwlk3  30404  numclwwlk6  30409  frgrreg  30413  frgrregord013  30414  nsnlplig  30500  nsnlpligALT  30501  ablodivdiv4  30573  imsdval  30705  nmcvcn  30714  sspval  30742  lnoadd  30777  lnosub  30778  nmooge0  30786  nmoolb  30790  nmoub3i  30792  blocnilem  30823  blocni  30824  cncph  30838  ipasslem1  30850  ipasslem2  30851  ipasslem4  30853  ipasslem11  30859  ipblnfi  30874  phoeqi  30876  ubthlem1  30889  ubthlem3  30891  htthlem  30936  hvsub4  31056  his7  31109  his2sub2  31112  hial2eq2  31126  hhip  31196  hhph  31197  bcs2  31201  hhssabloi  31281  hhssnv  31283  ocorth  31310  shsel  31333  shsel3  31334  shscli  31336  chsupss  31361  shjval  31370  chjval  31371  shjcl  31375  chjcl  31376  shsleji  31389  chslej  31517  chsscon2  31521  chjcom  31525  chub1  31526  chdmj1  31548  spanunsni  31598  spanpr  31599  fh1  31637  fh2  31638  cm2j  31639  spansncvi  31671  5oalem1  31673  5oalem3  31675  5oalem5  31677  3oalem2  31682  pjcompi  31691  pjds3i  31732  hoeq  31779  hoadddi  31822  hoadddir  31823  hosubdi  31827  hosub4  31832  hoeq1  31849  hoeq2  31850  adjval2  31910  counop  31940  adjeq  31954  brafnmul  31970  lnopsubi  31993  hmops  32039  hmopm  32040  hmopd  32041  hmopco  32042  nmcopexi  32046  lnconi  32052  lnfnsubi  32065  nmcfnexi  32070  imaelshi  32077  nlelshi  32079  riesz3i  32081  riesz1  32084  cnlnadjlem2  32087  cnlnadjlem6  32091  adjbdln  32102  adjlnop  32105  adjmul  32111  adjadd  32112  nmopcoi  32114  rnbra  32126  cnvbramul  32134  kbass2  32136  kbass4  32138  kbass5  32139  kbass6  32140  leopadd  32151  leopmul2i  32154  leoptri  32155  dmdmd  32319  mddmd  32320  cvdmd  32356  superpos  32373  chrelati  32383  atcv0eq  32398  atomli  32401  atcvatlem  32404  atcvati  32405  atcvat2i  32406  chirredlem4  32412  atcvat3i  32415  atcvat4i  32416  mdsymlem2  32423  mdsymlem3  32424  mdsymlem5  32426  mdsymlem8  32429  dmdsym  32432  cdjreui  32451  cdj1i  32452  cdj3lem2b  32456  cdj3lem3  32457  cdj3lem3b  32459  cdj3i  32460  brabgaf  32620  prct  32726  fcobijfs  32734  fzsplit3  32795  bcm1n  32797  dpfrac1  32874  wrdres  32919  xrge0mulgnn0  33020  xrge0tsmsd  33065  xrge0omnd  33088  cycpmco2  33153  suborng  33345  isarchiofld  33347  resvval  33353  nsgqusf1olem2  33442  lbslsat  33667  ply1degltdimlem  33673  ply1degltdim  33674  ordtrestNEW  33920  mhmhmeotmd  33926  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0pluscn  33939  hasheuni  34086  sxval  34191  measvuni  34215  ddemeas  34237  br2base  34271  dya2iocucvr  34286  sxbrsigalem2  34288  sxbrsiga  34292  omssubadd  34302  eulerpartlemgc  34364  ballotlemfc0  34495  ballotlemfcc  34496  signstfvc  34589  signstres  34590  signsvfn  34597  bnj563  34757  bnj554  34913  bnj557  34915  bnj570  34919  bnj594  34926  bnj849  34939  bnj970  34961  bnj1118  34998  bnj1145  35007  bnj1190  35022  bnj1398  35048  bnj1417  35055  zltp1ne  35115  nnltp1ne  35116  nn0ltp1ne  35117  0nn0m1nnn0  35118  cusgr3cyclex  35141  derangsn  35175  derangen  35177  subfacp1lem5  35189  erdsze2lem1  35208  txpconn  35237  txsconn  35246  cvmliftphtlem  35322  satfdm  35374  satfun  35416  ex-sategoelel  35426  mrsubff1  35519  msubff  35535  msubff1  35561  msubvrs  35565  inffz  35730  bcprod  35738  bccolsum  35739  faclim  35746  dfon2lem4  35787  colineardim1  36062  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem12  36099  btwnconn1lem13  36100  btwnconn1lem14  36101  outsideofeu  36132  funray  36141  lineintmo  36158  fwddifnp1  36166  hfun  36179  nn0prpw  36324  opnregcld  36331  cldregopn  36332  ivthALT  36336  onsucconni  36438  bj-nnfim1  36745  bj-nnfim2  36746  bj-2uplex  37023  bj-unexg  37039  bj-prexg  37040  bj-idres  37161  isbasisrelowllem1  37356  isbasisrelowllem2  37357  icoreclin  37358  relowlssretop  37364  exrecfnlem  37380  pibt2  37418  unccur  37610  phpreu  37611  finixpnum  37612  ltflcei  37615  cos2h  37618  lindsadd  37620  lindsdom  37621  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  ovoliunnfl  37669  mbfresfi  37673  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  indexa  37740  incsequz  37755  incsequz2  37756  geomcau  37766  sstotbnd2  37781  prdsbnd  37800  prdstotbnd  37801  prdsbnd2  37802  cntotbnd  37803  ismtyhmeolem  37811  ismtybndlem  37813  heibor1lem  37816  heiborlem3  37820  heiborlem6  37823  heibor  37828  bfplem1  37829  bfplem2  37830  elghomlem1OLD  37892  rngogrphom  37978  prnc  38074  ispridlc  38077  pridlc3  38080  mpobi123f  38169  mptbi12f  38173  antisymressn  38445  eqvreltr  38608  ax12indalem  38946  lsateln0  38996  atlatmstc  39320  hlatjidm  39370  llnneat  39516  lplnneat  39547  lplnnelln  39548  lvolneatN  39590  lvolnelln  39591  lvolnelpln  39592  dalem23  39698  snatpsubN  39752  linepsubN  39754  pmapsub  39770  pmapglbx  39771  paddasslem14  39835  polsubN  39909  pol1N  39912  2polvalN  39916  2polssN  39917  3polN  39918  2pmaplubN  39928  polatN  39933  2polatN  39934  pnonsingN  39935  polsubclN  39954  lautco  40099  cdlemefrs29cpre1  40400  dian0  41041  dia0eldmN  41042  dia1eldmN  41043  dia0  41054  dia1N  41055  dvhopaddN  41116  dib0  41166  dih0  41282  dih1  41288  dihglblem5apreN  41293  dihatexv2  41341  dochfN  41358  lcmineqlem1  42030  lcmineqlem17  42046  factwoffsmonot  42243  xppss12  42268  sumcubes  42347  dvdsexpnn  42368  remul01  42437  resubeqsub  42459  ricdrng1  42538  prjspeclsp  42622  ismrcd2  42710  nacsfix  42723  mzpaddmpt  42752  mzpmulmpt  42753  eq0rabdioph  42787  lerabdioph  42816  ltrabdioph  42819  nerabdioph  42820  dvdsrabdioph  42821  fiphp3d  42830  congneg  42981  jm2.22  43007  jm2.23  43008  jm2.15nn0  43015  jm3.1  43032  aomclem8  43073  lsmfgcl  43086  lmhmfgima  43096  lnmepi  43097  dgrsub2  43147  mpaaeu  43162  mendring  43200  proot1ex  43208  unielss  43230  oneltri  43270  onsucwordi  43301  oaabsb  43307  rp-oelim2  43321  nnoeomeqom  43325  cantnfresb  43337  oawordex2  43339  omcl3g  43347  ordsssucb  43348  tfsconcatrev  43361  onsucunipr  43385  onsucunitp  43386  oaun3lem1  43387  naddgeoa  43407  oaltom  43418  minregex2  43548  sssymdifcl  43585  relexp01min  43726  ntrclsiso  44080  ntrclsk3  44083  cvgdvgrat  44332  nznngen  44335  uzmptshftfval  44365  addrval  44485  subrval  44486  mulvval  44487  elpwgded  44584  eel132  44722  eel2131  44734  eel3132  44735  el12  44746  sspwimp  44938  sspwimpcf  44940  suctrALTcf  44942  suctrALT3  44944  relpfrlem  44974  cnfex  45033  disjinfi  45197  infxrbnd2  45380  supminfxr  45475  climinf  45621  lptre2pt  45655  limcresiooub  45657  limcresioolb  45658  addlimc  45663  limclner  45666  limsuppnflem  45725  limsupmnfuzlem  45741  limsupvaluz2  45753  limsupresxr  45781  liminfresxr  45782  cnrefiisplem  45844  cncfdmsn  45905  iblspltprt  45988  itgspltprt  45994  dirkertrigeqlem3  46115  fourierdlem62  46183  fourierdlem80  46201  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0f1o  46397  hoidmvlelem2  46611  pimdecfgtioo  46732  smfliminflem  46845  fnresfnco  47053  fcores  47079  dfatcolem  47267  nn0resubcl  47320  zgeltp1eq  47321  eluzge0nn0  47324  fz0addcom  47329  elfzlble  47332  fzopredsuc  47335  subsubelfzo0  47338  minusmod5ne  47351  submodlt  47352  uniimafveqt  47368  fundcmpsurinjimaid  47398  icceuelpartlem  47422  iccpartnel  47425  elsprel  47462  fmtnodvds  47531  goldbachth  47534  fmtnoprmfac2  47554  prmdvdsfmtnof1  47574  2pwp1prm  47576  flsqrt  47580  lighneallem4  47597  dfodd6  47624  divgcdoddALTV  47669  opoeALTV  47670  opeoALTV  47671  omoeALTV  47672  omeoALTV  47673  epoo  47690  emoo  47691  epee  47692  emee  47693  evensumeven  47694  even3prm2  47706  mogoldbblem  47707  fpprmod  47714  dfwppr  47725  fpprwppr  47726  fpprwpprb  47727  gbepos  47745  gbegt5  47748  gbowgt5  47749  gboge9  47751  sbgoldbst  47765  nnsum3primesgbe  47779  bgoldbtbndlem1  47792  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  isuspgrim0  47872  uspgrimprop  47873  isuspgrimlem  47874  grimco  47880  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrim  47902  grimedg  47903  isgrtri  47910  cycl3grtri  47914  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  isubgr3stgrlem8  47940  uspgrlimlem2  47956  uspgrlimlem3  47957  uspgrlimlem4  47958  grlictr  47975  gpgusgralem  48011  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg5grlic  48047  2zrngmmgm  48168  2zrngnmrid  48172  2zrngnmlid2  48173  altgsumbc  48268  altgsumbcALT  48269  zlmodzxzadd  48274  zlmodzxzsub  48276  invginvrid  48283  ply1mulgsumlem2  48304  ply1mulgsum  48307  lincvalpr  48335  lindslinindimp2lem1  48375  ldepsprlem  48389  ldepspr  48390  lincresunit3lem3  48391  lincresunitlem1  48392  lincresunit3lem1  48396  lincresunit3  48398  elfzolborelfzop1  48436  zgtp1leeq  48438  flsubz  48439  mod0mul  48440  m1modmmod  48442  nneom  48448  nn0ofldiv2  48453  rege1logbrege0  48479  nnpw2pb  48508  dignn0fr  48522  dignn0ldlem  48523  dignnld  48524  dignn0flhalflem1  48536  nn0sumshdiglemB  48541  nn0mulfsum  48545  rrx2plordisom  48644  ehl2eudis0lt  48647  itsclinecirc0in  48696  2itscp  48702  inlinecirc02plem  48707  mof0ALT  48749  i0oii  48817