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  584  aevlem0  2054  equvel  2461  elex2OLD  3505  elex22  3506  spcedv  3598  rspcdf  3609  rspcdva  3623  rspc3dv  3641  spsbcd  3802  opth  5481  euotd  5518  wereu2  5682  unielrel  6294  frpomin  6361  tz7.7  6410  funmo  6581  funmoOLD  6582  fvelimad  6976  iinpreima  7089  fompt  7138  fnfvima  7253  resfvresima  7255  fliftfun  7332  fliftval  7336  weniso  7374  riota5f  7416  riotass2  7418  fovcld  7560  ofmpteq  7720  ssorduni  7799  sucexeloniOLD  7830  suceloniOLD  7832  nlimsucg  7863  tfisi  7880  zfrep6  7979  curry1  8129  curry2  8132  fnwelem  8156  funsssuppss  8215  frrlem4  8314  frrlem8  8318  frrlem10  8320  fprlem1  8325  fprlem2  8326  wfrlem4OLD  8352  smogt  8407  tfrlem5  8420  omeulem1  8620  oeworde  8631  oelimcl  8638  oeeulem  8639  oeeui  8640  nnawordex  8675  oaabs2  8687  naddssim  8723  naddsuc2  8739  swoso  8779  qliftlem  8838  resixp  8973  domssl  9038  domssr  9039  undomOLD  9100  xpdom3  9110  domunsncan  9112  omxpenlem  9113  domssex  9178  xpf1o  9179  mapdom3  9189  dif1en  9200  findcard  9203  f1dmvrnfibi  9381  fsuppss  9423  fiin  9462  marypha1lem  9473  marypha1  9474  fisupcl  9509  supgtoreq  9510  ordiso2  9555  ordtypelem2  9559  ordtypelem8  9565  wemapso2lem  9592  unxpwdom2  9628  cantnflt  9712  cantnfrescl  9716  oemapvali  9724  cantnflem1d  9728  wemapwe  9737  cnfcom  9740  ttrclss  9760  ttrclselem2  9766  frrlem15  9797  rankr1id  9902  tcrank  9924  cardmin2  10039  infxpenlem  10053  fseqen  10067  ween  10075  ac5num  10076  indcardi  10081  acni2  10086  fodomfi2  10100  infpwfien  10102  inffien  10103  iunfictbso  10154  acacni  10181  dfac12lem2  10185  djuinf  10229  infmap2  10257  ackbij1lem18  10276  ackbij1b  10278  fictb  10284  cfslb2n  10308  cofsmo  10309  cfsmolem  10310  coftr  10313  infpssrlem4  10346  domfin4  10351  fin2i2  10358  isfin2-2  10359  fincssdom  10363  ssfin3ds  10370  fin23lem20  10377  fin23lem30  10382  isf32lem3  10395  fin1a2lem12  10451  fin1a2lem13  10452  hsmexlem2  10467  axdc2lem  10488  imadomg  10574  fnct  10577  iundom2g  10580  iundomg  10581  iundom  10582  unirnfdomd  10607  konigthlem  10608  iunctb  10614  fpwwe2  10683  canthwelem  10690  pwfseqlem3  10700  pwfseqlem5  10703  winalim2  10736  wunelss  10748  r1wunlim  10777  wunex2  10778  tsksdom  10796  tskinf  10809  inttsk  10814  inar1  10815  tskcard  10821  tskurn  10829  gruina  10858  grur1a  10859  grur1  10860  addsrpr  11115  mulsrpr  11116  lemul12a  12125  lemulge11  12130  lediv12a  12161  fiminre2  12216  nngt0  12297  nn0ge2m1nn  12596  peano5uzi  12707  nn0ind-raph  12718  znnn0nn  12729  suprzub  12981  uzsupss  12982  rpge0  13048  fz0fzelfz0  13674  fz0fzdiffz0  13677  ige2m2fzo  13767  elfzodifsumelfzo  13770  elfzom1elp1fzo  13771  fzonfzoufzol  13809  flltdivnn0lt  13873  fldiv  13900  modaddmodup  13975  uzrdgsuci  14001  fzennn  14009  uzindi  14023  fsuppmapnn0fiubex  14033  expcl2lem  14114  leexp1a  14215  modexp  14277  faclbnd  14329  faclbnd6  14338  facavg  14340  hashginv  14373  hashf1rn  14391  hasheqf1od  14392  seqcoll  14503  hashge2el2dif  14519  wrdsymb0  14587  wrdlenge2n0  14590  ccatsymb  14620  swrdnd2  14693  swrdnd0  14695  pfxnd  14725  pfxccat1  14740  swrdpfx  14745  pfxpfx  14746  wrd2ind  14761  pfxccatin12  14771  pfxccat3  14772  swrdccat  14773  pfxccatpfx1  14774  pfxccatpfx2  14775  swrdccatin1d  14781  pfxccatin12d  14783  repswswrd  14822  cshwidxmod  14841  s2f1o  14955  f1oun2prg  14956  wwlktovfo  14997  relexpfld  15088  rtrclreclem3  15099  resqrex  15289  cau3lem  15393  reusq0  15501  rlimcld2  15614  climcn2  15629  isercoll  15704  climsup  15706  caurcvgr  15710  sumeq2ii  15729  summolem3  15750  zsum  15754  fsumadd  15776  fsumsplit1  15781  fsum2dlem  15806  fsum0diag2  15819  fsummulc2  15820  fsumabs  15837  fsumrelem  15843  fsumrlim  15847  fsumo1  15848  o1fsum  15849  fsumiun  15857  qshash  15863  prodeq2ii  15947  prodmolem3  15969  fprodmul  15996  fproddiv  15997  fprod2dlem  16016  fprodsplit1f  16026  sin02gt0  16228  efieq1re  16235  p1modz1  16297  dvdsleabs2  16349  4dvdseven  16410  sumeven  16424  sumodd  16425  divalglem9  16438  smupvallem  16520  algfx  16617  eucalgcvga  16623  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmflefac  16685  qredeq  16694  dvdszzq  16758  fermltl  16821  modprm0  16843  pythagtriplem4  16857  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem12  16864  pythagtriplem13  16865  pythagtriplem14  16866  pythagtriplem16  16868  difsqpwdvds  16925  pcmpt  16930  prmreclem2  16955  4sqlem11  16993  vdwlem9  17027  vdwlem11  17029  vdwlem12  17030  0ram  17058  0ram2  17059  0ramcl  17061  ramcl  17067  prmolelcmf  17086  cshwsidrepsw  17131  cshwshashlem2  17134  prmlem1  17145  prmlem2  17157  strfvd  17237  strfv2d  17238  strssd  17242  firest  17477  prdsdsval3  17530  imasbas  17557  imasds  17558  imasaddfnlem  17573  imasaddvallem  17574  imasvscafn  17582  qusaddvallem  17596  qusaddflem  17597  qusaddval  17598  qusaddf  17599  qusmulval  17600  qusmulf  17601  catideu  17718  idinv  17833  brcici  17844  invfuc  18022  2initoinv  18055  initoeu1w  18057  initoeu2lem0  18058  2termoinv  18062  termoeu1w  18064  mod2ile  18539  lubss  18558  acsmapd  18599  lidrididd  18683  gsumval2a  18698  mndind  18841  submefmnd  18908  mgm2nsgrplem4  18934  qusgrp2  19076  mulgnegnn  19102  pgrpsubgsymg  19427  fvcosymgeq  19447  gsmsymgreqlem1  19448  psgnunilem4  19515  pgpssslw  19632  sylow2alem2  19636  fislw  19643  efgsres  19756  rinvmod  19824  gsumval3lem2  19924  gsumzaddlem  19939  gsum2d  19990  nn0gsumfz  20002  telgsums  20011  dprddomcld  20021  ablfac2  20109  qusrng  20177  srgdilem  20189  o2timesd  20207  rglcom4d  20208  ringdilem  20246  qusring2  20331  lssintcl  20962  lbsextlem3  21162  lbsextlem4  21163  zringlpirlem3  21475  psgnodpm  21606  psgndiflemB  21618  frlmup4  21821  lindff1  21840  lindfrn  21841  lmisfree  21862  evlseu  22107  mhpmulcl  22153  mptcoe1fsupp  22217  cply1coe0bi  22306  mpfpf1  22355  pf1mpf  22356  mat0dimscm  22475  mdetdiagid  22606  mdet1  22607  mdetunilem9  22626  slesolinv  22686  cramerimp  22692  cpmatmcllem  22724  mptcoe1matfsupp  22808  mp2pm2mp  22817  chpdmat  22847  cctop  23013  subbascn  23262  cnss2  23285  cmpcovf  23399  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  comppfsc  23540  ptclsg  23623  dfac14  23626  txcnp  23628  ptcnplem  23629  uptx  23633  txtube  23648  tx2ndc  23659  xkococnlem  23667  elqtop  23705  qtoprest  23725  indishmph  23806  ptcmpfi  23821  kqhmph  23827  csdfil  23902  filssufilg  23919  ufilen  23938  rnelfm  23961  fmfnfmlem4  23965  alexsubALTlem4  24058  ptcmplem4  24063  cnextfvval  24073  cnextcn  24075  cnextfres  24077  tmdgsum2  24104  imasf1oxmet  24385  metss  24521  met2ndci  24535  prdsxmslem2  24542  metust  24571  cfilucfil  24572  metustbl  24579  psmetutop  24580  opnreen  24853  rectbntr0  24854  fsumcn  24894  rescncf  24923  xrhmeo  24977  cnllycmp  24988  lebnumlem1  24993  lebnumlem3  24995  cfilss  25304  iscmet3lem1  25325  iscmet3lem2  25326  ivthicc  25493  ovolsslem  25519  ovoliunlem2  25538  ovoliunnul  25542  ovolicc2lem4  25555  voliunlem3  25587  volsup  25591  uniiccdif  25613  uniioombllem2  25618  volivth  25642  mbfimaopnlem  25690  mbflimsup  25701  i1fd  25716  itg1addlem4  25734  itg2addlem  25793  itg2gt0  25795  limciun  25929  dvadd  25977  dvmul  25978  dvco  25985  dvrec  25993  dvcnv  26015  dvferm  26026  rollelem  26027  dvlip  26032  dvlip2  26034  c1liplem1  26035  c1lip2  26037  dvgt0lem1  26041  dvivthlem1  26047  lhop1lem  26052  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsumrlim2  26073  dvfsum2  26075  ftc1cn  26084  ftc2ditglem  26086  itgsubstlem  26089  itgpowd  26091  mdegaddle  26113  mdegmullem  26117  deg1sublt  26149  ply1divmo  26175  fta1g  26209  dgrub  26273  dgrnznn  26286  dgradd2  26308  dvply1  26325  plyrem  26347  aalioulem4  26377  aalioulem5  26378  aalioulem6  26379  aaliou2  26382  taylf  26402  ulmdv  26446  psercn2  26466  psercn2OLD  26467  abelth  26485  abelth2  26486  reeff1olem  26490  efopn  26700  logreclem  26805  isosctrlem2  26862  xrlimcnp  27011  basellem4  27127  ppiwordi  27205  musum  27234  chpub  27264  gausslemma2dlem0c  27402  2sqlem6  27467  addsqnreup  27487  2sqreulem1  27490  2sqreunnlem1  27493  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  pntlemp  27654  pntleml  27655  ostth3  27682  sltres  27707  noextenddif  27713  nolesgn2ores  27717  nogesgn1ores  27719  nosep1o  27726  nosep2o  27727  nosepeq  27730  nolt02o  27740  noresle  27742  nosupno  27748  nosupbday  27750  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfres  27767  noinfbnd1lem5  27772  noinfbnd1  27774  noinfbnd2lem1  27775  sltled  27814  madebday  27938  sleadd1  28022  precsexlem10  28240  noseqrdg0  28313  noseqrdgsuc  28314  elnnzs  28387  iscgrglt  28522  colline  28657  axlowdimlem16  28972  axlowdimlem17  28973  axcontlem3  28981  axcontlem10  28988  uhgr2edg  29225  nbupgruvtxres  29424  cusgrres  29466  cusgrfilem2  29474  vdumgr0  29498  frusgrnn0  29589  wlkp1lem8  29698  pthdivtx  29747  upgrwlkdvde  29757  spthonepeq  29772  usgr2pthlem  29783  cyclnumvtx  29820  lfgrn1cycl  29825  wwlknbp1  29864  wwlknllvtx  29866  wlkiswwlks2lem3  29891  umgr2adedgspth  29968  clwlkclwwlklem3  30020  clwwisshclwwslemlem  30032  clwwisshclwws  30034  clwwlkel  30065  wwlksubclwwlk  30077  eleclclwwlknlem1  30079  eleclclwwlknlem2  30080  erclwwlknref  30088  clwwlknonccat  30115  clwwlknonex2lem2  30127  3wlkdlem4  30181  vdn0conngrumgrv2  30215  eucrctshift  30262  frgrnbnb  30312  frgrncvvdeqlem2  30319  frgrncvvdeqlem3  30320  fusgreghash2wspv  30354  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwwlk5  30407  numclwwlk7  30410  frgrreggt1  30412  minvecolem4b  30897  minvecolem4  30899  bcsiALT  31198  ococin  31427  spanpr  31599  pjorthi  31688  nmbdoplbi  32043  nmcoplbi  32047  nmbdfnlbi  32068  nmcfnlbi  32071  nmopcoi  32114  branmfn  32124  hstnmoc  32242  mdsl0  32329  atomli  32401  atcvat4i  32416  atabsi  32420  foresf1o  32523  rabfodom  32524  abrexdomjm  32526  elpreq  32548  ifeqeqx  32555  disjiunel  32609  ac6mapd  32635  aciunf1lem  32672  ffsrn  32740  xlt2addrd  32762  supxrnemnf  32772  ssnnssfz  32789  resspos  32956  resstos  32957  chnso  33004  gsummptres2  33056  gsumfs2d  33058  archirngz  33196  orngsqr  33334  isarchiofld  33347  unitprodclb  33417  elrspunidl  33456  drngidlhash  33462  prmidl2  33469  qsidomlem2  33481  ssmxidl  33502  1arithidom  33565  1arithufdlem4  33575  constrmon  33785  locfinreflem  33839  cmpcref  33849  fmcncfil  33930  xrge0iifiso  33934  elzdif0  33981  qqhval2lem  33982  esumcst  34064  esumrnmpt2  34069  esumpinfval  34074  esumpinfsum  34078  sigaclci  34133  insiga  34138  ldgenpisys  34167  measres  34223  measdivcstALTV  34226  dya2iocnrect  34283  dya2iocnei  34284  omssubadd  34302  carsggect  34320  carsgclctunlem2  34321  sitgclg  34344  eulerpartlemsv2  34360  eulerpartlemv  34366  eulerpartlemf  34372  eulerpartlemgh  34380  eulerpartlemgs2  34382  ballotlemfp1  34494  ballotlemfrcn0  34532  ftc2re  34613  fdvposlt  34614  fdvposle  34616  bnj1379  34844  bnj580  34927  bnj944  34952  bnj999  34972  bnj1204  35026  bnj1398  35048  cusgredgex  35127  pthacycspth  35162  derangenlem  35176  subfacp1lem3  35187  resconn  35251  cvmliftlem3  35292  satfv0fvfmla0  35418  satfv1fvfmla1  35428  mrsub0  35521  cgrextend  36009  segconeq  36011  trisegint  36029  fwddifnp1  36166  ivthALT  36336  fnessref  36358  refssfne  36359  neibastop1  36360  filnetlem4  36382  ontgval  36432  weiunlem2  36464  weiunse  36469  unblimceq0lem  36507  unbdqndv2lem2  36511  unbdqndv2  36512  bj-babygodel  36604  bj-alrimd  36621  bj-exlimd  36626  bj-spcimdv  36896  bj-spcimdvv  36897  bj-finsumval0  37286  bj-fvimacnv0  37287  dfgcd3  37325  relowlssretop  37364  relowlpssretop  37365  onsucuni3  37368  finxpreclem4  37395  poimirlem18  37645  poimirlem21  37648  poimirlem25  37652  ftc1cnnclem  37698  ftc1cnnc  37699  ftc2nc  37709  dvasin  37711  dvacos  37712  abrexdom  37737  indexdom  37741  mettrifi  37764  equivtotbnd  37785  totbndbnd  37796  prdstotbnd  37801  heibor1lem  37816  bfplem1  37829  bfplem2  37830  opidonOLD  37859  rngodm1dm2  37939  zerdivemp1x  37954  equid1  38900  omllaw5N  39248  cmtcomlemN  39249  cmtbr3N  39255  omlfh3N  39260  atlen0  39311  exatleN  39406  hlrelat3  39414  cvrexchlem  39421  atlelt  39440  cvrat4  39445  4atlem11b  39610  4atlem12b  39613  lneq2at  39780  cdlema1N  39793  cdlemblem  39795  paddss12  39821  paddasslem2  39823  paddasslem4  39825  paddasslem6  39827  paddasslem12  39833  paddunN  39929  poml4N  39955  poml5N  39956  osumcllem6N  39963  pexmidlem6N  39977  pl42lem2N  39982  ltrnu  40123  ltrneq2  40150  trlval2  40165  cdlemd6  40205  cdleme25b  40356  cdleme29b  40377  cdlemefr29exN  40404  ltrniotacnvval  40584  cdlemk28-3  40910  dochexmidlem7  41468  muldvds2d  41999  frlmsnic  42550  nna4b4nsq  42670  mzpsubmpt  42754  mzpsubst  42759  eqrabdioph  42788  rabdiophlem2  42813  elpell14qr2  42873  elpell1qr2  42883  pellfundre  42892  pellfundge  42893  pellfundglb  42896  pellfund14gap  42898  congabseq  42986  jm2.22  43007  jm2.23  43008  jm2.26lem3  43013  wepwsolem  43054  dnwech  43060  aomclem2  43067  aomclem4  43069  pwfi2f1o  43108  onexlimgt  43255  oaltublim  43303  oege1  43319  cantnfub2  43335  cantnfresb  43337  cantnf2  43338  oacl2g  43343  tfsconcatb0  43357  tfsconcatrev  43361  oaun3lem1  43387  oaun3lem2  43388  nadd2rabtr  43397  nadd1suc  43405  naddwordnexlem0  43409  naddwordnexlem3  43412  oawordex3  43413  naddwordnexlem4  43414  oaltom  43418  omltoe  43420  ss2iundf  43672  dssmapf1od  44034  neik0pk1imk0  44060  gneispace  44147  grur1cld  44251  cpcolld  44277  mnuop23d  44285  mnuprdlem1  44291  mnuprdlem2  44292  mnurndlem1  44300  grumnudlem  44304  radcnvrat  44333  sbiota1  44453  ordelordALT  44557  2pm13.193  44572  ee11an  44710  modelaxreplem2  44996  refsumcn  45035  rfcnnnub  45041  disjxp1  45074  xrnmnfpnf  45088  ssinc  45092  nssd  45110  disjf1o  45196  disjinfi  45197  choicefi  45205  axccdom  45227  dmrelrnrel  45231  monoords  45309  fperiodmullem  45315  xadd0ge  45332  xrssre  45359  xrlexaddrp  45363  xrred  45376  infxr  45378  xrnpnfmnf  45485  monoordxrv  45492  monoord2xrv  45494  cvgcaule  45502  fsumiunss  45590  fmul01  45595  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  cncfmptss  45602  climinf  45621  climsuselem1  45622  climsuse  45623  limcperiod  45643  limcrecl  45644  sumnnodd  45645  limcleqr  45659  0ellimcdiv  45664  climleltrp  45691  limsuppnfdlem  45716  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  cnrefiisplem  45844  xlimmnfvlem1  45847  xlimpnfvlem1  45851  cncfperiod  45894  icccncfext  45902  cncfiooicclem1  45908  dvbdfbdioolem1  45943  dvnmptdivc  45953  dvdsn1add  45954  dvnmptconst  45956  dvnmul  45958  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem2  45962  iblspltprt  45988  itgsubsticclem  45990  itgspltprt  45994  itgsbtaddcnst  45997  stoweidlem3  46018  stoweidlem16  46031  stoweidlem17  46032  stoweidlem19  46034  stoweidlem20  46035  stoweidlem23  46038  stoweidlem25  46040  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  stoweidlem42  46057  stoweidlem48  46063  stoweidlem51  46066  stoweidlem52  46067  stoweidlem59  46074  wallispilem1  46080  wallispilem3  46082  stirlinglem13  46101  fourierdlem16  46138  fourierdlem20  46142  fourierdlem21  46143  fourierdlem38  46160  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem54  46175  fourierdlem68  46189  fourierdlem72  46193  fourierdlem73  46194  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem86  46207  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  etransclem24  46273  etransclem25  46274  etransclem28  46277  etransclem41  46290  etransclem44  46293  etransclem48  46297  salexct  46349  dfsalgen2  46356  sge0f1o  46397  sge0rnbnd  46408  sge0split  46424  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0iunmpt  46433  nnfoctbdjlem  46470  iundjiunlem  46474  meadjiunlem  46480  ismeannd  46482  meaiuninclem  46495  omeiunle  46532  carageniuncllem1  46536  caratheodorylem1  46541  hoidmvlelem4  46613  hoiqssbllem2  46638  salpreimagelt  46722  salpreimalegt  46724  pimdecfgtioc  46730  smfaddlem2  46779  smflimlem6  46791  nsssmfmbflem  46793  smfpimcclem  46822  ormkglobd  46890  or2expropbilem1  47044  funressndmfvrn  47056  f1cof1b  47089  2leaddle2  47310  smonoord  47358  uniimaprimaeqfv  47369  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjALT  47399  iccpartf  47418  ich2exprop  47458  ichnreuop  47459  ichreuopeq  47460  sprbisymrel  47486  fmtnodvds  47531  proththdlem  47600  gbowgt5  47749  gboge9  47751  gbege6  47752  stgoldbwt  47763  sbgoldbalt  47768  bgoldbnnsum3prm  47791  grimgrtri  47916  grlimgrtri  47963  grlicsym  47973  clnbgr3stgrgrlic  47979  gpg5gricstgr3  48046  uspgrbisymrelALT  48071  ssnn0ssfz  48265  ldepspr  48390  seposep  48823  upeu  48928  subthinc  49092  prsthinc  49111  iunord  49195  bnd2d  49200  setrecsss  49220