Theorem sylc 65

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	⊢ (𝜑 → 𝜓)
sylc.2	⊢ (𝜑 → 𝜒)
sylc.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylc.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 2, 3	syl2im 40	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 52	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl3c  66  mpsyl  68  jc  161  jcnd  163  2thd  265  jca  511  syl2anc  585  aevlem0  2058  equvel  2461  elex22  3467  spcedv  3554  rspcdf  3565  rspcdva  3579  rspc3dv  3597  spsbcd  3756  opth  5434  euotd  5471  wereu2  5631  unielrel  6242  frpomin  6308  tz7.7  6353  funmo  6518  fvelimad  6911  iinpreima  7025  fompt  7074  fnfvima  7191  resfvresima  7193  fliftfun  7270  fliftval  7274  weniso  7312  riota5f  7355  riotass2  7357  fovcld  7497  ofmpteq  7657  ssorduni  7736  nlimsucg  7796  tfisi  7813  zfrep6OLD  7911  curry1  8058  curry2  8061  fnwelem  8085  funsssuppss  8144  frrlem4  8243  frrlem8  8247  frrlem10  8249  fprlem1  8254  fprlem2  8255  smogt  8311  tfrlem5  8323  omeulem1  8521  oeworde  8533  oelimcl  8540  oeeulem  8541  oeeui  8542  nnawordex  8577  oaabs2  8589  naddssim  8625  naddsuc2  8641  swoso  8682  qliftlem  8749  resixp  8885  domssl  8949  domssr  8950  xpdom3  9017  domunsncan  9019  omxpenlem  9020  domssex  9080  xpf1o  9081  mapdom3  9091  dif1en  9100  findcard  9102  f1dmvrnfibi  9255  fsuppss  9300  fiin  9339  marypha1lem  9350  marypha1  9351  fisupcl  9387  supgtoreq  9388  ordiso2  9434  ordtypelem2  9438  ordtypelem8  9444  wemapso2lem  9471  unxpwdom2  9507  cantnflt  9595  cantnfrescl  9599  oemapvali  9607  cantnflem1d  9611  wemapwe  9620  cnfcom  9623  ttrclss  9643  ttrclselem2  9649  frrlem15  9683  rankr1id  9788  tcrank  9810  cardmin2  9925  infxpenlem  9937  fseqen  9951  ween  9959  ac5num  9960  indcardi  9965  acni2  9970  fodomfi2  9984  infpwfien  9986  inffien  9987  iunfictbso  10038  acacni  10065  dfac12lem2  10069  djuinf  10113  infmap2  10141  ackbij1lem18  10160  ackbij1b  10162  fictb  10168  cfslb2n  10192  cofsmo  10193  cfsmolem  10194  coftr  10197  infpssrlem4  10230  domfin4  10235  fin2i2  10242  isfin2-2  10243  fincssdom  10247  ssfin3ds  10254  fin23lem20  10261  fin23lem30  10266  isf32lem3  10279  fin1a2lem12  10335  fin1a2lem13  10336  hsmexlem2  10351  axdc2lem  10372  imadomg  10458  fnct  10461  iundom2g  10464  iundomg  10465  iundom  10466  unirnfdomd  10492  konigthlem  10493  iunctb  10499  fpwwe2  10568  canthwelem  10575  pwfseqlem3  10585  pwfseqlem5  10588  winalim2  10621  wunelss  10633  r1wunlim  10662  wunex2  10663  tsksdom  10681  tskinf  10694  inttsk  10699  inar1  10700  tskcard  10706  tskurn  10714  gruina  10743  grur1a  10744  grur1  10745  addsrpr  11000  mulsrpr  11001  lemul12a  12013  lemulge11  12018  lediv12a  12049  fiminre2  12104  nngt0  12190  nn0ge2m1nn  12485  peano5uzi  12595  nn0ind-raph  12606  znnn0nn  12617  suprzub  12866  uzsupss  12867  rpge0  12933  fz0fzelfz0  13564  fz0fzdiffz0  13567  ige2m2fzo  13658  elfzodifsumelfzo  13661  elfzom1elp1fzo  13662  fzonfzoufzol  13701  flltdivnn0lt  13767  fldiv  13794  modaddmodup  13871  uzrdgsuci  13897  fzennn  13905  uzindi  13919  fsuppmapnn0fiubex  13929  expcl2lem  14010  leexp1a  14112  modexp  14175  faclbnd  14227  faclbnd6  14236  facavg  14238  hashginv  14271  hashf1rn  14289  hasheqf1od  14290  seqcoll  14401  hashge2el2dif  14417  wrdsymb0  14486  wrdlenge2n0  14489  ccatsymb  14520  swrdnd2  14593  swrdnd0  14595  pfxnd  14625  pfxccat1  14639  swrdpfx  14644  pfxpfx  14645  wrd2ind  14660  pfxccatin12  14670  pfxccat3  14671  swrdccat  14672  pfxccatpfx1  14673  pfxccatpfx2  14674  swrdccatin1d  14680  pfxccatin12d  14682  repswswrd  14721  cshwidxmod  14740  s2f1o  14853  f1oun2prg  14854  wwlktovfo  14895  relexpfld  14986  rtrclreclem3  14997  resqrex  15187  cau3lem  15292  reusq0  15402  rlimcld2  15515  climcn2  15530  isercoll  15605  climsup  15607  caurcvgr  15611  sumeq2ii  15630  summolem3  15651  zsum  15655  fsumadd  15677  fsumsplit1  15682  fsum2dlem  15707  fsum0diag2  15720  fsummulc2  15721  fsumabs  15738  fsumrelem  15744  fsumrlim  15748  fsumo1  15749  o1fsum  15750  fsumiun  15758  qshash  15764  prodeq2ii  15848  prodmolem3  15870  fprodmul  15897  fproddiv  15898  fprod2dlem  15917  fprodsplit1f  15927  sin02gt0  16131  efieq1re  16138  p1modz1  16200  dvdsleabs2  16253  4dvdseven  16314  sumeven  16328  sumodd  16329  divalglem9  16342  smupvallem  16424  algfx  16521  eucalgcvga  16527  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmflefac  16589  qredeq  16598  dvdszzq  16662  fermltl  16725  modprm0  16747  pythagtriplem4  16761  pythagtriplem6  16763  pythagtriplem7  16764  pythagtriplem12  16768  pythagtriplem13  16769  pythagtriplem14  16770  pythagtriplem16  16772  difsqpwdvds  16829  pcmpt  16834  prmreclem2  16859  4sqlem11  16897  vdwlem9  16931  vdwlem11  16933  vdwlem12  16934  0ram  16962  0ram2  16963  0ramcl  16965  ramcl  16971  prmolelcmf  16990  cshwsidrepsw  17035  cshwshashlem2  17038  prmlem1  17049  prmlem2  17061  strfvd  17141  strfv2d  17142  strssd  17146  firest  17366  prdsdsval3  17419  imasbas  17447  imasds  17448  imasaddfnlem  17463  imasaddvallem  17464  imasvscafn  17472  qusaddvallem  17486  qusaddflem  17487  qusaddval  17488  qusaddf  17489  qusmulval  17490  qusmulf  17491  catideu  17612  idinv  17727  brcici  17738  invfuc  17915  2initoinv  17948  initoeu1w  17950  initoeu2lem0  17951  2termoinv  17955  termoeu1w  17957  resspos  18366  resstos  18367  mod2ile  18431  lubss  18450  acsmapd  18491  chnso  18561  lidrididd  18609  gsumval2a  18624  mndind  18767  submefmnd  18834  mgm2nsgrplem4  18863  qusgrp2  19005  mulgnegnn  19031  pgrpsubgsymg  19355  fvcosymgeq  19375  gsmsymgreqlem1  19376  psgnunilem4  19443  pgpssslw  19560  sylow2alem2  19564  fislw  19571  efgsres  19684  rinvmod  19752  gsumval3lem2  19852  gsumzaddlem  19867  gsum2d  19918  nn0gsumfz  19930  telgsums  19939  dprddomcld  19949  ablfac2  20037  qusrng  20132  srgdilem  20144  o2timesd  20162  rglcom4d  20163  ringdilem  20201  qusring2  20287  orngsqr  20816  lssintcl  20932  lbsextlem3  21132  lbsextlem4  21133  zringlpirlem3  21436  psgnodpm  21560  psgndiflemB  21572  frlmup4  21773  lindff1  21792  lindfrn  21793  lmisfree  21814  evlseu  22055  mhpmulcl  22109  mptcoe1fsupp  22173  cply1coe0bi  22263  mpfpf1  22312  pf1mpf  22313  mat0dimscm  22430  mdetdiagid  22561  mdet1  22562  mdetunilem9  22581  slesolinv  22641  cramerimp  22647  cpmatmcllem  22679  mptcoe1matfsupp  22763  mp2pm2mp  22772  chpdmat  22802  cctop  22967  subbascn  23215  cnss2  23238  cmpcovf  23352  2ndcctbss  23416  2ndcomap  23419  2ndcsep  23420  comppfsc  23493  ptclsg  23576  dfac14  23579  txcnp  23581  ptcnplem  23582  uptx  23586  txtube  23601  tx2ndc  23612  xkococnlem  23620  elqtop  23658  qtoprest  23678  indishmph  23759  ptcmpfi  23774  kqhmph  23780  csdfil  23855  filssufilg  23872  ufilen  23891  rnelfm  23914  fmfnfmlem4  23918  alexsubALTlem4  24011  ptcmplem4  24016  cnextfvval  24026  cnextcn  24028  cnextfres  24030  tmdgsum2  24057  imasf1oxmet  24336  metss  24469  met2ndci  24483  prdsxmslem2  24490  metust  24519  cfilucfil  24520  metustbl  24527  psmetutop  24528  opnreen  24793  rectbntr0  24794  fsumcn  24834  rescncf  24863  xrhmeo  24917  cnllycmp  24928  lebnumlem1  24933  lebnumlem3  24935  cfilss  25243  iscmet3lem1  25264  iscmet3lem2  25265  ivthicc  25432  ovolsslem  25458  ovoliunlem2  25477  ovoliunnul  25481  ovolicc2lem4  25494  voliunlem3  25526  volsup  25530  uniiccdif  25552  uniioombllem2  25557  volivth  25581  mbfimaopnlem  25629  mbflimsup  25640  i1fd  25655  itg1addlem4  25673  itg2addlem  25732  itg2gt0  25734  limciun  25868  dvadd  25916  dvmul  25917  dvco  25924  dvrec  25932  dvcnv  25954  dvferm  25965  rollelem  25966  dvlip  25971  dvlip2  25973  c1liplem1  25974  c1lip2  25976  dvgt0lem1  25980  dvivthlem1  25986  lhop1lem  25991  dvcnvrelem1  25995  dvcnvrelem2  25996  dvcvx  25998  dvfsumle  25999  dvfsumleOLD  26000  dvfsumabs  26002  dvfsumlem1  26005  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  dvfsumrlim2  26012  dvfsum2  26014  ftc1cn  26023  ftc2ditglem  26025  itgsubstlem  26028  itgpowd  26030  mdegaddle  26052  mdegmullem  26056  deg1sublt  26088  ply1divmo  26114  fta1g  26148  dgrub  26212  dgrnznn  26225  dgradd2  26247  dvply1  26264  plyrem  26286  aalioulem4  26316  aalioulem5  26317  aalioulem6  26318  aaliou2  26321  taylf  26341  ulmdv  26385  psercn2  26405  psercn2OLD  26406  abelth  26424  abelth2  26425  reeff1olem  26429  efopn  26640  logreclem  26745  isosctrlem2  26802  xrlimcnp  26951  basellem4  27067  ppiwordi  27145  musum  27174  chpub  27204  gausslemma2dlem0c  27342  2sqlem6  27407  addsqnreup  27427  2sqreulem1  27430  2sqreunnlem1  27433  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  pntlemp  27594  pntleml  27595  ostth3  27622  ltsres  27647  noextenddif  27653  nolesgn2ores  27657  nogesgn1ores  27659  nosep1o  27666  nosep2o  27667  nosepeq  27670  nolt02o  27680  noresle  27682  nosupno  27688  nosupbday  27690  nosupres  27692  nosupbnd1lem1  27693  nosupbnd1lem4  27696  nosupbnd1  27699  nosupbnd2lem1  27700  nosupbnd2  27701  noinfno  27703  noinfbday  27705  noinfres  27707  noinfbnd1lem5  27712  noinfbnd1  27714  noinfbnd2lem1  27715  ltlesd  27758  madebday  27913  leadds1  28002  precsexlem10  28229  noseqrdg0  28320  noseqrdgsuc  28321  elnnzs  28414  bdaypw2n0bndlem  28476  iscgrglt  28604  colline  28739  axlowdimlem16  29048  axlowdimlem17  29049  axcontlem3  29057  axcontlem10  29064  uhgr2edg  29299  nbupgruvtxres  29498  cusgrres  29540  cusgrfilem2  29548  vdumgr0  29572  frusgrnn0  29663  wlkp1lem8  29770  pthdivtx  29818  upgrwlkdvde  29828  spthonepeq  29843  usgr2pthlem  29854  cyclnumvtx  29891  lfgrn1cycl  29896  wwlknbp1  29935  wwlknllvtx  29937  wlkiswwlks2lem3  29962  umgr2adedgspth  30039  clwlkclwwlklem3  30094  clwwisshclwwslemlem  30106  clwwisshclwws  30108  clwwlkel  30139  wwlksubclwwlk  30151  eleclclwwlknlem1  30153  eleclclwwlknlem2  30154  erclwwlknref  30162  clwwlknonccat  30189  clwwlknonex2lem2  30201  3wlkdlem4  30255  vdn0conngrumgrv2  30289  eucrctshift  30336  frgrnbnb  30386  frgrncvvdeqlem2  30393  frgrncvvdeqlem3  30394  fusgreghash2wspv  30428  numclwwlk2lem1  30469  numclwlk2lem2f  30470  numclwwlk5  30481  numclwwlk7  30484  frgrreggt1  30486  minvecolem4b  30972  minvecolem4  30974  bcsiALT  31273  ococin  31502  spanpr  31674  pjorthi  31763  nmbdoplbi  32118  nmcoplbi  32122  nmbdfnlbi  32143  nmcfnlbi  32146  nmopcoi  32189  branmfn  32199  hstnmoc  32317  mdsl0  32404  atomli  32476  atcvat4i  32491  atabsi  32495  foresf1o  32597  rabfodom  32598  abrexdomjm  32600  elpreq  32621  ifeqeqx  32635  disjiunel  32689  ac6mapd  32719  aciunf1lem  32758  ffsrn  32824  xlt2addrd  32856  supxrnemnf  32865  ssnnssfz  32884  gsummptres2  33153  gsumfs2d  33161  archirngz  33289  isarchiofld  33299  unitprodclb  33488  elrspunidl  33527  drngidlhash  33533  prmidl2  33540  qsidomlem2  33552  ssmxidl  33573  1arithidom  33636  1arithufdlem4  33646  constrmon  33928  locfinreflem  34024  cmpcref  34034  fmcncfil  34115  xrge0iifiso  34119  elzdif0  34164  qqhval2lem  34165  esumcst  34247  esumrnmpt2  34252  esumpinfval  34257  esumpinfsum  34261  sigaclci  34316  insiga  34321  ldgenpisys  34350  measres  34406  measdivcstALTV  34409  dya2iocnrect  34465  dya2iocnei  34466  omssubadd  34484  carsggect  34502  carsgclctunlem2  34503  sitgclg  34526  eulerpartlemsv2  34542  eulerpartlemv  34548  eulerpartlemf  34554  eulerpartlemgh  34562  eulerpartlemgs2  34564  ballotlemfp1  34676  ballotlemfrcn0  34714  ftc2re  34782  fdvposlt  34783  fdvposle  34785  bnj1379  35012  bnj580  35095  bnj944  35120  bnj999  35140  bnj1204  35194  bnj1398  35216  cusgredgex  35344  pthacycspth  35379  derangenlem  35393  subfacp1lem3  35404  resconn  35468  cvmliftlem3  35509  satfv0fvfmla0  35635  satfv1fvfmla1  35645  mrsub0  35738  cgrextend  36230  segconeq  36232  trisegint  36250  fwddifnp1  36387  ivthALT  36557  fnessref  36579  refssfne  36580  neibastop1  36581  filnetlem4  36603  ontgval  36653  weiunlem  36685  weiunse  36690  unblimceq0lem  36734  unbdqndv2lem2  36738  unbdqndv2  36739  bj-babygodel  36836  bj-alrimd  36858  bj-exlimd  36870  bj-spim  36888  bj-spime  36889  bj-nnf-spime  37040  bj-spcimdv  37170  bj-spcimdvv  37171  bj-finsumval0  37567  bj-fvimacnv0  37568  dfgcd3  37606  relowlssretop  37645  relowlpssretop  37646  onsucuni3  37649  finxpreclem4  37676  poimirlem18  37918  poimirlem21  37921  poimirlem25  37925  ftc1cnnclem  37971  ftc1cnnc  37972  ftc2nc  37982  dvasin  37984  dvacos  37985  abrexdom  38010  indexdom  38014  mettrifi  38037  equivtotbnd  38058  totbndbnd  38069  prdstotbnd  38074  heibor1lem  38089  bfplem1  38102  bfplem2  38103  opidonOLD  38132  rngodm1dm2  38212  zerdivemp1x  38227  equid1  39304  omllaw5N  39652  cmtcomlemN  39653  cmtbr3N  39659  omlfh3N  39664  atlen0  39715  exatleN  39809  hlrelat3  39817  cvrexchlem  39824  atlelt  39843  cvrat4  39848  4atlem11b  40013  4atlem12b  40016  lneq2at  40183  cdlema1N  40196  cdlemblem  40198  paddss12  40224  paddasslem2  40226  paddasslem4  40228  paddasslem6  40230  paddasslem12  40236  paddunN  40332  poml4N  40358  poml5N  40359  osumcllem6N  40366  pexmidlem6N  40380  pl42lem2N  40385  ltrnu  40526  ltrneq2  40553  trlval2  40568  cdlemd6  40608  cdleme25b  40759  cdleme29b  40780  cdlemefr29exN  40807  ltrniotacnvval  40987  cdlemk28-3  41313  dochexmidlem7  41871  muldvds2d  42397  frlmsnic  42939  nna4b4nsq  43047  mzpsubmpt  43129  mzpsubst  43134  eqrabdioph  43163  rabdiophlem2  43188  elpell14qr2  43248  elpell1qr2  43258  pellfundre  43267  pellfundge  43268  pellfundglb  43271  pellfund14gap  43273  congabseq  43360  jm2.22  43381  jm2.23  43382  jm2.26lem3  43387  wepwsolem  43428  dnwech  43434  aomclem2  43441  aomclem4  43443  pwfi2f1o  43482  onexlimgt  43629  oaltublim  43676  oege1  43692  cantnfub2  43708  cantnfresb  43710  cantnf2  43711  oacl2g  43716  tfsconcatb0  43730  tfsconcatrev  43734  oaun3lem1  43760  oaun3lem2  43761  nadd2rabtr  43770  nadd1suc  43778  naddwordnexlem0  43782  naddwordnexlem3  43785  oawordex3  43786  naddwordnexlem4  43787  oaltom  43790  omltoe  43792  ss2iundf  44044  dssmapf1od  44406  neik0pk1imk0  44432  gneispace  44519  grur1cld  44617  cpcolld  44643  mnuop23d  44651  mnuprdlem1  44657  mnuprdlem2  44658  mnurndlem1  44666  grumnudlem  44670  radcnvrat  44699  sbiota1  44819  ordelordALT  44922  2pm13.193  44937  ee11an  45075  modelaxreplem2  45364  refsumcn  45419  rfcnnnub  45425  disjxp1  45458  xrnmnfpnf  45472  ssinc  45475  nssd  45493  disjf1o  45579  disjinfi  45580  choicefi  45587  axccdom  45609  dmrelrnrel  45613  monoords  45688  fperiodmullem  45694  xadd0ge  45710  xrssre  45736  xrlexaddrp  45740  xrred  45752  infxr  45754  xrnpnfmnf  45861  monoordxrv  45868  monoord2xrv  45870  cvgcaule  45878  fsumiunss  45964  fmul01  45969  fmuldfeqlem1  45971  fmuldfeq  45972  fmul01lt1lem1  45973  fmul01lt1lem2  45974  cncfmptss  45976  climinf  45995  climsuselem1  45996  climsuse  45997  limcperiod  46017  limcrecl  46018  sumnnodd  46019  limcleqr  46031  0ellimcdiv  46036  climleltrp  46063  limsuppnfdlem  46088  limsupresxr  46153  liminfresxr  46154  liminfvalxr  46170  cnrefiisplem  46216  xlimmnfvlem1  46219  xlimpnfvlem1  46223  cncfperiod  46266  icccncfext  46274  cncfiooicclem1  46280  dvbdfbdioolem1  46315  dvnmptdivc  46325  dvdsn1add  46326  dvnmptconst  46328  dvnmul  46330  dvmptfprodlem  46331  dvmptfprod  46332  dvnprodlem2  46334  iblspltprt  46360  itgsubsticclem  46362  itgspltprt  46366  itgsbtaddcnst  46369  stoweidlem3  46390  stoweidlem16  46403  stoweidlem17  46404  stoweidlem19  46406  stoweidlem20  46407  stoweidlem23  46410  stoweidlem25  46412  stoweidlem27  46414  stoweidlem31  46418  stoweidlem34  46421  stoweidlem42  46429  stoweidlem48  46435  stoweidlem51  46438  stoweidlem52  46439  stoweidlem59  46446  wallispilem1  46452  wallispilem3  46454  stirlinglem13  46473  fourierdlem16  46510  fourierdlem20  46514  fourierdlem21  46515  fourierdlem38  46532  fourierdlem42  46536  fourierdlem46  46539  fourierdlem48  46541  fourierdlem49  46542  fourierdlem50  46543  fourierdlem54  46547  fourierdlem68  46561  fourierdlem72  46565  fourierdlem73  46566  fourierdlem76  46569  fourierdlem79  46572  fourierdlem81  46574  fourierdlem86  46579  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem92  46585  fourierdlem97  46590  fourierdlem101  46594  fourierdlem103  46596  fourierdlem104  46597  fourierdlem111  46604  etransclem24  46645  etransclem25  46646  etransclem28  46649  etransclem41  46662  etransclem44  46665  etransclem48  46669  salexct  46721  dfsalgen2  46728  sge0f1o  46769  sge0rnbnd  46780  sge0split  46796  sge0iunmptlemre  46802  sge0fodjrnlem  46803  sge0iunmpt  46805  nnfoctbdjlem  46842  iundjiunlem  46846  meadjiunlem  46852  ismeannd  46854  meaiuninclem  46867  omeiunle  46904  carageniuncllem1  46908  caratheodorylem1  46913  hoidmvlelem4  46985  hoiqssbllem2  47010  salpreimagelt  47094  salpreimalegt  47096  pimdecfgtioc  47102  smfaddlem2  47151  smflimlem6  47163  nsssmfmbflem  47165  smfpimcclem  47194  ormkglobd  47262  or2expropbilem1  47421  funressndmfvrn  47433  f1cof1b  47466  2leaddle2  47687  smonoord  47760  uniimaprimaeqfv  47771  fundcmpsurbijinjpreimafv  47796  fundcmpsurinjALT  47801  iccpartf  47820  ich2exprop  47860  ichnreuop  47861  ichreuopeq  47862  sprbisymrel  47888  fmtnodvds  47933  proththdlem  48002  gbowgt5  48151  gboge9  48153  gbege6  48154  stgoldbwt  48165  sbgoldbalt  48170  bgoldbnnsum3prm  48193  grimgrtri  48338  grlimgrtri  48392  grlicsym  48402  clnbgr3stgrgrlim  48408  clnbgr3stgrgrlic  48409  gpg5gricstgr3  48479  uspgrbisymrelALT  48544  ssnn0ssfz  48738  ldepspr  48862  seposep  49314  upeu  49559  subthinc  49831  prsthinc  49852  iunord  50064  bnd2d  50069  setrecsss  50089