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  2460  elex2OLD  3484  elex22  3485  spcedv  3577  rspcdf  3588  rspcdva  3602  rspc3dv  3620  spsbcd  3779  opth  5451  euotd  5488  wereu2  5651  unielrel  6263  frpomin  6329  tz7.7  6378  funmo  6550  funmoOLD  6551  fvelimad  6945  iinpreima  7058  fompt  7107  fnfvima  7224  resfvresima  7226  fliftfun  7304  fliftval  7308  weniso  7346  riota5f  7388  riotass2  7390  fovcld  7532  ofmpteq  7692  ssorduni  7771  sucexeloniOLD  7802  suceloniOLD  7804  nlimsucg  7835  tfisi  7852  zfrep6  7951  curry1  8101  curry2  8104  fnwelem  8128  funsssuppss  8187  frrlem4  8286  frrlem8  8290  frrlem10  8292  fprlem1  8297  fprlem2  8298  wfrlem4OLD  8324  smogt  8379  tfrlem5  8392  omeulem1  8592  oeworde  8603  oelimcl  8610  oeeulem  8611  oeeui  8612  nnawordex  8647  oaabs2  8659  naddssim  8695  naddsuc2  8711  swoso  8751  qliftlem  8810  resixp  8945  domssl  9010  domssr  9011  undomOLD  9072  xpdom3  9082  domunsncan  9084  omxpenlem  9085  domssex  9150  xpf1o  9151  mapdom3  9161  dif1en  9172  findcard  9175  f1dmvrnfibi  9351  fsuppss  9393  fiin  9432  marypha1lem  9443  marypha1  9444  fisupcl  9480  supgtoreq  9481  ordiso2  9527  ordtypelem2  9531  ordtypelem8  9537  wemapso2lem  9564  unxpwdom2  9600  cantnflt  9684  cantnfrescl  9688  oemapvali  9696  cantnflem1d  9700  wemapwe  9709  cnfcom  9712  ttrclss  9732  ttrclselem2  9738  frrlem15  9769  rankr1id  9874  tcrank  9896  cardmin2  10011  infxpenlem  10025  fseqen  10039  ween  10047  ac5num  10048  indcardi  10053  acni2  10058  fodomfi2  10072  infpwfien  10074  inffien  10075  iunfictbso  10126  acacni  10153  dfac12lem2  10157  djuinf  10201  infmap2  10229  ackbij1lem18  10248  ackbij1b  10250  fictb  10256  cfslb2n  10280  cofsmo  10281  cfsmolem  10282  coftr  10285  infpssrlem4  10318  domfin4  10323  fin2i2  10330  isfin2-2  10331  fincssdom  10335  ssfin3ds  10342  fin23lem20  10349  fin23lem30  10354  isf32lem3  10367  fin1a2lem12  10423  fin1a2lem13  10424  hsmexlem2  10439  axdc2lem  10460  imadomg  10546  fnct  10549  iundom2g  10552  iundomg  10553  iundom  10554  unirnfdomd  10579  konigthlem  10580  iunctb  10586  fpwwe2  10655  canthwelem  10662  pwfseqlem3  10672  pwfseqlem5  10675  winalim2  10708  wunelss  10720  r1wunlim  10749  wunex2  10750  tsksdom  10768  tskinf  10781  inttsk  10786  inar1  10787  tskcard  10793  tskurn  10801  gruina  10830  grur1a  10831  grur1  10832  addsrpr  11087  mulsrpr  11088  lemul12a  12097  lemulge11  12102  lediv12a  12133  fiminre2  12188  nngt0  12269  nn0ge2m1nn  12569  peano5uzi  12680  nn0ind-raph  12691  znnn0nn  12702  suprzub  12953  uzsupss  12954  rpge0  13020  fz0fzelfz0  13649  fz0fzdiffz0  13652  ige2m2fzo  13742  elfzodifsumelfzo  13745  elfzom1elp1fzo  13746  fzonfzoufzol  13784  flltdivnn0lt  13848  fldiv  13875  modaddmodup  13950  uzrdgsuci  13976  fzennn  13984  uzindi  13998  fsuppmapnn0fiubex  14008  expcl2lem  14089  leexp1a  14191  modexp  14254  faclbnd  14306  faclbnd6  14315  facavg  14317  hashginv  14350  hashf1rn  14368  hasheqf1od  14369  seqcoll  14480  hashge2el2dif  14496  wrdsymb0  14565  wrdlenge2n0  14568  ccatsymb  14598  swrdnd2  14671  swrdnd0  14673  pfxnd  14703  pfxccat1  14718  swrdpfx  14723  pfxpfx  14724  wrd2ind  14739  pfxccatin12  14749  pfxccat3  14750  swrdccat  14751  pfxccatpfx1  14752  pfxccatpfx2  14753  swrdccatin1d  14759  pfxccatin12d  14761  repswswrd  14800  cshwidxmod  14819  s2f1o  14933  f1oun2prg  14934  wwlktovfo  14975  relexpfld  15066  rtrclreclem3  15077  resqrex  15267  cau3lem  15371  reusq0  15479  rlimcld2  15592  climcn2  15607  isercoll  15682  climsup  15684  caurcvgr  15688  sumeq2ii  15707  summolem3  15728  zsum  15732  fsumadd  15754  fsumsplit1  15759  fsum2dlem  15784  fsum0diag2  15797  fsummulc2  15798  fsumabs  15815  fsumrelem  15821  fsumrlim  15825  fsumo1  15826  o1fsum  15827  fsumiun  15835  qshash  15841  prodeq2ii  15925  prodmolem3  15947  fprodmul  15974  fproddiv  15975  fprod2dlem  15994  fprodsplit1f  16004  sin02gt0  16208  efieq1re  16215  p1modz1  16277  dvdsleabs2  16329  4dvdseven  16390  sumeven  16404  sumodd  16405  divalglem9  16418  smupvallem  16500  algfx  16597  eucalgcvga  16603  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmflefac  16665  qredeq  16674  dvdszzq  16738  fermltl  16801  modprm0  16823  pythagtriplem4  16837  pythagtriplem6  16839  pythagtriplem7  16840  pythagtriplem12  16844  pythagtriplem13  16845  pythagtriplem14  16846  pythagtriplem16  16848  difsqpwdvds  16905  pcmpt  16910  prmreclem2  16935  4sqlem11  16973  vdwlem9  17007  vdwlem11  17009  vdwlem12  17010  0ram  17038  0ram2  17039  0ramcl  17041  ramcl  17047  prmolelcmf  17066  cshwsidrepsw  17111  cshwshashlem2  17114  prmlem1  17125  prmlem2  17137  strfvd  17217  strfv2d  17218  strssd  17222  firest  17444  prdsdsval3  17497  imasbas  17524  imasds  17525  imasaddfnlem  17540  imasaddvallem  17541  imasvscafn  17549  qusaddvallem  17563  qusaddflem  17564  qusaddval  17565  qusaddf  17566  qusmulval  17567  qusmulf  17568  catideu  17685  idinv  17800  brcici  17811  invfuc  17988  2initoinv  18021  initoeu1w  18023  initoeu2lem0  18024  2termoinv  18028  termoeu1w  18030  mod2ile  18502  lubss  18521  acsmapd  18562  lidrididd  18646  gsumval2a  18661  mndind  18804  submefmnd  18871  mgm2nsgrplem4  18897  qusgrp2  19039  mulgnegnn  19065  pgrpsubgsymg  19388  fvcosymgeq  19408  gsmsymgreqlem1  19409  psgnunilem4  19476  pgpssslw  19593  sylow2alem2  19597  fislw  19604  efgsres  19717  rinvmod  19785  gsumval3lem2  19885  gsumzaddlem  19900  gsum2d  19951  nn0gsumfz  19963  telgsums  19972  dprddomcld  19982  ablfac2  20070  qusrng  20138  srgdilem  20150  o2timesd  20168  rglcom4d  20169  ringdilem  20207  qusring2  20292  lssintcl  20919  lbsextlem3  21119  lbsextlem4  21120  zringlpirlem3  21423  psgnodpm  21546  psgndiflemB  21558  frlmup4  21759  lindff1  21778  lindfrn  21779  lmisfree  21800  evlseu  22039  mhpmulcl  22085  mptcoe1fsupp  22149  cply1coe0bi  22238  mpfpf1  22287  pf1mpf  22288  mat0dimscm  22405  mdetdiagid  22536  mdet1  22537  mdetunilem9  22556  slesolinv  22616  cramerimp  22622  cpmatmcllem  22654  mptcoe1matfsupp  22738  mp2pm2mp  22747  chpdmat  22777  cctop  22942  subbascn  23190  cnss2  23213  cmpcovf  23327  2ndcctbss  23391  2ndcomap  23394  2ndcsep  23395  comppfsc  23468  ptclsg  23551  dfac14  23554  txcnp  23556  ptcnplem  23557  uptx  23561  txtube  23576  tx2ndc  23587  xkococnlem  23595  elqtop  23633  qtoprest  23653  indishmph  23734  ptcmpfi  23749  kqhmph  23755  csdfil  23830  filssufilg  23847  ufilen  23866  rnelfm  23889  fmfnfmlem4  23893  alexsubALTlem4  23986  ptcmplem4  23991  cnextfvval  24001  cnextcn  24003  cnextfres  24005  tmdgsum2  24032  imasf1oxmet  24312  metss  24445  met2ndci  24459  prdsxmslem2  24466  metust  24495  cfilucfil  24496  metustbl  24503  psmetutop  24504  opnreen  24769  rectbntr0  24770  fsumcn  24810  rescncf  24839  xrhmeo  24893  cnllycmp  24904  lebnumlem1  24909  lebnumlem3  24911  cfilss  25220  iscmet3lem1  25241  iscmet3lem2  25242  ivthicc  25409  ovolsslem  25435  ovoliunlem2  25454  ovoliunnul  25458  ovolicc2lem4  25471  voliunlem3  25503  volsup  25507  uniiccdif  25529  uniioombllem2  25534  volivth  25558  mbfimaopnlem  25606  mbflimsup  25617  i1fd  25632  itg1addlem4  25650  itg2addlem  25709  itg2gt0  25711  limciun  25845  dvadd  25893  dvmul  25894  dvco  25901  dvrec  25909  dvcnv  25931  dvferm  25942  rollelem  25943  dvlip  25948  dvlip2  25950  c1liplem1  25951  c1lip2  25953  dvgt0lem1  25957  dvivthlem1  25963  lhop1lem  25968  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem4  25986  dvfsumrlim2  25989  dvfsum2  25991  ftc1cn  26000  ftc2ditglem  26002  itgsubstlem  26005  itgpowd  26007  mdegaddle  26029  mdegmullem  26033  deg1sublt  26065  ply1divmo  26091  fta1g  26125  dgrub  26189  dgrnznn  26202  dgradd2  26224  dvply1  26241  plyrem  26263  aalioulem4  26293  aalioulem5  26294  aalioulem6  26295  aaliou2  26298  taylf  26318  ulmdv  26362  psercn2  26382  psercn2OLD  26383  abelth  26401  abelth2  26402  reeff1olem  26406  efopn  26617  logreclem  26722  isosctrlem2  26779  xrlimcnp  26928  basellem4  27044  ppiwordi  27122  musum  27151  chpub  27181  gausslemma2dlem0c  27319  2sqlem6  27384  addsqnreup  27404  2sqreulem1  27407  2sqreunnlem1  27410  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  pntlemp  27571  pntleml  27572  ostth3  27599  sltres  27624  noextenddif  27630  nolesgn2ores  27634  nogesgn1ores  27636  nosep1o  27643  nosep2o  27644  nosepeq  27647  nolt02o  27657  noresle  27659  nosupno  27665  nosupbday  27667  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem4  27673  nosupbnd1  27676  nosupbnd2lem1  27677  nosupbnd2  27678  noinfno  27680  noinfbday  27682  noinfres  27684  noinfbnd1lem5  27689  noinfbnd1  27691  noinfbnd2lem1  27692  sltled  27731  madebday  27855  sleadd1  27939  precsexlem10  28157  noseqrdg0  28230  noseqrdgsuc  28231  elnnzs  28304  iscgrglt  28439  colline  28574  axlowdimlem16  28882  axlowdimlem17  28883  axcontlem3  28891  axcontlem10  28898  uhgr2edg  29133  nbupgruvtxres  29332  cusgrres  29374  cusgrfilem2  29382  vdumgr0  29406  frusgrnn0  29497  wlkp1lem8  29606  pthdivtx  29655  upgrwlkdvde  29665  spthonepeq  29680  usgr2pthlem  29691  cyclnumvtx  29728  lfgrn1cycl  29733  wwlknbp1  29772  wwlknllvtx  29774  wlkiswwlks2lem3  29799  umgr2adedgspth  29876  clwlkclwwlklem3  29928  clwwisshclwwslemlem  29940  clwwisshclwws  29942  clwwlkel  29973  wwlksubclwwlk  29985  eleclclwwlknlem1  29987  eleclclwwlknlem2  29988  erclwwlknref  29996  clwwlknonccat  30023  clwwlknonex2lem2  30035  3wlkdlem4  30089  vdn0conngrumgrv2  30123  eucrctshift  30170  frgrnbnb  30220  frgrncvvdeqlem2  30227  frgrncvvdeqlem3  30228  fusgreghash2wspv  30262  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwwlk5  30315  numclwwlk7  30318  frgrreggt1  30320  minvecolem4b  30805  minvecolem4  30807  bcsiALT  31106  ococin  31335  spanpr  31507  pjorthi  31596  nmbdoplbi  31951  nmcoplbi  31955  nmbdfnlbi  31976  nmcfnlbi  31979  nmopcoi  32022  branmfn  32032  hstnmoc  32150  mdsl0  32237  atomli  32309  atcvat4i  32324  atabsi  32328  foresf1o  32431  rabfodom  32432  abrexdomjm  32434  elpreq  32455  ifeqeqx  32469  disjiunel  32523  ac6mapd  32549  aciunf1lem  32586  ffsrn  32652  xlt2addrd  32682  supxrnemnf  32691  ssnnssfz  32710  resspos  32892  resstos  32893  chnso  32940  gsummptres2  32993  gsumfs2d  32995  archirngz  33133  orngsqr  33272  isarchiofld  33285  unitprodclb  33350  elrspunidl  33389  drngidlhash  33395  prmidl2  33402  qsidomlem2  33414  ssmxidl  33435  1arithidom  33498  1arithufdlem4  33508  constrmon  33724  locfinreflem  33817  cmpcref  33827  fmcncfil  33908  xrge0iifiso  33912  elzdif0  33957  qqhval2lem  33958  esumcst  34040  esumrnmpt2  34045  esumpinfval  34050  esumpinfsum  34054  sigaclci  34109  insiga  34114  ldgenpisys  34143  measres  34199  measdivcstALTV  34202  dya2iocnrect  34259  dya2iocnei  34260  omssubadd  34278  carsggect  34296  carsgclctunlem2  34297  sitgclg  34320  eulerpartlemsv2  34336  eulerpartlemv  34342  eulerpartlemf  34348  eulerpartlemgh  34356  eulerpartlemgs2  34358  ballotlemfp1  34470  ballotlemfrcn0  34508  ftc2re  34576  fdvposlt  34577  fdvposle  34579  bnj1379  34807  bnj580  34890  bnj944  34915  bnj999  34935  bnj1204  34989  bnj1398  35011  cusgredgex  35090  pthacycspth  35125  derangenlem  35139  subfacp1lem3  35150  resconn  35214  cvmliftlem3  35255  satfv0fvfmla0  35381  satfv1fvfmla1  35391  mrsub0  35484  cgrextend  35972  segconeq  35974  trisegint  35992  fwddifnp1  36129  ivthALT  36299  fnessref  36321  refssfne  36322  neibastop1  36323  filnetlem4  36345  ontgval  36395  weiunlem2  36427  weiunse  36432  unblimceq0lem  36470  unbdqndv2lem2  36474  unbdqndv2  36475  bj-babygodel  36567  bj-alrimd  36584  bj-exlimd  36589  bj-spcimdv  36859  bj-spcimdvv  36860  bj-finsumval0  37249  bj-fvimacnv0  37250  dfgcd3  37288  relowlssretop  37327  relowlpssretop  37328  onsucuni3  37331  finxpreclem4  37358  poimirlem18  37608  poimirlem21  37611  poimirlem25  37615  ftc1cnnclem  37661  ftc1cnnc  37662  ftc2nc  37672  dvasin  37674  dvacos  37675  abrexdom  37700  indexdom  37704  mettrifi  37727  equivtotbnd  37748  totbndbnd  37759  prdstotbnd  37764  heibor1lem  37779  bfplem1  37792  bfplem2  37793  opidonOLD  37822  rngodm1dm2  37902  zerdivemp1x  37917  equid1  38863  omllaw5N  39211  cmtcomlemN  39212  cmtbr3N  39218  omlfh3N  39223  atlen0  39274  exatleN  39369  hlrelat3  39377  cvrexchlem  39384  atlelt  39403  cvrat4  39408  4atlem11b  39573  4atlem12b  39576  lneq2at  39743  cdlema1N  39756  cdlemblem  39758  paddss12  39784  paddasslem2  39786  paddasslem4  39788  paddasslem6  39790  paddasslem12  39796  paddunN  39892  poml4N  39918  poml5N  39919  osumcllem6N  39926  pexmidlem6N  39940  pl42lem2N  39945  ltrnu  40086  ltrneq2  40113  trlval2  40128  cdlemd6  40168  cdleme25b  40319  cdleme29b  40340  cdlemefr29exN  40367  ltrniotacnvval  40547  cdlemk28-3  40873  dochexmidlem7  41431  muldvds2d  41957  frlmsnic  42510  nna4b4nsq  42630  mzpsubmpt  42713  mzpsubst  42718  eqrabdioph  42747  rabdiophlem2  42772  elpell14qr2  42832  elpell1qr2  42842  pellfundre  42851  pellfundge  42852  pellfundglb  42855  pellfund14gap  42857  congabseq  42945  jm2.22  42966  jm2.23  42967  jm2.26lem3  42972  wepwsolem  43013  dnwech  43019  aomclem2  43026  aomclem4  43028  pwfi2f1o  43067  onexlimgt  43214  oaltublim  43261  oege1  43277  cantnfub2  43293  cantnfresb  43295  cantnf2  43296  oacl2g  43301  tfsconcatb0  43315  tfsconcatrev  43319  oaun3lem1  43345  oaun3lem2  43346  nadd2rabtr  43355  nadd1suc  43363  naddwordnexlem0  43367  naddwordnexlem3  43370  oawordex3  43371  naddwordnexlem4  43372  oaltom  43376  omltoe  43378  ss2iundf  43630  dssmapf1od  43992  neik0pk1imk0  44018  gneispace  44105  grur1cld  44204  cpcolld  44230  mnuop23d  44238  mnuprdlem1  44244  mnuprdlem2  44245  mnurndlem1  44253  grumnudlem  44257  radcnvrat  44286  sbiota1  44406  ordelordALT  44510  2pm13.193  44525  ee11an  44663  modelaxreplem2  44952  refsumcn  45002  rfcnnnub  45008  disjxp1  45041  xrnmnfpnf  45055  ssinc  45059  nssd  45077  disjf1o  45163  disjinfi  45164  choicefi  45172  axccdom  45194  dmrelrnrel  45198  monoords  45274  fperiodmullem  45280  xadd0ge  45296  xrssre  45323  xrlexaddrp  45327  xrred  45340  infxr  45342  xrnpnfmnf  45449  monoordxrv  45456  monoord2xrv  45458  cvgcaule  45466  fsumiunss  45552  fmul01  45557  fmuldfeqlem1  45559  fmuldfeq  45560  fmul01lt1lem1  45561  fmul01lt1lem2  45562  cncfmptss  45564  climinf  45583  climsuselem1  45584  climsuse  45585  limcperiod  45605  limcrecl  45606  sumnnodd  45607  limcleqr  45621  0ellimcdiv  45626  climleltrp  45653  limsuppnfdlem  45678  limsupresxr  45743  liminfresxr  45744  liminfvalxr  45760  cnrefiisplem  45806  xlimmnfvlem1  45809  xlimpnfvlem1  45813  cncfperiod  45856  icccncfext  45864  cncfiooicclem1  45870  dvbdfbdioolem1  45905  dvnmptdivc  45915  dvdsn1add  45916  dvnmptconst  45918  dvnmul  45920  dvmptfprodlem  45921  dvmptfprod  45922  dvnprodlem2  45924  iblspltprt  45950  itgsubsticclem  45952  itgspltprt  45956  itgsbtaddcnst  45959  stoweidlem3  45980  stoweidlem16  45993  stoweidlem17  45994  stoweidlem19  45996  stoweidlem20  45997  stoweidlem23  46000  stoweidlem25  46002  stoweidlem27  46004  stoweidlem31  46008  stoweidlem34  46011  stoweidlem42  46019  stoweidlem48  46025  stoweidlem51  46028  stoweidlem52  46029  stoweidlem59  46036  wallispilem1  46042  wallispilem3  46044  stirlinglem13  46063  fourierdlem16  46100  fourierdlem20  46104  fourierdlem21  46105  fourierdlem38  46122  fourierdlem42  46126  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem54  46137  fourierdlem68  46151  fourierdlem72  46155  fourierdlem73  46156  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem86  46169  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  etransclem24  46235  etransclem25  46236  etransclem28  46239  etransclem41  46252  etransclem44  46255  etransclem48  46259  salexct  46311  dfsalgen2  46318  sge0f1o  46359  sge0rnbnd  46370  sge0split  46386  sge0iunmptlemre  46392  sge0fodjrnlem  46393  sge0iunmpt  46395  nnfoctbdjlem  46432  iundjiunlem  46436  meadjiunlem  46442  ismeannd  46444  meaiuninclem  46457  omeiunle  46494  carageniuncllem1  46498  caratheodorylem1  46503  hoidmvlelem4  46575  hoiqssbllem2  46600  salpreimagelt  46684  salpreimalegt  46686  pimdecfgtioc  46692  smfaddlem2  46741  smflimlem6  46753  nsssmfmbflem  46755  smfpimcclem  46784  ormkglobd  46852  or2expropbilem1  47009  funressndmfvrn  47021  f1cof1b  47054  2leaddle2  47275  smonoord  47333  uniimaprimaeqfv  47344  fundcmpsurbijinjpreimafv  47369  fundcmpsurinjALT  47374  iccpartf  47393  ich2exprop  47433  ichnreuop  47434  ichreuopeq  47435  sprbisymrel  47461  fmtnodvds  47506  proththdlem  47575  gbowgt5  47724  gboge9  47726  gbege6  47727  stgoldbwt  47738  sbgoldbalt  47743  bgoldbnnsum3prm  47766  grimgrtri  47909  grlimgrtri  47956  grlicsym  47966  clnbgr3stgrgrlic  47972  gpg5gricstgr3  48040  uspgrbisymrelALT  48078  ssnn0ssfz  48272  ldepspr  48397  seposep  48848  upeu  49054  subthinc  49277  prsthinc  49298  iunord  49488  bnd2d  49493  setrecsss  49513