Theorem sylanbrc 581

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	⊢ (𝜑 → 𝜓)
sylanbrc.2	⊢ (𝜑 → 𝜒)
sylanbrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanbrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylanbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 510	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 233	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sylanblrc  588  ifpimpda  1079  ecase23d  1471  raleqbidvvOLD  3328  elrabd  3684  eqeu  3701  euind  3719  reuind  3748  eldifd  3958  eqssd  3998  ssrabdv  4070  psstr  4103  elind  4193  elpwdifsn  4791  prproe  4905  propeqop  5506  issod  5620  wereu  5671  wereu2  5672  relssdmrnOLD  6267  predtrss  6322  ordelord  6385  funun  6593  fnsng  6599  fnprg  6606  fntpg  6607  fununi  6622  fncoOLD  6667  f00  6772  f1ss  6792  f1ssr  6793  f1ssres  6794  focofo  6817  f1f1orn  6843  foimacnv  6849  foun  6850  f1oprswap  6876  rescnvimafod  7074  fvn0ssdmfun  7075  dff3  7100  fmpt  7110  fompt  7118  ffnfv  7119  fmpt2d  7124  ffvresb  7125  fprb  7196  fpr2g  7214  nvof1o  7280  fcof1  7287  fcofo  7288  fcof1od  7294  fliftf  7314  soisores  7326  soisoi  7327  isoini2  7338  f1oiso  7350  moriotass  7400  fnoprabg  7533  f1ocnvd  7659  fiun  7931  f1iun  7932  1stcof  8007  2ndcof  8008  1stconst  8088  2ndconst  8089  curry1  8092  curry2  8095  fo2ndf  8109  f1o2ndf1  8110  soxp  8117  wexp  8118  fnwelem  8119  poxp2  8131  frxp2  8132  poxp3  8138  frxp3  8139  suppssov1  8185  suppssfv  8189  fpr1  8290  wfrlem10OLD  8320  smores2  8356  smo11  8366  smoiso2  8371  tfrlem12  8391  tfrlem13  8392  oalimcl  8562  oaf1o  8565  omlimcl  8580  omeu  8587  oeeulem  8603  oeeui  8604  omsmo  8659  cofonr  8675  naddunif  8694  eroveu  8808  fsetfocdm  8857  undifixp  8930  resixpfo  8932  elixpsn  8933  dom2lem  8990  difsnen  9055  omxpenlem  9075  sucdom2OLD  9084  sdomdomtr  9112  domsdomtr  9114  fodomr  9130  xpf1o  9141  ssfi  9175  sdomdomtrfi  9206  domsdomtrfi  9207  sucdom2  9208  php2  9213  php3  9214  phpeqd  9217  php2OLD  9225  php3OLD  9226  phpeqdOLD  9227  1sdom2dom  9249  unxpdomlem3  9254  f1finf1o  9273  f1finf1oOLD  9274  frfi  9290  wofi  9294  nnsdomg  9304  nnsdomgOLD  9305  domunfican  9322  fofinf1o  9329  mapfienlem3  9404  mapfien  9405  marypha1lem  9430  supeu  9451  infeu  9493  ordtypelem2  9516  ordtypelem4  9518  ordtypelem10  9524  oismo  9537  wemaplem2  9544  card2inf  9552  brwdom2  9570  wdom2d  9577  harwdom  9588  cantnfp1lem2  9676  cantnfp1lem3  9677  cantnflem1  9686  cantnflem2  9687  cantnf  9690  cnfcom2lem  9698  cnfcom3lem  9700  ttrcltr  9713  frr1  9756  tskwe  9947  cardsdomelir  9970  cardprclem  9976  cardmin2  9996  en2other2  10006  r0weon  10009  infxpenc  10015  fseqenlem1  10021  fseqenlem2  10022  fodomacn  10053  infpwfien  10059  finnisoeu  10110  iunfictbso  10111  dfac12lem2  10141  cofsmo  10266  cfsmolem  10267  alephsing  10273  sornom  10274  infpssrlem3  10302  infpssrlem5  10304  ssfin4  10307  isfin4p1  10312  fincssdom  10320  fin23lem23  10323  fin23lem28  10337  fin23lem31  10340  fin23lem34  10343  isf32lem9  10358  compssiso  10371  fin1a2lem12  10408  hsmexlem1  10423  hsmexlem4  10426  domtriomlem  10439  cardmin  10561  smobeth  10583  gchen1  10622  gchen2  10623  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  canthnum  10646  canthwe  10648  canthp1lem2  10650  canthp1  10651  pwfseqlem5  10660  gchdjuidm  10665  gchxpidm  10666  gchhar  10676  r1wunlim  10734  inar1  10772  inatsk  10775  r1tskina  10779  gruiun  10796  gruima  10799  gruina  10815  addclpi  10889  mulclpi  10890  nqereu  10926  dmrecnq  10965  genpcl  11005  suplem1pr  11049  receu  11863  recgt0  12064  cju  12212  peano5nni  12219  nn0n0n1ge2  12543  nn0ge2m1nn  12545  nnnegz  12565  elnnz  12572  nnz  12583  msqznn  12648  eluzaddiOLD  12858  eluzsubiOLD  12860  uz2mulcl  12914  elq  12938  nnrp  12989  rpaddcl  13000  rpmulcl  13001  rpdivcl  13003  rpgecl  13006  ge0p1rp  13009  elrpd  13017  nn0rp0  13436  ge0addcl  13441  ge0mulcl  13442  ge0xaddcl  13443  ge0xmulcl  13444  icoshftf1o  13455  xnn0xrge0  13487  peano2fzr  13518  uzsubsubfz  13527  fzsplit2  13530  elfznn  13534  fzss1  13544  fzss2  13545  fzp1elp1  13558  elfz1b  13574  elfz0fzfz0  13610  fz0fzelfz0  13611  difelfznle  13619  elfzofz  13652  prinfzo0  13675  nn0p1elfzo  13679  fzosplitsnm1  13711  ubmelm1fzo  13732  fzofzp1b  13734  elfznelfzo  13741  fzosplitsn  13744  injresinj  13757  flge0nn0  13789  flge1nn  13790  zmodcl  13860  modmuladdnn0  13884  modsumfzodifsn  13913  seqcl2  13990  seqf2  13991  seqfveq2  13994  monoord  14002  seqid2  14018  expcl2lem  14043  expclzlem  14053  zsqcl2  14107  bcval4  14271  bcn1  14277  bccl2  14287  hashnn0n0nn  14355  hashfun  14401  seqcoll  14429  ccatsymb  14536  ccatrn  14543  ccat2s1fvw  14592  swrds1  14620  swrdccat2  14623  swrdccatin2  14683  pfxccatin12lem2  14685  pfxccatin12lem3  14686  pfxccatin12  14687  pfxccat3  14688  pfxccat3a  14692  spllen  14708  splfv2a  14710  splval2  14711  repswswrd  14738  cshwidxmod  14757  cshwcsh2id  14783  pfx2  14902  2swrd2eqwrdeq  14908  wwlktovfo  14913  wwlktovf1o  14914  shftfn  15024  shftf  15030  01sqrexlem2  15194  01sqrexlem7  15199  resqreu  15203  sqrtneg  15218  nn0abscl  15263  nnabscl  15276  abs2dif  15283  sqreu  15311  limsupval2  15428  climuni  15500  2clim  15520  climcn2  15541  rlimdiv  15596  isercolllem2  15616  isercolllem3  15617  isercoll  15618  isercoll2  15619  iseralt  15635  summolem2a  15665  mptfzshft  15728  fsum0diag2  15733  fsumge0  15745  climcndslem1  15799  mertenslem1  15834  ntrivcvgmul  15852  prodmolem2a  15882  fprodser  15897  fprodeq0  15923  fprodge0  15941  binomrisefac  15990  eff2  16046  tanval  16075  rpnnen2lem9  16169  sqrt2irrlem  16195  fzo0dvdseq  16270  oexpneg  16292  oddge22np1  16296  evennn02n  16297  evennn2n  16298  nno  16329  divalglem5  16344  bitsfzolem  16379  bitsinv1lem  16386  bitsinv2  16388  bitsf1ocnv  16389  bitsinvp1  16394  sadcaddlem  16402  sadadd2lem  16404  sadadd3  16406  sadasslem  16415  sadeq  16417  gcdcllem3  16446  divgcdz  16456  sqgcd  16506  lcmneg  16544  lcmfunsnlem2lem2  16580  prmind2  16626  sqnprm  16643  isprm5  16648  isprm6  16655  qgt0numnn  16691  crth  16715  phimullem  16716  eulerthlem1  16718  eulerthlem2  16719  hashgcdlem  16725  oddprm  16747  pythagtriplem6  16758  pythagtriplem11  16762  pythagtriplem13  16764  pythagtriplem19  16770  iserodd  16772  pclem  16775  pcpremul  16780  pceu  16783  pc2dvds  16816  difsqpwdvds  16824  pcadd  16826  oddprmdvds  16840  pockthlem  16842  pockthg  16843  prmreclem3  16855  1arith  16864  4sqlem11  16892  4sqlem12  16893  4sqlem13  16894  4sqlem14  16895  4sqlem17  16898  vdwlem2  16919  vdwlem8  16925  vdwlem12  16929  ramtlecl  16937  ramub1lem1  16963  prmgaplem4  16991  prmgaplem7  16994  cshwshashlem2  17034  cshwrepswhash1  17040  imasaddfnlem  17478  imasaddflem  17480  imasvscafn  17487  imasvscaf  17489  isacs1i  17605  mreacs  17606  catideu  17623  invfun  17715  invf  17719  invf1o  17720  issubc3  17803  cofucl  17842  funcres2c  17856  ffthf1o  17874  fulloppc  17877  fthoppc  17878  ffthoppc  17879  idffth  17888  cofull  17889  cofth  17890  ressffth  17893  initoeu2lem2  17969  setcmon  18041  setcepi  18042  catciso  18065  fthestrcsetc  18106  fullestrcsetc  18107  embedsetcestrclem  18113  fthsetcestrc  18121  fullsetcestrc  18122  hofcllem  18215  hofcl  18216  yonedalem3  18237  yonffthlem  18239  yoniso  18242  poslubd  18370  lubun  18472  isacs5  18505  acsfiindd  18510  mreclatBAD  18520  psss  18537  cnvtsr  18545  mgmsscl  18570  gsumval2  18611  mgmhmf1o  18625  idmgmhm  18626  resmgmhm  18636  resmgmhm2  18637  resmgmhm2b  18638  mgmhmco  18639  mgmhmeql  18641  sgrp0  18652  sgrp1  18654  hashfinmndnn  18676  ismndd  18681  mndpfo  18682  mnd1  18701  mhmf1o  18718  0mhm  18736  resmhm  18737  resmhm2  18738  resmhm2b  18739  mhmco  18740  gsumvallem2  18751  frmdss2  18780  efmndmnd  18806  sgrp2nmndlem4  18845  isgrpd2e  18877  grpinvf1o  18929  grpinvnzcl  18931  dfgrp3  18958  grp1  18966  mhmmnd  18983  ghmgrp  18985  subgmulg  19056  issubg4  19061  0subgOLD  19068  isnsg3  19076  nmzsubg  19081  ssnmz  19082  nmznsg  19084  0nsg  19085  nsgid  19086  ghmnsgima  19154  ghmnsgpreima  19155  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  conjnmzb  19167  gicref  19186  gafo  19201  gaid  19204  subgga  19205  gass  19206  gasubg  19207  gastacl  19214  orbsta  19218  cntrsubgnsg  19248  invoppggim  19268  symgextf1  19330  symgextfo  19331  symgextf1o  19332  symgfixf1  19346  symgfixfo  19348  symgfixf1o  19349  f1omvdmvd  19352  pmtrprfv  19362  pmtrdifwrdel2  19395  psgneu  19415  psgnvalfi  19423  psgnfieu  19427  psgnprfval  19430  odf1  19471  dfod2  19473  odf1o1  19481  odf1o2  19482  odhash3  19485  sylow1lem2  19508  sylow2blem2  19530  sylow3lem1  19536  sylow3lem2  19537  pj1eu  19605  efglem  19625  efginvrel2  19636  efgsrel  19643  efgsp1  19646  efgsres  19647  efgredleme  19652  efgrelexlemb  19659  efgredeu  19661  efgcpbllemb  19664  isabld  19704  ghmcmn  19740  ghmabl  19741  invghm  19742  cntrabl  19752  torsubg  19763  prdsabld  19771  qusabl  19774  abl1  19775  iscygd  19796  iscygodd  19797  cycsubmcmn  19798  gsumval3a  19812  gsumval3eu  19813  gsumpt  19871  gsummptf1o  19872  dprdcntz  19919  dprdff  19923  dprdfcntz  19926  dprdfadd  19931  dprdlub  19937  dprd2dlem1  19952  dprd2da  19953  dmdprdpr  19960  dprdpr  19961  ablfacrp  19977  ablfac1eu  19984  pgpfaclem1  19992  pgpfaclem2  19993  ablfaclem3  19998  issimpgd  20004  prmgrpsimpgd  20025  ablsimpgprmd  20026  xpsrngd  20073  srgfcl  20090  srglmhm  20115  srgrmhm  20116  iscrngd  20180  ringsrg  20185  prdscrngd  20210  xpsringd  20220  opprring  20238  dvdsrmul  20255  1unit  20265  unitmulcl  20271  unitgrp  20274  unitabl  20275  unitnegcl  20288  isrnghm2d  20341  rnghmf1o  20343  rnghmco  20348  idrnghm  20349  c0mgm  20350  c0snmgmhm  20353  c0snmhm  20354  rngisomring  20358  rhmf1o  20382  rimgim  20388  rhmco  20392  rhmdvdsr  20399  elrhmunit  20401  opprnzr  20411  ringelnzr  20412  0ringnnzr  20414  c0rhm  20423  c0rnghm  20424  zrrnghm  20425  subrngringnsg  20441  subrgcrng  20465  subrguss  20477  subrgunit  20480  subrgnzr  20484  resrhm  20491  isdrng2  20514  drngnzr  20520  isdrngd  20533  isdrngdOLD  20535  issubdrg  20544  imadrhmcl  20556  fldsdrgfld  20557  subdrgint  20562  primefld  20564  isabvd  20571  srngf1o  20605  issrngd  20612  lssneln0  20707  islmhm2  20793  lmhmf1o  20801  pwssplit1  20814  lmimgim  20820  lsslvec  20864  lspabs3  20879  lspsneq  20880  lspfixed  20886  lspexch  20887  lspsolvlem  20900  islbs3  20913  lbsextlem1  20916  lbsextlem3  20918  lbsextlem4  20919  rlmlvec  20973  lidlnz  21002  quscrng  21029  rnglidlmsgrp  21035  rngqiprngimfo  21060  rngqiprngim  21063  drnglpir  21091  unitrrg  21109  domnrrg  21116  opprdomn  21119  drngdomn  21121  fldidomOLD  21124  fidomndrng  21126  cnfldfunALT  21157  xrs1mnd  21183  xrs10  21184  cnmsubglem  21208  gzrngunit  21211  zringunit  21237  prmirredlem  21243  expghm  21246  mulgghm2  21247  domnchr  21303  zncyg  21323  znf1o  21326  zntoslem  21331  znfld  21335  znidomb  21336  cygznlem3  21344  psgnghm  21352  pjfo  21489  frlmlvec  21535  frlmphl  21555  uvcf1  21566  frlmssuvc1  21568  frlmsslsp  21570  frlmup4  21575  lindff1  21594  lindfrn  21595  lsslindf  21604  lmimlbs  21610  indlcim  21614  lmimco  21618  isassad  21638  sraassab  21641  psrbagcon  21702  psrbagconOLD  21703  gsumbagdiaglemOLD  21710  gsumbagdiagOLD  21711  psrass1lemOLD  21712  gsumbagdiaglem  21713  gsumbagdiag  21714  psrass1lem  21715  psrbas  21716  psrcrng  21752  mvrf1  21764  mvrcl  21770  mvrf2  21771  mplsubrglem  21782  mplsubrg  21783  mpllvec  21798  subrgmvrf  21808  mplmon  21809  mplcoe1  21811  mplbas2  21816  opsrtoslem2  21836  evlseu  21865  ply1sclf1  22031  matinvgcell  22157  mat0dimcrng  22192  mat1dimcrng  22199  mat1rngiso  22208  dmatcrng  22224  scmatcrng  22243  scmatfo  22252  scmatf1  22253  scmatf1o  22254  scmatrngiso  22258  mdetunilem9  22342  invrvald  22398  cpmatsubgpmat  22442  mat2pmatf1  22451  mat2pmatghm  22452  m2cpmfo  22478  m2cpmf1o  22479  m2cpmrngiso  22480  pmatcollpwscmatlem2  22512  pm2mpf1  22521  pm2mpfo  22536  pm2mpf1o  22537  pm2mpgrpiso  22539  pm2mprngiso  22544  chfacfisf  22576  chfacfisfcpmat  22577  chfacfscmul0  22580  chfacfpmmul0  22584  chfacfpmmulgsum2  22587  tgcl  22692  tgtopon  22694  indistopon  22724  fctop  22727  cctop  22729  ppttop  22730  epttop  22732  mretopd  22816  toponmre  22817  neiptopuni  22854  neiptoptop  22855  neiptopnei  22856  resttopon  22885  resttopon2  22892  restfpw  22903  perfopn  22909  ordtrest2  22928  cnco  22990  cnpco  22991  lmss  23022  cnt0  23070  cnt1  23074  cnhaus  23078  isnrm2  23082  isnrm3  23083  isreg2  23101  dnsconst  23102  ordtt1  23103  lmfun  23105  dishaus  23106  cncmp  23116  fincmp  23117  tgcmp  23125  cmpcld  23126  uncmp  23127  sscmp  23129  cmpfi  23132  cnconn  23146  conncn  23150  iunconn  23152  conncompss  23157  2ndc1stc  23175  1stcrest  23177  2ndcdisj  23180  1stcelcls  23185  llynlly  23201  restnlly  23206  restlly  23207  islly2  23208  llyrest  23209  nllyrest  23210  llyidm  23212  nllyidm  23213  hausllycmp  23218  cldllycmp  23219  lly1stc  23220  dislly  23221  comppfsc  23256  kgentopon  23262  llycmpkgen2  23274  1stckgen  23278  ptbasfi  23305  txtopon  23315  pttopon  23320  xkotopon  23324  ptclsg  23339  xkoccn  23343  ptcnplem  23345  uptx  23349  txdis1cn  23359  txlly  23360  txnlly  23361  pthaus  23362  ptrescn  23363  txcmp  23367  txhaus  23371  tx1stc  23374  txkgen  23376  xkohaus  23377  txconn  23413  qtoptop2  23423  qtoptopon  23428  qtopkgen  23434  qtopss  23439  qtopeu  23440  qtopomap  23442  qtopcmap  23443  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  nrmr0reg  23473  hmeocnv  23486  hmeof1o2  23487  hmeores  23495  hmeoco  23496  idhmeo  23497  reghmph  23517  nrmhmph  23518  indishmph  23522  ordthmeolem  23525  ordthmeo  23526  txhmeo  23527  txswaphmeo  23529  pt1hmeo  23530  ptunhmeo  23532  xpstopnlem1  23533  xkohmeo  23539  qtopf1  23540  qtophmeo  23541  isfil2  23580  filconn  23607  isufil2  23632  filssufilg  23635  fixufil  23646  uffixfr  23647  fin1aufil  23656  fmf  23669  fmufil  23683  fclsfnflim  23751  ptcmplem3  23778  ptcmplem4  23779  cnextfun  23788  cnextf  23790  cnextfres  23793  grpinvhmeo  23810  tmdgsum2  23820  tgplacthmeo  23827  symgtgp  23830  clsnsg  23834  tgpconncompeqg  23836  tgpconncomp  23837  tgpt0  23843  qustgpopn  23844  prdstgpd  23849  tsmsfbas  23852  tsmsgsum  23863  tsmsres  23868  tsmsinv  23872  tgptsmscls  23874  tsmsxplem1  23877  tsmsxplem2  23878  tsmsxp  23879  tvclvec  23923  ustfilxp  23937  trust  23954  utoptop  23959  utoptopon  23961  utopreg  23977  ressusp  23989  tususp  23997  psmetxrge0  24039  isxmet2d  24053  metres2  24089  prdsdsf  24093  prdsxmetlem  24094  prdsmet  24096  imasdsf1olem  24099  imasf1oxmet  24101  imasf1omet  24102  xmetresbl  24163  tmsxms  24215  tmsms  24216  imasf1oxms  24218  imasf1oms  24219  blcls  24235  comet  24242  stdbdxmet  24244  stdbdmet  24245  met1stc  24250  ressxms  24254  ressms  24255  prdsxms  24259  prdsms  24260  metustto  24282  xmsusp  24298  nrmmetd  24303  tngngp2  24389  nrgdomn  24408  subrgnrg  24410  tngnrg  24411  sranlm  24421  nrginvrcn  24429  nlmtlm  24431  nvctvc  24437  lssnlm  24438  lssnvc  24439  ngpocelbl  24441  nmhmco  24493  nmhmplusg  24494  qdensere  24506  tgioo  24532  xrtgioo  24542  xrsmopn  24548  reperflem  24554  icccmplem1  24558  icccmplem2  24559  reconnlem2  24563  xrge0tsms  24570  metdsf  24584  metdsre  24589  metnrm  24598  mulc1cncf  24645  icchmeo  24685  icchmeoOLD  24686  icopnfcnv  24687  xrhmeo  24691  cnrehmeo  24698  cnrehmeoOLD  24699  evth  24705  phtpcer  24741  pcohtpy  24767  pi1xfrgim  24805  cvsdiv  24879  cvsdivcl  24880  cphnvc  24924  cphsubrglem  24925  cphreccllem  24926  tcphcph  24985  clsocv  24998  iscmet3lem1  25039  iscmet3  25041  cmetss  25064  relcmpcmet  25066  bcthlem5  25076  cmetcusp1  25101  cmetcusp  25102  cphssphl  25119  cmscsscms  25121  cssbn  25123  cmslsschl  25125  chlcsschl  25126  rrxmet  25156  rrxbasefi  25158  minveclem7  25183  hlhil  25191  ivthlem1  25200  evthicc2  25209  ovolfsf  25220  ovolunlem1a  25245  ovoliunlem1  25251  ovolicc2lem2  25267  ovolicc2lem4  25269  ovolicc2lem5  25270  cmmbl  25283  nulmbl  25284  nulmbl2  25285  unmbl  25286  shftmbl  25287  voliunlem2  25300  ioombl1  25311  uniioombl  25338  dyadmbllem  25348  volcn  25355  vitalilem2  25358  vitalilem5  25361  mbfconst  25382  cncombf  25407  cnmbf  25408  i1fd  25430  i1fmullem  25443  itg1addlem2  25446  i1fmulc  25453  itg1mulc  25454  mbfi1fseqlem1  25465  mbfi1fseqlem4  25468  mbfi1flimlem  25472  xrge0f  25481  itg2const2  25491  itg2mulclem  25496  itg2mono  25503  itg2i1fseq  25505  itg2addlem  25508  itg2gt0  25510  itg2cnlem2  25512  itg2cn  25513  iblss  25554  itgle  25559  itgeqa  25563  iblconst  25567  itgconst  25568  ibladdlem  25569  itgaddlem1  25572  iblabslem  25577  iblabs  25578  iblabsr  25579  iblmulc2  25580  itgmulc2lem1  25581  itgsplit  25585  bddmulibl  25588  bddiblnc  25591  itggt0  25593  itgcn  25594  limciun  25643  perfdvf  25652  dvfre  25703  dvcnvlem  25728  dvexp3  25730  dvferm1lem  25736  dvferm2lem  25738  c1lip2  25750  dvle  25759  dvne0  25763  lhop1lem  25765  dvfsumrlim  25783  ftc1lem5  25792  ftc1cn  25795  ply1nz  25874  ply1nzb  25875  ply1domn  25876  ply1divalg  25890  fta1blem  25921  fta1b  25922  ig1peu  25924  ig1pdvds  25929  ply1lpir  25931  ply1pid  25932  elplyr  25950  plyeq0  25960  coeeu  25974  dgrub  25983  plyreres  26032  plydivalg  26048  fta1lem  26056  elqaalem3  26070  qaa  26072  aareccl  26075  aannenlem1  26077  aalioulem6  26086  taylfvallem1  26105  taylf  26109  tayl0  26110  dvtaylp  26118  ulmss  26145  mtest  26152  radcnvle  26168  psercnlem2  26172  psercn  26174  abelthlem2  26180  abelthlem8  26187  abelth  26189  pilem2  26200  pilem3  26201  efif1olem4  26290  efifo  26292  eff1olem  26293  logdmss  26386  dvloglem  26392  logf1o2  26394  efopnlem2  26401  logtayl  26404  cxpcn2  26490  cxpcn3  26492  loglesqrt  26502  logreclem  26503  relogbcl  26514  relogbreexp  26516  relogbmul  26518  relogbcxp  26526  atanre  26626  asinneg  26627  atandmneg  26647  atandmcj  26650  atandmtan  26661  bndatandm  26670  atansssdm  26674  areaf  26702  rlimcnp  26706  rlimcnp3  26708  xrlimcnp  26709  amgmlem  26730  amgm  26731  emcllem7  26742  dmlogdmgm  26764  rpdmgm  26765  dmgmaddnn0  26767  lgamgulmlem1  26769  lgamgulmlem2  26770  wilthlem2  26809  wilthlem3  26810  wilth  26811  ftalem3  26815  basellem3  26823  basellem4  26824  ppisval  26844  ppisval2  26845  sgmnncl  26887  chtdif  26898  ppidif  26903  ppinncl  26914  ppiltx  26917  sqff1o  26922  muinv  26933  dvdsmulf1o  26934  logexprlim  26964  mersenne  26966  perfectlem2  26969  dchrfi  26994  dchrghm  26995  dchrabs  26999  dchr1re  27002  bcmono  27016  bposlem3  27025  bposlem4  27026  bposlem5  27027  bposlem6  27028  bposlem9  27031  lgsfcl2  27042  lgsval2lem  27046  lgsmod  27062  lgsdirprm  27070  lgsne0  27074  lgsqrlem2  27086  gausslemma2dlem0h  27102  gausslemma2dlem1a  27104  gausslemma2dlem4  27108  lgseisenlem1  27114  lgseisenlem2  27115  lgsquadlem1  27119  lgsquadlem2  27120  lgsquad2lem2  27124  2sqlem8  27165  2sqlem9  27166  2sqlem11  27168  2sqmod  27175  2sqreulem1  27185  2sqreunnlem1  27188  dchrisumlem2  27229  dchrisumlem3  27230  dchrmusum2  27233  dchrvmasumlem2  27237  dchrvmasumiflem1  27240  dchrvmaeq0  27243  dchrisum0flblem2  27248  dchrisum0re  27252  dchrisum0lem1b  27254  dchrisum0lem2  27257  dirith2  27267  2vmadivsumlem  27279  chpdifbndlem1  27292  selberg3lem1  27296  selberg4lem1  27299  pntrlog2bndlem3  27318  pntpbnd1  27325  pntibndlem2  27330  pntlemo  27346  pntlem3  27348  nofnbday  27391  noxp1o  27402  nosepdmlem  27422  nosupno  27442  nosupbday  27444  nosupfv  27445  nosupbnd1  27453  nosupbnd2  27455  noinfno  27457  noinfbday  27459  noinffv  27460  noinfbnd1  27468  noinfbnd2  27470  nocvxmin  27516  conway  27537  scutun12  27548  etasslt  27551  scutbdaybnd2  27554  scutbdaybnd2lim  27555  scutbdaylt  27556  slerec  27557  sltlpss  27638  0elleft  27641  0elright  27642  cofcutr  27649  addsval  27684  addsproplem2  27692  addsproplem4  27694  addsproplem5  27695  addsproplem6  27696  addsuniflem  27723  negsproplem2  27742  negsproplem4  27744  negsproplem5  27745  negsproplem6  27746  mulsproplem5  27815  mulsproplem6  27816  mulsproplem7  27817  mulsproplem8  27818  mulsproplem12  27822  mulsuniflem  27843  noreceuw  27878  elons2  27924  peano5n0s  27935  tglngval  28069  hlcgreu  28136  tglinethrueu  28157  ragncol  28227  foot  28240  mideu  28256  opptgdim2  28263  hlpasch  28274  trgcopyeu  28324  cgraswap  28338  cgracom  28340  cgratr  28341  flatcgra  28342  dfcgra2  28348  acopyeu  28352  cgrg3col4  28371  f1otrg  28389  f1otrge  28390  xmstrkgc  28410  axlowdimlem13  28479  axlowdimlem15  28481  axlowdimlem16  28482  axcontlem2  28490  axcontlem3  28491  axcontlem4  28492  axcontlem10  28498  eengtrkg  28511  eengtrkge  28512  structiedg0val  28549  upgr1elem  28639  umgrislfupgrlem  28649  edglnl  28670  ausgrumgri  28694  usgredgreu  28742  uspgredg2vtxeu  28744  uspgredg2v  28748  usgredg2v  28751  usgr1e  28769  subgruhgredgd  28808  subuhgr  28810  subupgr  28811  subumgr  28812  subusgr  28813  upgrreslem  28828  upgrres  28830  umgrres  28831  nbumgrvtx  28870  nbgrssovtx  28885  nbupgrres  28888  nbusgrf1o0  28893  uvtxnbgrb  28925  cusgr0v  28952  cplgr1v  28954  cusgr1v  28955  cusgrexilem2  28966  cusgrexi  28967  structtocusgr  28970  cusgrres  28972  cusgrfilem2  28980  vtxdgfisf  29000  umgr2v2evd2  29051  ewlkprop  29127  lfgriswlk  29212  trlres  29224  upgrwlkdvdelem  29260  uhgrwkspth  29279  usgr2wlkspth  29283  pthdlem1  29290  crctcshwlkn0lem7  29337  crctcshtrl  29344  crctcsh  29345  wwlknbp  29363  wspthnp  29371  wlkswwlksf1o  29400  wwlksnext  29414  wwlksnextinj  29420  wwlksnextsurj  29421  wwlksnextbij0  29422  wwlksnextproplem3  29432  2trld  29459  2spthd  29462  umgr2adedgwlk  29466  umgr2adedgwlkon  29467  umgr2adedgwlkonALT  29468  umgr2adedgspth  29469  elwwlks2ons3  29476  clwwlkbp  29505  clwwlkccatlem  29509  clwlkclwwlklem2a2  29513  clwlkclwwlklem2fv2  29516  clwlkclwwlklem2a4  29517  clwlkclwwlkfolem  29527  clwlkclwwlkfo  29529  clwlkclwwlkf1  29530  clwlkclwwlkf1o  29531  clwwlkinwwlk  29560  clwwlkel  29566  clwwlkf1  29569  clwwlkfo  29570  clwwlkf1o  29571  wwlksext2clwwlk  29577  wwlksubclwwlk  29578  clwwnisshclwwsn  29579  clwwlknccat  29583  s2elclwwlknon2  29624  clwwlknonex2lem2  29628  clwwlknonex2e  29630  lp1cycl  29672  3trld  29692  3spthd  29696  3cycld  29698  eupthp1  29736  eupth2eucrct  29737  frgr1v  29791  nfrgr2v  29792  3vfriswmgrlem  29797  n4cyclfrgr  29811  frgrncvvdeqlem8  29826  frgrncvvdeqlem9  29827  frgrncvvdeqlem10  29828  frgrwopreglem5  29841  clwwnonrepclwwnon  29865  numclwwlk1lem2f1  29877  numclwwlk1lem2fo  29878  numclwwlk1lem2f1o  29879  numclwlk2lem2f1o  29899  nvex  30131  isnv  30132  isblo3i  30321  ipblnfi  30375  ubthlem2  30391  minvecolem7  30403  htthlem  30437  hlimadd  30713  hhsscms  30798  ocsh  30803  occl  30824  pjhthlem2  30912  pjhtheu  30914  pjpreeq  30918  ococin  30928  chscllem2  31158  chscl  31161  unopf1o  31436  cnvunop  31438  unoplin  31440  counop  31441  hmopadj2  31461  hmoplin  31462  bralnfn  31468  lnopmi  31520  unopbd  31535  hmops  31540  hmopm  31541  hmopco  31543  bdophmi  31552  nlelshi  31580  nlelchi  31581  riesz3i  31582  cnlnadjlem2  31588  adjlnop  31606  hmopidmpji  31672  pjclem4  31719  pj3si  31727  h1da  31869  shatomistici  31881  iundisjf  32087  f1o3d  32118  2ndresdju  32141  2ndresdjuf1o  32142  xppreima2  32143  isoun  32190  f1od2  32213  xrge0infss  32240  xrge0addcld  32242  xrofsup  32247  difioo  32260  fzsplit3  32272  iundisjfi  32274  subne0nn  32294  xreceu  32355  s3f1  32380  ccatf1  32382  swrdf1  32387  posrasymb  32402  resspos  32403  resstos  32404  odutos  32405  mgcf1o  32440  abliso  32464  gsumpart  32477  xrge0tsmsd  32479  cntrcrng  32484  pmtrcnel  32520  pmtrcnelor  32522  cycpmfv2  32543  cycpmcl  32545  cycpmco2lem4  32558  tocyccntz  32573  archiabllem1  32609  archiabllem2c  32611  archiabllem2  32613  isdrng4  32665  suborng  32703  subofld  32704  quslvec  32745  0nellinds  32757  dvdsruasso  32764  lindssn  32768  nsgmgc  32797  ghmqusker  32806  lmhmqusker  32808  rhmqusker  32818  drngidlhash  32826  qsidomlem2  32846  qsnzr  32848  mxidlirredi  32861  drngmxidl  32867  fply1  32911  ply1lvec  32912  sradrng  32958  sralvec  32960  rlmdim  32982  rgmoddimOLD  32983  matdim  32988  lmhmlvec2  32992  ply1degltdimlem  32995  ply1degltdim  32996  dimkerim  33000  fedgmul  33004  extdg1id  33030  irngnzply1  33044  algextdeglem8  33069  qtopt1  33113  qtophaus  33114  locfinreflem  33118  cmppcmp  33136  dispcmp  33137  zarmxt1  33158  pstmxmet  33175  xpinpreima2  33185  tpr2rico  33190  ordtrest2NEW  33201  xrmulc1cn  33208  zrhnm  33247  indf1ofs  33322  hashf2  33380  hasheuni  33381  esumcvg  33382  prsiga  33427  pwldsys  33453  ldsysgenld  33456  ldgenpisyslem1  33459  sxsigon  33488  measdivcstALTV  33521  volfiniune  33526  imambfm  33559  dya2iocnrect  33578  omssubaddlem  33596  sibfof  33637  sitgf  33644  oddpwdc  33651  eulerpartlemb  33665  eulerpartlemgvv  33673  sseqmw  33688  sseqf  33689  sseqp1  33692  fibp1  33698  prob01  33710  probfinmeasb  33725  probfinmeasbALTV  33726  probmeasb  33727  dstrvprob  33768  dstfrvel  33770  ballotlemic  33803  ballotlem1c  33804  ballotlemro  33819  ballotlemrc  33827  ballotlemirc  33828  ballotth  33834  plymulx0  33856  signstfvn  33878  signstfvcl  33882  signstfveq0a  33885  signstfveq0  33886  fdvposlt  33909  reprpmtf1o  33936  tgoldbachgnn  33969  bnj951  34084  bnj1379  34139  bnj1422  34146  bnj149  34184  bnj151  34186  bnj908  34240  bnj944  34247  bnj970  34256  bnj1006  34269  bnj1177  34315  bnj1189  34318  bnj1321  34336  bnj1398  34343  bnj1417  34350  bnj1523  34380  srcmpltd  34383  f1resrcmplf1d  34388  pthhashvtx  34416  2cycld  34427  subfacp1lem3  34471  subfacp1lem5  34473  erdszelem8  34487  erdszelem9  34488  cnpconn  34519  txpconn  34521  ptpconn  34522  connpconn  34524  sconnpi1  34528  txsconn  34530  cvxpconn  34531  cvxsconn  34532  iccllysconn  34539  cvmseu  34565  cvmfolem  34568  cvmliftmolem2  34571  cvmliftlem14  34586  cvmlift2lem9a  34592  cvmlift2lem12  34603  cvmlift2lem13  34604  cvmlift3  34617  satfdm  34658  fmla1  34676  fmlaomn0  34679  fmlasucdisj  34688  satff  34699  sategoelfvb  34708  mvrsfpw  34795  mrsubrn  34802  mrsubff1  34803  msubff  34819  msubff1  34845  mvhf1  34848  mclsssvlem  34851  mclsind  34859  mthmpps  34871  lediv2aALT  34960  dfon2  35068  dfrdg4  35227  altxpsspw  35253  segconeu  35287  btwnconn1lem13  35375  btwnconn1lem14  35376  outsideofeu  35407  outsidele  35408  linerflx1  35425  linethrueu  35432  fwddifval  35438  fwddifnval  35439  gg-cnfldfunALT  35484  nn0prpwlem  35510  neibastop1  35547  neibastop2lem  35548  topjoin  35553  fnemeet1  35554  fnemeet2  35555  fnejoin1  35556  fnejoin2  35557  filnetlem3  35568  onsuctopon  35622  bj-nnfim  35927  bj-nnfand  35930  bj-nnford  35932  bj-dfnnf3  35938  bj-nnfalt  35947  bj-nnfext  35948  bj-elgab  36122  relowlssretop  36547  elxp8  36555  finorwe  36566  finxp1o  36576  pibt2  36601  finixpnum  36776  fin2solem  36777  fin2so  36778  lindsadd  36784  lindsdom  36785  lindsenlbs  36786  ptrecube  36791  poimirlem4  36795  poimirlem7  36798  poimirlem13  36804  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem24  36815  poimirlem26  36817  poimirlem27  36818  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  opnmbllem0  36827  mblfinlem2  36829  itg2gt0cn  36846  ibladdnclem  36847  itgaddnclem1  36849  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  itgmulc2nclem1  36857  itggt0cn  36861  ftc1cnnc  36863  ftc1anclem3  36866  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  areacirclem2  36880  areacirc  36884  unirep  36885  sdclem1  36914  mettrifi  36928  istotbnd3  36942  sstotbnd2  36945  sstotbnd  36946  sstotbnd3  36947  equivtotbnd  36949  isbndx  36953  isbnd3  36955  blbnd  36958  equivbnd  36961  prdsbnd  36964  prdstotbnd  36965  ismtyhmeo  36976  heibor1  36981  heibor  36992  bfp  36995  rrnmet  37000  rrncmslem  37003  rrnequiv  37006  ismrer1  37009  iccbnd  37011  opidonOLD  37023  grpokerinj  37064  isgrpda  37126  isdrngo2  37129  iscringd  37169  crngohomfo  37177  smprngopr  37223  prnc  37238  isfldidl  37239  petlem  37985  prter3  38055  lshpnelb  38157  lsatspn0  38173  lsatssn0  38175  lssats  38185  lsatcv0  38204  lsat0cv  38206  islshpcv  38226  lkr0f  38267  lshpsmreu  38282  lduallvec  38327  lkrlspeqN  38344  cdleme50f1  39717  cdleme50f1o  39720  cdleme  39734  cdlemk56  40145  dvalveclem  40199  dvhlveclem  40282  dvheveccl  40286  cdlemm10N  40292  diaf1oN  40304  dihord4  40432  dihf11lem  40440  dihf11  40441  dihglblem2N  40468  dihglb2  40516  dochvalr  40531  doch2val2  40538  dochocss  40540  dochsat  40557  dochshpncl  40558  dochnel  40567  dvh4dimlem  40617  dochsnkr2cl  40648  dochkr1  40652  lcfl6lem  40672  lcfl9a  40679  lclkrlem1  40680  lclkrlem2l  40692  lclkrlem2o  40695  lclkrlem2q  40697  lclkr  40707  lclkrslem1  40711  lclkrslem2  40712  lcfrlem9  40724  lcfrlem16  40732  lcfrlem17  40733  lcfrlem27  40743  lcfrlem37  40753  lcfrlem38  40754  lcfrlem40  40756  lcdlkreqN  40796  mapdordlem2  40811  mapdrvallem2  40819  mapdn0  40843  mapdpglem20  40865  mapdpglem30  40876  mapdpglem32  40879  mapdpg  40880  mapdindp0  40893  mapdh6aN  40909  mapdh6eN  40914  mapdh6kN  40920  hdmaplem4  40948  hdmap1val  40972  hdmap1l6a  40983  hdmap1l6e  40988  hdmap1l6k  40994  hdmapval3N  41012  hdmap11lem2  41016  hdmapnzcl  41019  hdmaprnlem3eN  41032  hdmap14lem4a  41045  hdmap14lem6  41047  hdmap14lem7  41048  hgmapvvlem2  41098  hgmapvvlem3  41099  hlhilhillem  41138  lcmineqlem15  41214  aks4d1p1  41247  aks4d1p3  41249  xppss12  41353  imacrhmcl  41393  frlmsnic  41412  mhmcompl  41422  evlsbagval  41440  mhpind  41468  posqsqznn  41536  addinvcom  41606  prjspersym  41651  0prjspnlem  41667  dffltz  41678  flt0  41681  flt4lem5e  41700  isnacs3  41750  mzpindd  41786  eldioph  41798  eldioph3  41806  rencldnfilem  41860  irrapxlem1  41862  irrapxlem4  41865  irrapxlem6  41867  pellexlem5  41873  pellfundlb  41924  rmspecnonsq  41947  rmxnn  41992  rmynn  41997  rmynn0  41998  jm2.22  42036  jm2.23  42037  jm2.20nn  42038  jm2.27a  42046  jm2.27c  42048  rmydioph  42055  jm3.1lem3  42060  dford3lem1  42067  rpnnen3lem  42072  harinf  42075  wepwsolem  42086  dnnumch3  42091  fnwe2lem2  42095  fnwe2  42097  dfac11  42106  lnmlsslnm  42125  lnmepi  42129  lmhmlnmsplit  42131  pwssplit4  42133  filnm  42134  imasgim  42144  harn0  42146  lpirlnr  42161  hbtlem7  42169  hbtlem6  42173  hbt  42174  dgraaub  42192  mpaaeu  42194  aaitgo  42206  rgspnmin  42215  proot1ex  42245  deg1mhm  42251  onsucelab  42315  onsucf1olem  42322  cantnfub2  42374  omabs2  42384  tfsconcatlem  42388  tfsconcatfo  42395  ofoafo  42408  naddcnffo  42416  oaun3lem1  42426  oaun3lem3  42428  nadd2rabord  42437  nadd2rabon  42439  nadd1rabord  42441  nadd1rabon  42443  naddwordnexlem4  42454  fzunt  42508  fzuntd  42509  fzunt1d  42510  fzuntgd  42511  omssrncard  42593  fiinfi  42626  cotrclrcl  42795  fsovf1od  43069  ntrk2imkb  43090  ntrf  43176  gneispacef2  43189  rr-phpd  43264  expgrowth  43396  binomcxplemdvbinom  43414  binomcxplemnotnn0  43417  ordelordALT  43600  2uasbanh  43624  rfcnnnub  44022  elixpconstg  44079  ssrabdf  44105  rabidd  44150  wessf1ornlem  44182  disjinfi  44189  projf1o  44194  fconst7  44267  fzisoeu  44308  monoordxrv  44490  iccshift  44529  iooshift  44533  fmul01lt1lem2  44599  ellimciota  44628  mullimc  44630  mullimcf  44637  sumnnodd  44644  addlimc  44662  liminfval2  44782  liminflimsupxrre  44831  icccncfext  44901  dvcosre  44926  dvdivbd  44937  dvdivcncf  44941  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  itgsinexplem1  44968  iblcncfioo  44992  itgperiod  44995  stoweidlem7  45021  stoweidlem14  45028  stoweidlem16  45030  stoweidlem26  45040  stoweidlem27  45041  stoweidlem31  45045  stoweidlem34  45048  stoweidlem36  45050  stoweidlem46  45060  stoweidlem47  45061  stoweidlem52  45066  stoweidlem57  45071  stoweidlem59  45073  stoweidlem60  45074  wallispilem3  45081  wallispilem4  45082  dirkertrigeqlem3  45114  dirkeritg  45116  dirkercncf  45121  fourierdlem15  45136  fourierdlem20  45141  fourierdlem25  45146  fourierdlem34  45155  fourierdlem37  45158  fourierdlem41  45162  fourierdlem42  45163  fourierdlem47  45167  fourierdlem48  45168  fourierdlem51  45171  fourierdlem52  45172  fourierdlem57  45177  fourierdlem58  45178  fourierdlem59  45179  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem68  45188  fourierdlem79  45199  fourierdlem80  45200  fourierdlem81  45201  fourierdlem92  45212  fourierdlem104  45224  fourierdlem111  45231  fouriersw  45245  etransclem3  45251  etransclem7  45255  etransclem10  45258  etransclem15  45263  etransclem19  45267  etransclem20  45268  etransclem21  45269  etransclem22  45270  etransclem24  45272  etransclem25  45273  etransclem27  45275  etransclem28  45276  etransclem35  45283  etransclem44  45292  etransclem48  45296  nnfoctbdjlem  45469  preimagelt  45713  preimalegt  45714  fnresfnco  46049  funressnfv  46051  fsetsnf1  46060  fsetsnfo  46061  fsetsnf1o  46062  cfsetsnfsetf1  46067  cfsetsnfsetfo  46068  cfsetsnfsetf1o  46069  fcoresf1  46077  ffnafv  46177  rlimdmafv  46183  dfatco  46262  rlimdmafv2  46264  zm1nn  46308  eluzge0nn0  46318  2elfz2melfz  46324  subsubelfzo0  46332  smonoord  46337  setsnidel  46343  imasetpreimafvbijlemf1  46370  imasetpreimafvbijlemfo  46371  imasetpreimafvbij  46372  iccpartigtl  46389  iccpartgt  46393  iccpartf  46397  icceuelpart  46402  fargshiftf1  46407  fargshiftfo  46408  sprsymrelfolem2  46459  sprsymrelfo  46463  sprsymrelf1o  46464  prproropf1o  46473  sfprmdvdsmersenne  46569  lighneallem4  46576  evenm1odd  46605  evenp1odd  46606  oddp1eveni  46607  oddm1eveni  46608  m2even  46620  oexpnegALTV  46643  opoeALTV  46649  opeoALTV  46650  oddprmALTV  46653  nnoALTV  46661  nn0oALTV  46662  nnpw2evenALTV  46668  perfectALTVlem2  46688  perfectALTV  46689  sbgoldbalt  46747  wtgoldbnnsum4prm  46768  bgoldbnnsum3prm  46770  isomuspgrlem2c  46796  isomuspgrlem2d  46797  isomuspgrlem2e  46798  1hegrlfgr  46808  uspgrsprfo  46824  uspgrsprf1o  46825  copissgrp  46844  zlidlring  46914  2zlidl  46920  2zrngamgm  46925  2zrngagrp  46929  2zrngmmgm  46932  rngcinv  46967  rngcinvALTV  46979  ringcinv  47018  ringcinvALTV  47042  nn0eo  47301  blennnelnn  47349  nnpw2blen  47353  dignn0fr  47374  dignn0ldlem  47375  dig2nn1st  47378  1arymaptf1  47415  1arymaptfo  47416  1arymaptf1o  47417  2arymaptf1  47426  2arymaptfo  47427  2arymaptf1o  47428  inlinecirc02p  47560  toslat  47694  topdlat  47716  isthincd  47744  fullthinc  47753  thincfth  47755  thincciso  47756  0thincg  47757  aacllem  47935