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  1466  ax13  2377  nfeqf  2383  eqeqan12dALT  2756  sylan9eq  2794  sylan9ss  4008  ssconb  4151  ineqan12d  4229  ifpr  4697  disjtp2  4720  dfopg  4875  disjxiun  5144  breqan12d  5163  eusv1  5396  opelvvg  5729  opthprc  5752  relop  5863  dmpropg  6236  unixp  6303  tz7.7  6411  ordin  6415  onin  6416  ontri1  6419  onfr  6424  onelpss  6425  onsseleq  6426  ontr2  6432  onunel  6490  onun2  6493  funssres  6611  funtpg  6622  funtp  6624  resasplit  6778  fodmrnu  6828  f1un  6868  dffv2  7003  fvreseq0  7057  fvcofneq  7112  funopdmsn  7169  fprg  7174  fprb  7213  fconst2g  7222  isofrlem  7359  oveqan12d  7449  ov3  7595  ovg  7597  ovima0  7611  f1opw2  7687  off  7714  unexgOLD  7767  pwuncl  7788  epweon  7793  epweonALT  7794  sucexeloni  7828  ordunpr  7845  omun  7909  peano4  7914  fabexg  7958  f1oabexg  7962  fiun  7965  offres  8006  el2mpocsbcl  8108  curry1  8127  curry1val  8128  curry2  8130  curry2val  8132  soxp  8152  wexp  8153  xpord2pred  8168  poxp3  8173  poseq  8181  soseq  8182  suppfnss  8212  frrlem4  8312  frrlem11  8319  frrlem12  8320  fprlem1  8323  iunon  8377  onfununi  8379  tfrlem11  8426  tz7.48lem  8479  seqomeq12  8492  oacan  8584  oawordri  8586  oaass  8597  omord2  8603  omcan  8605  oen0  8622  oeordi  8623  oeord  8624  oecan  8625  oeworde  8629  oeordsuc  8630  oelimcl  8636  nnawordi  8657  nnaword  8663  nnmord  8668  oaabslem  8683  omabslem  8686  omsmo  8694  eldifsucnn  8700  naddcllem  8712  naddov2  8715  ertr  8758  erex  8767  brecop  8848  ecopovtrn  8858  ecovdi  8863  mapvalg  8874  pmvalg  8875  pmss12g  8907  elmapresaun  8918  boxcutc  8979  undom  9097  sbthlem7  9127  sbth  9131  sdomnsym  9136  sdomdomtr  9148  xpf1o  9177  xpen  9178  limenpsi  9190  pssnn  9206  sbthfi  9236  php2  9245  php3  9246  phpeqd  9249  nndomog  9250  phplem4OLD  9254  phpOLD  9256  php3OLD  9258  nndomogOLD  9260  onomeneq  9262  1sdomOLD  9282  ominfOLD  9292  isinf  9293  isinfOLD  9294  fineqvlem  9295  f1finf1o  9302  en1eqsnOLD  9306  dif1ennnALT  9308  findcard3  9315  findcard3OLD  9316  unblem2  9326  isfinite2  9331  unfilem1  9340  unfi2  9345  fodomfir  9365  unifi2  9382  f1opwfi  9393  fsuppxpfi  9422  fsuppunbi  9426  fsuppco2  9440  fsuppcor  9441  fival  9449  fiin  9459  ordiso  9553  ordtypelem10  9564  hartogslem1  9579  wofib  9582  brwdom3  9619  unwdomg  9621  xpwdomg  9622  sucprcreg  9638  preleqALT  9654  inf3lem6  9670  oemapval  9720  cantnf  9730  wemapwe  9734  cnfcom  9737  ttrcltr  9753  dfttrcl2  9761  frmin  9786  r111  9812  r1ord3g  9816  prwf  9848  r1pw  9882  rankprb  9888  rankxplim  9916  tcrank  9921  updjud  9971  finnum  9985  xpnum  9988  carduni  10018  nnsdomel  10027  fidomtri  10030  pr2nelemOLD  10040  infxpenlem  10050  fseqdom  10063  onssnum  10077  acndom2  10091  alephinit  10132  dfac5lem4  10163  dfac5lem4OLD  10165  kmlem6  10193  undjudom  10205  endjudisj  10206  djuen  10207  djucomen  10215  pwdjuen  10219  djudom1  10220  djuxpdom  10223  djufi  10224  cardadju  10232  nnadju  10235  nnadjuALT  10236  ficardadju  10237  ficardun  10238  ficardun2  10239  pwsdompw  10240  unctb  10241  ackbij2lem1  10255  ackbij1lem6  10261  ackbij1lem16  10271  ackbij1b  10275  ackbij2  10279  coflim  10298  cflim2  10300  cofsmo  10306  coftr  10310  sornom  10314  infpssrlem5  10344  fin4en1  10346  fin23lem23  10363  fin23lem28  10377  isf32lem2  10391  isf32lem4  10393  isf32lem7  10396  isf34lem7  10416  isf34lem6  10417  fin67  10432  isfin7-2  10433  fin1a2lem9  10445  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  zorn2lem6  10538  ttukeylem3  10548  brdom6disj  10569  carddom  10591  cardsdom  10592  domtri  10593  konigthlem  10605  iunctb  10611  alephadd  10614  alephmul  10615  pwcfsdom  10620  cfpwsdom  10621  fpwwe2lem12  10679  canthp1lem2  10690  pwfseqlem3  10697  pwfseqlem4a  10698  inar1  10812  tskcard  10818  tskuni  10820  grur1  10857  mulclpi  10930  addcompi  10931  mulcompi  10933  distrpi  10935  ltexpi  10939  ltapi  10940  ltmpi  10941  enqbreq2  10957  nqereu  10966  addpipq  10974  addpqnq  10975  mulpipq  10977  mulpqnq  10978  addpqf  10981  addclnq  10982  mulpqf  10983  mulclnq  10984  adderpq  10993  mulerpq  10994  ltsonq  11006  lterpq  11007  ltbtwnnq  11015  ltrnq  11016  genpv  11036  genpdm  11039  genpnnp  11042  mulclprlem  11056  distrlem1pr  11062  distrlem4pr  11063  prlem934  11070  addcanpr  11083  suplem1pr  11089  mulcmpblnr  11108  mulclsr  11121  mulasssr  11127  distrsr  11128  ltsosr  11131  1idsr  11135  00sr  11136  recexsrlem  11140  mulgt0sr  11142  addcnsr  11172  axmulf  11183  axmulass  11194  axdistr  11195  axcnre  11201  mulrid  11256  axltadd  11331  lenlt  11336  dedekind  11421  dedekindle  11422  resubcl  11570  subeqrev  11682  muladd  11692  mulsub  11703  mulsub2  11704  ltaddsub2  11735  leaddsub2  11737  leltadd  11744  ltaddpos2  11751  posdif  11753  addge02  11771  mullt0  11779  ltord1  11786  leord1  11787  eqord1  11788  recextlem1  11890  recex  11892  divmuldiv  11964  conjmul  11981  div2sub  12089  prodgt02  12112  lemul2  12117  lemul2a  12119  ltmulgt12  12125  lemulge12  12128  mulge0b  12135  mulle0b  12136  ltmuldiv2  12139  ltdivmul2  12142  lt2mul2div  12143  ledivmul2  12144  lemuldiv2  12146  ledivdiv  12154  lediv2  12155  ltdiv23  12156  lediv23  12157  supmul  12237  riotaneg  12244  negiso  12245  cju  12259  nnaddcl  12286  nnmulcl  12287  nnmtmip  12289  nnsub  12307  addltmul  12499  avgle1  12503  avgle2  12504  avgle  12505  nnrecl  12521  nn0nnaddcl  12554  nn0sub  12573  elz2  12628  zaddcl  12654  zsubcl  12656  znnsub  12660  znn0sub  12661  nzadd  12662  zmulcl  12663  zltp1le  12664  zleltp1  12665  nnleltp1  12670  nnltp1le  12671  nnaddm1cl  12672  nn0ltp1le  12673  nn0leltp1  12674  nn0ltlem1  12675  nn0lem1lt  12680  nnlem1lt  12681  nnltlem1  12682  zdiv  12685  zextle  12688  zextlt  12689  btwnnz  12691  prime  12696  nneo  12699  peano2uz2  12703  uzind  12707  fzind  12713  zriotaneg  12728  uzneg  12895  uztric  12899  uz11  12900  eluzp1m1  12901  eluzp1p1  12903  uzin  12915  uzwo  12950  indstr  12955  uz2mulcl  12965  supminf  12974  uzsupss  12979  zmax  12984  rebtwnz  12986  qre  12992  qaddcl  13004  qsubcl  13007  irradd  13012  elpqb  13015  rpnnen1lem5  13020  cnref1o  13024  rpaddcl  13054  rpmulcl  13055  rpmtmip  13056  rpdivcl  13057  max1  13223  max2  13225  min1  13227  min2  13228  z2ge  13236  qbtwnxr  13238  xaddf  13262  rexadd  13270  rexsub  13271  xnn0xaddcl  13273  xaddcom  13278  xnn0xadd0  13285  xnegdi  13286  rexmul  13309  supxrbnd2  13360  ixxin  13400  elicc2  13448  difreicc  13520  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  fzval2  13546  elfz1eq  13571  peano2fzr  13573  fzn  13576  fzsplit2  13585  fzaddel  13594  fzadd2  13595  fzsubel  13596  fzrev2  13624  fzrev3  13626  uzsplit  13632  fznuz  13645  uznfz  13646  fzrevral  13648  fzrevral3  13650  fzshftral  13651  elfz2nn0  13654  fznn0sub2  13671  fz0fzdiffz0  13673  elfzmlbp  13675  difelfzle  13677  difelfznle  13678  elfzouz2  13710  fzo0n  13717  fzouzsplit  13730  fzoun  13732  elfzo0le  13739  fzonmapblen  13744  fzofzim  13745  fzoaddel2  13755  eluzgtdifelfzo  13762  elfzodifsumelfzo  13766  ssfzoulel  13795  ubmelm1fzo  13798  fzofzp1b  13800  elfzonelfzo  13804  elfznelfzo  13807  fzostep1  13818  injresinjlem  13822  subfzo0  13824  flflp1  13843  divfl0  13860  flzadd  13862  flmulnn0  13863  fldivnn0le  13868  fldiv  13896  uzsup  13899  mulmod0  13913  modlt  13916  modmulnn  13925  zmodcl  13927  zmodfz  13929  zmodid2  13935  modcyc  13942  muladdmodid  13947  modmuladdnn0  13952  negmod  13953  addmodidr  13957  modadd2mod  13958  modaddmodup  13971  modaddmulmod  13975  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  om2uzlti  13987  om2uzf1oi  13990  fzen2  14006  ssnn0fi  14022  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub0  14030  seqshft2  14065  seqsplit  14072  seqcaopr2  14075  seqf1olem2  14079  expcllem  14109  expcl2lem  14110  1exp  14128  expge1  14136  expadd  14141  expmul  14144  expsub  14147  nn0sq11  14168  lt2sq  14169  le2sq  14170  expmordi  14203  leexp2  14207  leexp1a  14211  sumsqeq0  14214  bernneq  14264  bernneq2  14265  expnbnd  14267  digit2  14271  digit1  14272  facdiv  14322  facwordi  14324  faclbnd  14325  faclbnd3  14327  faclbnd4lem4  14331  faclbnd5  14333  faclbnd6  14334  facavg  14336  bcrpcl  14343  bccmpl  14344  bcval5  14353  hashen  14382  hasheqf1oi  14386  hashgadd  14412  hashdom  14414  hashsdom  14416  hashun  14417  hashunsnggt  14429  hashprg  14430  hashssdif  14447  hashxplem  14468  seqcoll  14499  tpf1o  14536  eqwrd  14591  ccatfval  14607  ccatlen  14609  ccat0  14610  elfzelfzccat  14614  ccatsymb  14616  ccatval21sw  14619  ccatrn  14623  lswccatn0lsw  14625  ccatalpha  14627  ccatrcl1  14628  ccats1alpha  14653  swrdnd  14688  swrdfv2  14695  swrdsbslen  14698  swrdspsleq  14699  swrdccat2  14703  pfxnd0  14722  addlenrevpfx  14724  pfxeq  14730  ccatpfx  14735  pfxccat1  14736  swrdswrdlem  14738  pfxswrd  14740  pfxccatin12lem4  14760  pfxccatin12lem1  14762  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccatin12  14767  pfxccat3  14768  swrdccat  14769  pfxccatpfx2  14771  pfxccat3a  14772  swrdccat3blem  14773  swrdccat3b  14774  revccat  14800  revrev  14801  cshwlen  14833  cshwidxmod  14837  cshwidxmodr  14838  cshweqdif2  14853  cshweqrep  14855  2cshwcshw  14860  s3eq3seq  14974  cotr2g  15011  trclun  15049  shftf  15114  seqshft  15120  crre  15149  crim  15150  readd  15161  resub  15162  remul2  15165  imadd  15169  imsub  15170  immul2  15172  ipcnval  15178  cjsub  15184  cjreim  15195  01sqrexlem6  15282  sqrtle  15295  sqrt11  15297  absreimsq  15327  absreim  15328  absmul  15329  sqabs  15342  absdiflt  15352  absdifle  15353  abssuble0  15363  absmax  15364  abs2difabs  15369  fzomaxdif  15378  rexanuz  15380  rexuz3  15383  rexuzre  15387  caubnd2  15392  limsupgre  15513  limsupbnd2  15515  climconst2  15580  lo1resb  15596  o1resb  15598  2clim  15604  climshftlem  15606  climshft  15608  climshft2  15614  cjcn2  15632  o1of2  15645  o1rlimmul  15651  climaddc1  15667  climmulc2  15669  climsubc1  15670  climsubc2  15671  lo1le  15684  climlec2  15691  isershft  15696  isercolllem1  15697  isercolllem3  15699  isercoll  15700  isercoll2  15701  climsup  15702  caurcvg  15709  caucvg  15711  iseraltlem1  15714  iseraltlem2  15715  iseralt  15717  summolem2a  15747  isumclim3  15791  mptfzshft  15810  fsumrev  15811  fsum0diag2  15815  fsumconst  15822  telfsumo2  15835  fsumparts  15838  o1fsum  15845  cvgcmp  15848  cvgcmpub  15849  cvgcmpce  15850  binomlem  15861  binom1p  15863  binom1dif  15865  bcxmas  15867  incexclem  15868  incexc  15869  incexc2  15870  isumshft  15871  isumsplit  15872  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  supcvg  15888  expcnv  15896  geoserg  15898  pwdif  15900  geolim  15902  geoisum1  15911  geoisum1c  15912  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  mertens  15918  ntrivcvgfvn0  15931  ntrivcvgmullem  15933  prodmolem2a  15966  prodmo  15968  fprodf1o  15978  fproddiv  15993  fprodeq0  16007  risefacval2  16042  fallfacval2  16043  fallfacval3  16044  rprisefaccl  16055  risefallfac  16056  fallfacfwd  16068  binomfallfaclem1  16071  binomfallfaclem2  16072  binomrisefac  16074  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  efcj  16124  fprodefsum  16127  efexp  16133  eftlub  16141  effsumlt  16143  efle  16150  reef11  16151  efieq  16195  sinsub  16200  cossub  16201  subsin  16203  sinmul  16204  cosmul  16205  addcos  16206  subcos  16207  rpnnen2lem10  16255  rpnnen2lem12  16257  ruclem8  16269  ruclem12  16273  sqrt2irr  16281  dvdssub2  16334  dvdsadd  16335  dvdsaddr  16336  dvdssub  16337  dvdssubr  16338  dvdsle  16343  alzdvds  16353  fzocongeq  16357  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  pwp1fsum  16424  divalglem4  16429  divalglem9  16434  divalgb  16437  divalgmod  16439  ndvdsadd  16443  smueqlem  16523  gcdaddm  16558  modgcd  16565  bezoutlem1  16572  dvdsgcd  16577  absmulgcd  16582  rpmulgcd  16590  rprpwr  16592  sqgcd  16595  dvdssqlem  16599  dvdssq  16600  nn0seqcvgd  16603  algrf  16606  algcvg  16609  lcmcllem  16629  lcmabs  16638  lcmgcd  16640  lcmdvds  16641  lcmgcdnn  16644  lcmf  16666  coprmgcdb  16682  coprmdvds  16686  coprmdvds2  16687  qredeq  16690  isprm3  16716  nprm  16721  oddprmgt2  16732  isprm5  16740  isprm7  16741  divgcdodd  16743  prmdvdsexp  16748  zgcdsq  16786  hashdvds  16808  phiprmpw  16809  crth  16811  phimullem  16812  modprm0  16838  coprimeprodsq  16841  coprimeprodsq2  16842  pythagtriplem2  16850  pythagtriplem19  16866  iserodd  16868  pcpremul  16876  pcmul  16884  pcexp  16892  pcdvdsb  16902  pcneg  16907  pc2dvds  16912  pc11  16913  pcmpt  16925  fldivp1  16930  pcfac  16932  infpnlem1  16943  prmunb  16947  prmreclem1  16949  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  1arithlem4  16959  1arith  16960  gzaddcl  16970  gzmulcl  16971  gzreim  16972  gzsubcl  16973  4sqlem1  16981  4sqlem4a  16984  4sqlem4  16985  4sqlem12  16989  ramlb  17052  prmgaplem4  17087  prmgaplem5  17088  prmgaplem6  17089  prmgaplem7  17090  prmgaplem8  17091  prmgapprmolem  17094  cshwshashlem2  17130  setsvalg  17199  ressval  17276  ressval3d  17291  ressval3dOLD  17292  restval  17472  pwsval  17532  xpsval  17616  ssclem  17866  rescval  17874  funcestrcsetclem9  18203  embedsetcestrclem  18212  lubel  18571  ipodrsima  18598  tsrss  18646  resmgmhm  18736  resmgmhm2  18737  mgmhmco  18739  submnd0  18788  mndinvmod  18789  xpsmnd0  18803  resmhm  18845  resmhm2  18846  mhmco  18848  frmdplusg  18879  frmdmnd  18884  efmndcl  18907  smndex1id  18936  mgm2nsgrplem1  18943  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  sgrp2nmndlem1  18948  sgrp2rid2  18951  dfgrp3  19069  mhmmnd  19094  mulgnngsum  19109  mulgnnsubcl  19116  mulgnn0z  19131  mulgnndir  19133  mulgmodid  19143  eqgfval  19206  cycsubgcl  19236  cycsubg2  19240  0ghm  19260  resghm  19262  resghm2  19263  ghmco  19266  ghmeql  19269  isgim  19292  gicsubgen  19309  cntzmhm  19371  symgcl  19416  symgextf1  19453  gsmsymgrfixlem1  19459  symgfixf1  19469  symgtrinv  19504  pmtrdifellem3  19510  mndodcongi  19575  odmod  19578  odf1  19594  odf1o1  19604  gexdvds  19616  sylow1lem1  19630  pgpssslw  19646  lsmub1  19689  lsmub2  19690  cntzrecd  19710  pj1ghm  19735  lsmhash  19737  efgred  19780  frgpup1  19807  ablsubadd23  19845  ablsubsub23  19856  mulgnn0di  19857  torsubg  19886  zaddablx  19904  gsumzaddlem  19953  gsumzadd  19954  gsumconst  19966  gsumzmhm  19969  telgsumfzslem  20020  dprdfadd  20054  dprd2dlem1  20075  ablsimpgfindlem1  20141  srgbinomlem3  20245  srgbinomlem4  20246  srgbinomlem  20247  gsummgp0  20331  gsumdixp  20332  xpsring1d  20346  unitnegcl  20413  isrnghm  20457  rnghmco  20473  dfrhm2  20490  rhmco  20517  c0rhm  20550  c0rnghm  20551  rhmimasubrng  20582  cntzsubrng  20583  issubrg3  20616  resrhm  20617  rhmeql  20619  rhmima  20620  isdomn4  20732  imadrhmcl  20814  fldsdrgfld  20815  abvres  20848  lmodfopne  20914  lspf  20989  lspcl  20991  0lmhm  21056  lmhmco  21059  lmhmeql  21071  islmim  21078  rngqiprngghm  21326  rngqiprnglin  21329  xrs1cmn  21441  xrsdsreval  21446  xrsdsreclb  21448  znfld  21596  znchr  21598  znunithash  21600  znrrg  21601  freshmansdream  21610  cnmsgnsubg  21612  zrhpsgnmhm  21619  evpmodpmf1o  21631  psgndiflemB  21635  psgndif  21637  phlssphl  21694  frlmval  21785  uvcfval  21821  frlmsslsp  21833  frlmup2  21836  lindfmm  21864  lmimlbs  21873  islindf4  21875  issubassa3  21903  psrbaglesupp  21959  psrcom  22005  resspsrmul  22013  mplsubrglem  22041  mplcoe3  22073  ltbval  22078  ltbwe  22079  evlslem4  22117  evlslem3  22121  psropprmul  22254  coe1tmmul  22295  cply1mul  22315  gsummoncoe1  22327  lply1binomsc  22330  pf1ind  22374  mamufacex  22415  grpvlinv  22417  grpvrinv  22418  eqmat  22445  mat1dimcrng  22498  dmatcrng  22523  scmatf1  22552  m1detdiag  22618  mdetdiaglem  22619  mdet1  22622  mdetunilem9  22641  madulid  22666  gsummatr01lem4  22679  gsummatr01  22680  mat2pmatlin  22756  m2pmfzgsumcl  22769  monmatcollpw  22800  pmatcollpw3lem  22804  mp2pm2mplem4  22830  chpscmatgsummon  22866  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  cayhamlem1  22887  cpmadugsumlemF  22897  clsval2  23073  innei  23148  ordtrest  23225  ordtrestixx  23245  isnrm2  23381  lpcls  23387  tgcmp  23424  cmpcld  23425  uncmp  23426  hauscmplem  23429  hauscmp  23430  1stcfb  23468  1stcrest  23476  kgencmp2  23569  1stckgenlem  23576  kgen2ss  23578  kgencn  23579  kgencn3  23581  txval  23587  txuni2  23588  txbasex  23589  txbas  23590  txtop  23592  ptbasin  23600  txtopon  23614  txcld  23626  txss12  23628  txbasval  23629  xkoccn  23642  txcnp  23643  ptcnplem  23644  upxp  23646  txcnmpt  23647  uptx  23648  txrest  23654  txdis  23655  txindislem  23656  txlly  23659  txnlly  23660  txcmp  23666  hausdiag  23668  txhaus  23670  tx1stc  23673  tx2ndc  23674  txkgen  23675  xkoptsub  23677  cnmpt21  23694  txconn  23712  qtopval  23718  hmeoco  23795  txhmeo  23826  xpstopnlem1  23832  fbun  23863  filss  23876  infil  23886  fbunfip  23892  filuni  23908  fmfnfmlem4  23980  ufldom  23985  flffval  24012  flfval  24013  txflf  24029  fcfval  24056  alexsubALTlem3  24072  tgpmulg  24116  subgtgp  24128  qustgplem  24144  tsmsfbas  24151  tsmsres  24167  tsmsmhm  24169  tsmsadd  24170  isxmet2d  24352  blin2  24454  comet  24541  met2ndci  24550  metcn  24571  txmetcn  24576  dscopn  24601  nrmmetd  24602  isngp3  24626  tngval  24667  nm1  24703  subrgnrg  24709  nrginvrcn  24728  rlmnvc  24739  nmo0  24771  nmoco  24773  nghmco  24774  nmotri  24775  0nghm  24777  isnmhm2  24788  0nmhm  24791  nmhmco  24792  nmhmplusg  24793  qtopbaslem  24794  remetdval  24824  bl2ioo  24827  reperflem  24853  iccntr  24856  icccmplem2  24858  icccmp  24860  reconnlem2  24862  xrge0gsumle  24868  xrge0tsms  24869  divcnOLD  24903  divcn  24905  cncfmet  24948  iccpnfcnv  24988  bndth  25003  copco  25064  pcopt  25068  pcopt2  25069  nmhmcn  25166  cmodscexp  25167  cphassr  25259  lmmbrf  25309  lmnn  25310  iscauf  25327  caucfil  25330  iscmet3lem1  25338  iscmet3lem2  25339  iscmet3  25340  cfilres  25343  caussi  25344  caubl  25355  caublcls  25356  bcthlem2  25372  bcthlem5  25375  cmsss  25398  lssbn  25399  ovolfioo  25515  ovollb2lem  25536  ovolunlem1a  25544  ovoliunlem1  25550  ovoliunlem2  25551  ovoliunlem3  25552  ovoliun2  25554  ovolscalem1  25561  ovolicc2lem1  25565  ovolicc2lem4  25568  ovolicc2lem5  25569  inmbl  25590  voliunlem1  25598  volsup  25604  ioombl1lem4  25609  iccvolcl  25615  ioovolcl  25618  uniioovol  25627  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  dyadf  25639  dyadovol  25641  dyadss  25642  dyadmbl  25648  opnmbllem  25649  volsup2  25653  volcn  25654  ismbf  25676  mbfima  25678  ismbf3d  25702  mbfadd  25709  mbfsub  25710  mbflimsup  25714  itg1mulc  25753  itg1sub  25758  itg1climres  25763  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfmul  25775  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2lea  25793  itg2eqa  25794  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  itg2cnlem1  25810  bddmulibl  25888  ellimc3  25928  dvaddbr  25988  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvcnvlem  26028  c1lip1  26050  lhop  26069  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumrlimf  26079  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  tdeglem4  26113  deg1ge  26151  coe1mul3  26152  fta1g  26223  plyco0  26245  plyf  26251  ply1termlem  26256  plyeq0lem  26263  plypf1  26265  plymullem1  26267  plyaddlem  26268  plymullem  26269  coeeulem  26277  coeidlem  26290  plyco  26294  dgreq  26297  coefv0  26301  coeaddlem  26302  coemullem  26303  coemulhi  26307  coemulc  26308  plycn  26314  plycnOLD  26315  dgrlt  26320  dgrsub  26326  plycjlem  26330  plycj  26331  plycjOLD  26333  plyrecj  26335  plymul0or  26336  plyreres  26338  dvply1  26339  vieta1lem2  26367  plyexmo  26369  elqaalem2  26376  elqaalem3  26377  aareccl  26382  aalioulem1  26388  aalioulem3  26390  aaliou  26394  geolim3  26395  ulmcaulem  26451  ulmcau  26452  mtest  26461  dvradcnv  26478  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv2  26488  abelthlem6  26494  abelthlem8  26497  abelthlem9  26498  reeff1o  26505  reefgim  26508  sinperlem  26536  sincosq2sgn  26555  sincosq3sgn  26556  sinq12ge0  26564  sincos6thpi  26572  sineq0  26580  cosord  26587  cos11  26589  sinord  26590  tanord1  26593  eff1olem  26604  logrnaddcl  26630  relogeftb  26640  relogoprlem  26647  logleb  26659  advlogexp  26711  logtayllem  26715  logtayl  26716  logtaylsum  26717  logtayl2  26718  recxpcl  26731  rpcxpcl  26732  cxple3  26757  cxpcom  26795  cxpcn3  26805  cxpeq  26814  relogbmul  26834  relogbcxp  26842  relogbf  26848  atanord  26984  atantayl  26994  birthdaylem2  27009  birthdaylem3  27010  cxp2limlem  27033  fsumharmonic  27069  zetacvg  27072  ftalem1  27130  ftalem4  27133  ftalem5  27134  basellem2  27139  basellem3  27140  basellem4  27141  vmappw  27173  sqf11  27196  mumul  27238  fsumdvdscom  27242  dvdsppwf1o  27243  dvdsflf1o  27244  musum  27248  muinv  27250  fsumdvdsmul  27252  1sgmprm  27257  vmalelog  27263  chtublem  27269  fsumvma  27271  vmasum  27274  logfac2  27275  chpval2  27276  logfaclbnd  27280  logexprlim  27283  mersenne  27285  dchrmulcl  27307  dchrinvcl  27311  dchrfi  27313  dchrghm  27314  dchrptlem1  27322  dchrsum2  27326  dchrsum  27327  pcbcctr  27334  bcmono  27335  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem5  27346  bposlem6  27347  bposlem7  27348  lgslem3  27357  lgscllem  27362  lgsval4a  27377  lgsneg  27379  lgsdir2  27388  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  gausslemma2dlem6  27430  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2  27444  lgsquad3  27445  2lgslem1a1  27447  2lgslem1a  27449  2lgslem1c  27451  2sqlem2  27476  mul2sq  27477  2sqlem7  27482  2sqreultlem  27505  2sqreunnltlem  27508  2sqreunnltblem  27509  chebbnd1lem1  27527  vmadivsum  27540  rplogsumlem2  27543  dchrisum0lem1a  27544  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasum2if  27555  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  dchrisum0ff  27565  dchrisum0flblem1  27566  dchrisum0fno1  27569  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  mudivsum  27588  mulogsum  27590  mulog2sumlem1  27592  mulog2sumlem2  27593  mulog2sumlem3  27594  selberglem2  27604  selberg2  27609  chpdifbndlem1  27611  selberg3lem1  27615  pntrsumbnd2  27625  selbergr  27626  pntpbnd1  27644  pntpbnd2  27645  pntlemh  27657  pntlemj  27661  pntlemi  27662  pntlemf  27663  pntlemp  27668  ostth2lem1  27676  ostth1  27691  ostth2lem3  27693  ostth3  27696  noreson  27719  nosepon  27724  noextendseq  27726  nosupbnd1lem5  27771  noetasuplem4  27795  addscom  28013  negsdi  28096  om2noseqlt  28319  om2noseqf1o  28321  n0s0suc  28359  nnsge1  28360  n0sbday  28368  zaddscl  28394  elzn0s  28398  zseo  28420  pw2bday  28432  remulscllem2  28447  istrkg2ld  28482  isismt  28556  eedimeq  28927  eqeefv  28932  brbtwn2  28934  colinearalglem1  28935  colinearalglem2  28936  colinearalg  28939  eleesub  28940  eleesubd  28941  axcgrrflx  28943  axcgrid  28945  axsegconlem2  28947  axsegconlem7  28952  axsegconlem9  28954  axsegconlem10  28955  axlowdimlem14  28984  axlowdimlem16  28986  axlowdimlem17  28987  axcontlem2  28994  axcontlem4  28996  axcontlem8  29000  axcontlem10  29002  structiedg0val  29053  upgr1eop  29146  numedglnl  29175  usgredg2v  29258  ushgredgedg  29260  ushgredgedgloop  29262  uspgr1eop  29278  usgr1eop  29281  uhgrissubgr  29306  umgrres1lem  29341  upgrres1  29344  nbuhgr  29374  edgnbusgreu  29398  nb3gr2nb  29415  uvtxnm1nbgr  29435  cusgrexilem2  29473  finsumvtxdg2ssteplem4  29580  vtxdgoddnumeven  29585  wlkeq  29666  uspgr2wlkeq  29678  wlksoneq1eq2  29696  upgrwlkdvdelem  29768  usgr2wlkspthlem1  29789  usgrn2cycl  29838  crctcshwlkn0lem3  29841  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  crctcshwlkn0  29850  wspthneq1eq2  29889  wwlkseq  29920  wwlksnext  29922  rusgrnumwlkg  30006  clwwlkccatlem  30017  clwwlkccat  30018  clwlkclwwlklem2a4  30025  clwlkclwwlklem2  30028  clwlkclwwlkf1lem3  30034  clwwisshclwwslemlem  30041  clwwisshclwws  30043  erclwwlkeqlen  30047  erclwwlkref  30048  clwwnisshclwwsn  30087  clwwlknccat  30091  erclwwlkneqlen  30096  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwlksndivn  30114  uhgr3cyclex  30210  eucrctshift  30271  eucrct2eupth  30273  frgreu  30296  frgr3v  30303  3vfriswmgr  30306  frgrncvvdeqlem3  30329  frgrregorufrg  30354  numclwwlk1lem2f1  30385  numclwwlk1lem2fo  30386  numclwlk1lem2  30398  numclwwlk3  30413  numclwwlk6  30418  frgrreg  30422  frgrregord013  30423  nsnlplig  30509  nsnlpligALT  30510  ablodivdiv4  30582  imsdval  30714  nmcvcn  30723  sspval  30751  lnoadd  30786  lnosub  30787  nmooge0  30795  nmoolb  30799  nmoub3i  30801  blocnilem  30832  blocni  30833  cncph  30847  ipasslem1  30859  ipasslem2  30860  ipasslem4  30862  ipasslem11  30868  ipblnfi  30883  phoeqi  30885  ubthlem1  30898  ubthlem3  30900  htthlem  30945  hvsub4  31065  his7  31118  his2sub2  31121  hial2eq2  31135  hhip  31205  hhph  31206  bcs2  31210  hhssabloi  31290  hhssnv  31292  ocorth  31319  shsel  31342  shsel3  31343  shscli  31345  chsupss  31370  shjval  31379  chjval  31380  shjcl  31384  chjcl  31385  shsleji  31398  chslej  31526  chsscon2  31530  chjcom  31534  chub1  31535  chdmj1  31557  spanunsni  31607  spanpr  31608  fh1  31646  fh2  31647  cm2j  31648  spansncvi  31680  5oalem1  31682  5oalem3  31684  5oalem5  31686  3oalem2  31691  pjcompi  31700  pjds3i  31741  hoeq  31788  hoadddi  31831  hoadddir  31832  hosubdi  31836  hosub4  31841  hoeq1  31858  hoeq2  31859  adjval2  31919  counop  31949  adjeq  31963  brafnmul  31979  lnopsubi  32002  hmops  32048  hmopm  32049  hmopd  32050  hmopco  32051  nmcopexi  32055  lnconi  32061  lnfnsubi  32074  nmcfnexi  32079  imaelshi  32086  nlelshi  32088  riesz3i  32090  riesz1  32093  cnlnadjlem2  32096  cnlnadjlem6  32100  adjbdln  32111  adjlnop  32114  adjmul  32120  adjadd  32121  nmopcoi  32123  rnbra  32135  cnvbramul  32143  kbass2  32145  kbass4  32147  kbass5  32148  kbass6  32149  leopadd  32160  leopmul2i  32163  leoptri  32164  dmdmd  32328  mddmd  32329  cvdmd  32365  superpos  32382  chrelati  32392  atcv0eq  32407  atomli  32410  atcvatlem  32413  atcvati  32414  atcvat2i  32415  chirredlem4  32421  atcvat3i  32424  atcvat4i  32425  mdsymlem2  32432  mdsymlem3  32433  mdsymlem5  32435  mdsymlem8  32438  dmdsym  32441  cdjreui  32460  cdj1i  32461  cdj3lem2b  32465  cdj3lem3  32466  cdj3lem3b  32468  cdj3i  32469  brabgaf  32627  prct  32731  fcobijfs  32740  fzsplit3  32801  bcm1n  32802  dpfrac1  32858  wrdres  32903  xrge0mulgnn0  33002  xrge0tsmsd  33047  xrge0omnd  33070  cycpmco2  33135  suborng  33324  isarchiofld  33326  resvval  33332  nsgqusf1olem2  33421  lbslsat  33643  ply1degltdimlem  33649  ply1degltdim  33650  ordtrestNEW  33881  mhmhmeotmd  33887  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0pluscn  33900  hasheuni  34065  sxval  34170  measvuni  34194  ddemeas  34216  br2base  34250  dya2iocucvr  34265  sxbrsigalem2  34267  sxbrsiga  34271  omssubadd  34281  eulerpartlemgc  34343  ballotlemfc0  34473  ballotlemfcc  34474  signstfvc  34567  signstres  34568  signsvfn  34575  bnj563  34735  bnj554  34891  bnj557  34893  bnj570  34897  bnj594  34904  bnj849  34917  bnj970  34939  bnj1118  34976  bnj1145  34985  bnj1190  35000  bnj1398  35026  bnj1417  35033  zltp1ne  35093  nnltp1ne  35094  nn0ltp1ne  35095  0nn0m1nnn0  35096  cusgr3cyclex  35120  derangsn  35154  derangen  35156  subfacp1lem5  35168  erdsze2lem1  35187  txpconn  35216  txsconn  35225  cvmliftphtlem  35301  satfdm  35353  satfun  35395  ex-sategoelel  35405  mrsubff1  35498  msubff  35514  msubff1  35540  msubvrs  35544  inffz  35709  bcprod  35717  bccolsum  35718  faclim  35725  dfon2lem4  35767  colineardim1  36042  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem12  36079  btwnconn1lem13  36080  btwnconn1lem14  36081  outsideofeu  36112  funray  36121  lineintmo  36138  fwddifnp1  36146  hfun  36159  nn0prpw  36305  opnregcld  36312  cldregopn  36313  ivthALT  36317  onsucconni  36419  bj-nnfim1  36726  bj-nnfim2  36727  bj-2uplex  37004  bj-unexg  37020  bj-prexg  37021  bj-idres  37142  isbasisrelowllem1  37337  isbasisrelowllem2  37338  icoreclin  37339  relowlssretop  37345  exrecfnlem  37361  pibt2  37399  unccur  37589  phpreu  37590  finixpnum  37591  ltflcei  37594  cos2h  37597  lindsadd  37599  lindsdom  37600  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  heicant  37641  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  ovoliunnfl  37648  mbfresfi  37652  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  indexa  37719  incsequz  37734  incsequz2  37735  geomcau  37745  sstotbnd2  37760  prdsbnd  37779  prdstotbnd  37780  prdsbnd2  37781  cntotbnd  37782  ismtyhmeolem  37790  ismtybndlem  37792  heibor1lem  37795  heiborlem3  37799  heiborlem6  37802  heibor  37807  bfplem1  37808  bfplem2  37809  elghomlem1OLD  37871  rngogrphom  37957  prnc  38053  ispridlc  38056  pridlc3  38059  mpobi123f  38148  mptbi12f  38152  antisymressn  38425  eqvreltr  38588  ax12indalem  38926  lsateln0  38976  atlatmstc  39300  hlatjidm  39350  llnneat  39496  lplnneat  39527  lplnnelln  39528  lvolneatN  39570  lvolnelln  39571  lvolnelpln  39572  dalem23  39678  snatpsubN  39732  linepsubN  39734  pmapsub  39750  pmapglbx  39751  paddasslem14  39815  polsubN  39889  pol1N  39892  2polvalN  39896  2polssN  39897  3polN  39898  2pmaplubN  39908  polatN  39913  2polatN  39914  pnonsingN  39915  polsubclN  39934  lautco  40079  cdlemefrs29cpre1  40380  dian0  41021  dia0eldmN  41022  dia1eldmN  41023  dia0  41034  dia1N  41035  dvhopaddN  41096  dib0  41146  dih0  41262  dih1  41268  dihglblem5apreN  41273  dihatexv2  41321  dochfN  41338  lcmineqlem1  42010  lcmineqlem17  42026  factwoffsmonot  42223  xppss12  42246  sumcubes  42325  dvdsexpnn  42346  remul01  42413  resubeqsub  42435  ricdrng1  42514  prjspeclsp  42598  ismrcd2  42686  nacsfix  42699  mzpaddmpt  42728  mzpmulmpt  42729  eq0rabdioph  42763  lerabdioph  42792  ltrabdioph  42795  nerabdioph  42796  dvdsrabdioph  42797  fiphp3d  42806  congneg  42957  jm2.22  42983  jm2.23  42984  jm2.15nn0  42991  jm3.1  43008  aomclem8  43049  lsmfgcl  43062  lmhmfgima  43072  lnmepi  43073  dgrsub2  43123  mpaaeu  43138  mendring  43176  proot1ex  43184  unielss  43206  oneltri  43246  onsucwordi  43277  oaabsb  43283  rp-oelim2  43297  nnoeomeqom  43301  cantnfresb  43313  oawordex2  43315  omcl3g  43323  ordsssucb  43324  tfsconcatrev  43337  onsucunipr  43361  onsucunitp  43362  oaun3lem1  43363  naddgeoa  43383  oaltom  43394  minregex2  43524  sssymdifcl  43561  relexp01min  43702  ntrclsiso  44056  ntrclsk3  44059  cvgdvgrat  44308  nznngen  44311  uzmptshftfval  44341  addrval  44461  subrval  44462  mulvval  44463  elpwgded  44561  eel132  44699  eel2131  44711  eel3132  44712  el12  44723  sspwimp  44915  sspwimpcf  44917  suctrALTcf  44919  suctrALT3  44921  cnfex  44965  disjinfi  45134  infxrbnd2  45318  supminfxr  45413  climinf  45561  lptre2pt  45595  limcresiooub  45597  limcresioolb  45598  addlimc  45603  limclner  45606  limsuppnflem  45665  limsupmnfuzlem  45681  limsupvaluz2  45693  limsupresxr  45721  liminfresxr  45722  cnrefiisplem  45784  cncfdmsn  45845  iblspltprt  45928  itgspltprt  45934  dirkertrigeqlem3  46055  fourierdlem62  46123  fourierdlem80  46141  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sge0f1o  46337  hoidmvlelem2  46551  pimdecfgtioo  46672  smfliminflem  46785  fnresfnco  46990  fcores  47016  dfatcolem  47204  nn0resubcl  47257  zgeltp1eq  47258  eluzge0nn0  47261  fz0addcom  47266  elfzlble  47269  fzopredsuc  47272  subsubelfzo0  47275  minusmod5ne  47288  submodlt  47289  uniimafveqt  47305  fundcmpsurinjimaid  47335  icceuelpartlem  47359  iccpartnel  47362  elsprel  47399  fmtnodvds  47468  goldbachth  47471  fmtnoprmfac2  47491  prmdvdsfmtnof1  47511  2pwp1prm  47513  flsqrt  47517  lighneallem4  47534  dfodd6  47561  divgcdoddALTV  47606  opoeALTV  47607  opeoALTV  47608  omoeALTV  47609  omeoALTV  47610  epoo  47627  emoo  47628  epee  47629  emee  47630  evensumeven  47631  even3prm2  47643  mogoldbblem  47644  fpprmod  47651  dfwppr  47662  fpprwppr  47663  fpprwpprb  47664  gbepos  47682  gbegt5  47685  gbowgt5  47686  gboge9  47688  sbgoldbst  47702  nnsum3primesgbe  47716  bgoldbtbndlem1  47729  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  isuspgrim0  47809  uspgrimprop  47810  isuspgrimlem  47811  grimco  47817  uhgrimisgrgriclem  47835  uhgrimisgrgric  47836  clnbgrgrim  47839  grimedg  47840  isgrtri  47847  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  isubgr3stgrlem8  47875  uspgrlimlem2  47891  uspgrlimlem3  47892  uspgrlimlem4  47893  grlictr  47910  gpgusgralem  47945  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  gpg5grlic  47974  2zrngmmgm  48095  2zrngnmrid  48099  2zrngnmlid2  48100  altgsumbc  48196  altgsumbcALT  48197  zlmodzxzadd  48202  zlmodzxzsub  48204  invginvrid  48211  ply1mulgsumlem2  48232  ply1mulgsum  48235  lincvalpr  48263  lindslinindimp2lem1  48303  ldepsprlem  48317  ldepspr  48318  lincresunit3lem3  48319  lincresunitlem1  48320  lincresunit3lem1  48324  lincresunit3  48326  elfzolborelfzop1  48364  zgtp1leeq  48366  flsubz  48367  mod0mul  48368  m1modmmod  48370  nneom  48376  nn0ofldiv2  48381  rege1logbrege0  48407  nnpw2pb  48436  dignn0fr  48450  dignn0ldlem  48451  dignnld  48452  dignn0flhalflem1  48464  nn0sumshdiglemB  48469  nn0mulfsum  48473  rrx2plordisom  48572  ehl2eudis0lt  48575  itsclinecirc0in  48624  2itscp  48630  inlinecirc02plem  48635  mof0ALT  48669  i0oii  48715