Theorem sylc 66

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 41	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 53	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl3c  67  mpsyl  69  jc  162  jcnd  164  2thd  268  jca  521  syl2anc  596  aevlem0  2089  equvel  2490  elex22  3481  spcedv  3559  rspcdf  3570  rspcdva  3584  rspc3dv  3602  spsbcd  3760  opth  5460  euotd  5498  wereu2  5660  unielrel  6278  frpomin  6345  tz7.7  6390  funmo  6556  fvelimad  6952  iinpreima  7068  fompt  7117  fnfvima  7238  resfvresima  7240  fliftfun  7319  fliftval  7323  weniso  7363  riota5f  7404  riotass2  7406  fovcld  7546  ofmpteq  7707  ssorduni  7784  nlimsucg  7844  tfisi  7861  zfrep6OLD  7958  curry1  8105  curry2  8108  fnwelem  8133  funsssuppss  8192  frrlem4  8292  frrlem8  8296  frrlem10  8298  fprlem1  8303  fprlem2  8304  smogt  8360  tfrlem5  8372  omeulem1  8573  oeworde  8585  oelimcl  8592  oeeulem  8593  oeeui  8594  nnawordex  8629  oaabs2  8641  naddssim  8678  naddsuc2  8694  swoso  8735  qliftlem  8802  resixp  8937  domssl  9001  domssr  9002  xpdom3  9070  domunsncan  9072  omxpenlem  9073  domssex  9133  xpf1o  9134  mapdom3  9144  dif1en  9153  findcard  9155  f1dmvrnfibi  9305  fsuppss  9350  fiin  9389  marypha1lem  9400  marypha1  9401  fisupcl  9437  supgtoreq  9438  ordiso2  9484  ordtypelem2  9488  ordtypelem8  9494  wemapso2lem  9521  unxpwdom2  9557  cantnflt  9648  cantnfrescl  9652  oemapvali  9660  cantnflem1d  9664  wemapwe  9673  cnfcom  9676  ttrclss  9696  ttrclselem2  9702  frrlem15  9736  rankr1id  9841  tcrank  9863  cardmin2  10001  infxpenlem  10013  fseqen  10027  ween  10035  ac5num  10036  indcardi  10041  acni2  10046  fodomfi2  10060  infpwfien  10062  inffien  10063  iunfictbso  10114  acacni  10140  dfac12lem2  10144  djuinf  10188  infmap2  10216  ackbij1lem18  10235  ackbij1b  10237  fictb  10243  cfslb2n  10267  cofsmo  10268  cfsmolem  10269  coftr  10272  infpssrlem4  10305  domfin4  10310  fin2i2  10317  isfin2-2  10318  fincssdom  10322  ssfin3ds  10329  fin23lem20  10336  fin23lem30  10341  isf32lem3  10354  fin1a2lem12  10410  fin1a2lem13  10411  hsmexlem2  10426  axdc2lem  10447  imadomg  10534  fnct  10539  fnctOLD  10540  iundom2g  10543  iundomg  10544  iundom  10545  unirnfdomd  10571  konigthlem  10572  iunctb  10578  fpwwe2  10647  canthwelem  10654  pwfseqlem3  10664  pwfseqlem5  10667  winalim2  10700  wunelss  10712  r1wunlim  10741  wunex2  10742  tsksdom  10760  tskinf  10773  inttsk  10778  inar1  10779  tskcard  10785  tskurn  10793  gruina  10822  grur1a  10823  grur1  10824  addsrpr  11079  mulsrpr  11080  lemul12a  12092  lemulge11  12096  lediv12a  12127  fiminre2  12182  nngt0  12286  nn0ge2m1nn  12593  peano5uzi  12705  nn0ind-raph  12716  znnn0nn  12727  suprzub  12983  uzsupss  12984  rpge0  13050  fz0fzelfz0  13683  fz0fzdiffz0  13686  ige2m2fzo  13778  elfzodifsumelfzo  13781  elfzom1elp1fzo  13782  fzonfzoufzol  13821  flltdivnn0lt  13888  fldiv  13915  modaddmodup  13992  uzrdgsuci  14018  fzennn  14026  uzindi  14040  fsuppmapnn0fiubex  14050  expcl2lem  14131  leexp1a  14233  modexp  14296  faclbnd  14348  faclbnd6  14357  facavg  14359  hashginv  14392  hashf1rn  14410  hasheqf1od  14411  seqcoll  14523  hashge2el2dif  14539  wrdsymb0  14608  wrdlenge2n0  14611  ccatsymb  14642  swrdnd2  14719  swrdnd0  14721  pfxnd  14751  pfxccat1  14765  swrdpfx  14770  pfxpfx  14771  wrd2ind  14786  pfxccatin12  14796  pfxccat3  14797  swrdccat  14798  pfxccatpfx1  14799  pfxccatpfx2  14800  swrdccatin1d  14806  pfxccatin12d  14808  repswswrd  14849  cshwidxmod  14868  s2f1o  14981  f1oun2prg  14982  wwlktovfo  15023  relexpfld  15114  rtrclreclem3  15125  resqrex  15329  cau3lem  15434  reusq0  15544  rlimcld2  15657  climcn2  15672  isercoll  15747  climsup  15749  caurcvgr  15753  sumeq2ii  15772  summolem3  15792  zsum  15796  fsumadd  15818  fsumsplit1  15823  fsum2dlem  15848  fsum0diag2  15861  fsummulc2  15862  fsumabs  15880  fsumrelem  15886  fsumrlim  15890  fsumo1  15891  o1fsum  15892  fsumiun  15900  qshash  15906  prodeq2ii  15992  prodmolem3  16014  fprodmul  16041  fproddiv  16042  fprod2dlem  16061  fprodsplit1f  16071  sin02gt0  16274  efieq1re  16281  p1modz1  16343  dvdsleabs2  16396  4dvdseven  16457  sumeven  16471  sumodd  16472  divalglem9  16485  smupvallem  16567  algfx  16664  eucalgcvga  16670  lcmfunsnlem1  16721  lcmfunsnlem2lem1  16722  lcmflefac  16732  qredeq  16741  dvdszzq  16806  fermltl  16869  modprm0  16891  pythagtriplem4  16905  pythagtriplem6  16907  pythagtriplem7  16908  pythagtriplem12  16912  pythagtriplem13  16913  pythagtriplem14  16914  pythagtriplem16  16916  difsqpwdvds  16973  pcmpt  16978  prmreclem2  17003  4sqlem11  17041  vdwlem9  17075  vdwlem11  17077  vdwlem12  17078  0ram  17106  0ram2  17107  0ramcl  17109  ramcl  17115  prmolelcmf  17134  cshwsidrepsw  17179  cshwshashlem2  17182  prmlem1  17193  prmlem2  17206  strfvd  17286  strfv2d  17287  strssd  17291  firest  17511  prdsdsval3  17564  imasbas  17592  imasds  17593  imasaddfnlem  17608  imasaddvallem  17609  imasvscafn  17617  qusaddvallem  17631  qusaddflem  17632  qusaddval  17633  qusaddf  17634  qusmulval  17635  qusmulf  17636  catideu  17757  idinv  17872  brcici  17883  invfuc  18060  2initoinv  18093  initoeu1w  18095  initoeu2lem0  18096  2termoinv  18100  termoeu1w  18102  resspos  18511  resstos  18512  mod2ile  18576  lubss  18595  acsmapd  18636  chnso  18706  lidrididd  18758  gsumval2a  18779  mndind  18928  submefmnd  18995  mgm2nsgrplem4  19024  qusgrp2  19172  mulgnegnn  19198  pgrpsubgsymg  19527  fvcosymgeq  19547  gsmsymgreqlem1  19548  psgnunilem4  19615  pgpssslw  19732  sylow2alem2  19736  fislw  19743  efgsres  19856  rinvmod  19924  gsumval3lem2  20024  gsumzaddlem  20039  gsum2d  20090  nn0gsumfz  20102  telgsums  20111  dprddomcld  20121  ablfac2  20209  qusrng  20306  srgdilem  20322  o2timesd  20340  rglcom4d  20341  ringdilem  20379  qusring2  20466  orngsqr  21023  lssintcl  21139  lbsextlem3  21338  lbsextlem4  21339  prmidl2  21520  qsidomlem2  21535  zringlpirlem3  21668  psgnodpm  21792  psgndiflemB  21804  frlmup4  22005  lindff1  22024  lindfrn  22025  lmisfree  22046  evlseu  22288  mhpmulcl  22366  mptcoe1fsupp  22429  cply1coe0bi  22516  mpfpf1  22565  pf1mpf  22566  mat0dimscm  22680  mdetdiagid  22811  mdet1  22812  mdetunilem9  22831  slesolinv  22891  cramerimp  22897  cpmatmcllem  22929  mptcoe1matfsupp  23013  mp2pm2mp  23022  chpdmat  23052  cctop  23217  subbascn  23465  cnss2  23488  cmpcovf  23602  2ndcctbss  23667  2ndcomap  23670  2ndcsep  23671  comppfsc  23744  ptclsg  23827  dfac14  23830  txcnp  23832  ptcnplem  23833  uptx  23837  txtube  23852  tx2ndc  23863  xkococnlem  23871  elqtop  23909  qtoprest  23929  indishmph  24010  ptcmpfi  24025  kqhmph  24031  csdfil  24106  filssufilg  24123  ufilen  24142  rnelfm  24165  fmfnfmlem4  24169  alexsubALTlem4  24262  ptcmplem4  24267  cnextfvval  24277  cnextcn  24279  cnextfres  24281  tmdgsum2  24308  imasf1oxmet  24587  metss  24720  met2ndci  24734  prdsxmslem2  24741  metust  24770  cfilucfil  24771  metustbl  24778  psmetutop  24779  opnreen  25044  rectbntr0  25045  fsumcn  25084  rescncf  25111  xrhmeo  25160  cnllycmp  25170  lebnumlem1  25175  lebnumlem3  25177  cfilss  25484  iscmet3lem1  25505  iscmet3lem2  25506  ivthicc  25672  ovolsslem  25698  ovoliunlem2  25717  ovoliunnul  25721  ovolicc2lem4  25734  voliunlem3  25766  volsup  25770  uniiccdif  25792  uniioombllem2  25797  volivth  25821  mbfimaopnlem  25869  mbflimsup  25880  i1fd  25895  itg1addlem4  25913  itg2addlem  25972  itg2gt0  25974  limciun  26108  dvadd  26154  dvmul  26155  dvco  26161  dvrec  26169  dvcnv  26191  dvferm  26202  rollelem  26203  dvlip  26207  dvlip2  26209  c1liplem1  26210  c1lip2  26212  dvgt0lem1  26216  dvivthlem1  26222  lhop1lem  26227  dvcnvrelem1  26231  dvcnvrelem2  26232  dvcvx  26234  dvfsumle  26235  dvfsumabs  26237  dvfsumlem1  26240  dvfsumlem2  26241  dvfsumlem4  26243  dvfsumrlim2  26246  dvfsum2  26248  ftc1cn  26257  ftc2ditglem  26259  itgsubstlem  26262  itgpowd  26264  mdegaddle  26286  mdegmullem  26290  deg1sublt  26322  ply1divmo  26348  fta1g  26382  dgrub  26446  dgrnznn  26459  dgradd2  26480  dvply1  26500  plyrem  26521  aalioulem4  26553  aalioulem5  26554  aalioulem6  26555  aaliou2  26558  taylf  26579  ulmdv  26621  psercn2  26641  abelth  26659  abelth2  26660  reeff1olem  26664  efopn  26878  logreclem  26982  isosctrlem2  27039  xrlimcnp  27188  basellem4  27303  ppiwordi  27381  musum  27410  chpub  27439  gausslemma2dlem0c  27577  2sqlem6  27642  addsqnreup  27662  2sqreulem1  27665  2sqreunnlem1  27668  dchrisumlema  27707  dchrisumlem2  27709  dchrisumlem3  27710  pntlemp  27829  pntleml  27830  ostth3  27857  ltsres  27881  noextenddif  27887  nolesgn2ores  27891  nogesgn1ores  27893  nosep1o  27900  nosep2o  27901  nosepeq  27904  nolt02o  27914  noresle  27916  nosupno  27922  nosupbday  27924  nosupres  27926  nosupbnd1lem1  27927  nosupbnd1lem4  27930  nosupbnd1  27933  nosupbnd2lem1  27934  nosupbnd2  27935  noinfno  27937  noinfbday  27939  noinfres  27941  noinfbnd1lem5  27946  noinfbnd1  27948  noinfbnd2lem1  27949  ltlesd  27992  madebday  28148  leadds1  28237  precsexlem10  28464  noseqrdg0  28555  noseqrdgsuc  28556  elnnzs  28649  bdaypw2n0bndlem  28711  iscgrglt  28838  colline  28978  axlowdimlem16  29366  axlowdimlem17  29367  axcontlem3  29375  axcontlem10  29382  uhgr2edg  29620  nbupgruvtxres  29819  cusgrres  29860  cusgrfilem2  29868  vdumgr0  29892  frusgrnn0  29983  wlkp1lem8  30090  pthdivtx  30143  upgrwlkdvde  30154  spthonepeq  30169  usgr2pthlem  30180  cyclnumvtx  30219  lfgrn1cycl  30225  wwlknbp1  30264  wwlknllvtx  30266  wlkiswwlks2lem3  30291  umgr2adedgspth  30368  clwlkclwwlklem3  30423  clwwisshclwwslemlem  30435  clwwisshclwws  30437  clwwlkel  30468  wwlksubclwwlk  30480  eleclclwwlknlem1  30482  eleclclwwlknlem2  30483  erclwwlknref  30491  clwwlknonccat  30518  clwwlknonex2lem2  30530  3wlkdlem4  30588  vdn0conngrumgrv2  30622  eucrctshift  30669  frgrnbnb  30719  frgrncvvdeqlem2  30726  frgrncvvdeqlem3  30727  fusgreghash2wspv  30761  numclwwlk2lem1  30802  numclwlk2lem2f  30803  numclwwlk5  30814  numclwwlk7  30817  frgrreggt1  30819  minvecolem4b  31305  minvecolem4  31307  bcsiALT  31606  ococin  31835  spanpr  32007  pjorthi  32096  nmbdoplbi  32451  nmcoplbi  32455  nmbdfnlbi  32476  nmcfnlbi  32479  nmopcoi  32522  branmfn  32532  hstnmoc  32650  mdsl0  32737  atomli  32809  atcvat4i  32824  atabsi  32828  foresf1o  32925  rabfodom  32926  abrexdomjm  32928  elpreq  32949  ifeqeqx  32963  disjiunel  33016  ac6mapd  33043  aciunf1lem  33082  ffsrn  33147  xlt2addrd  33178  supxrnemnf  33187  ssnnssfz  33206  gsummptres2  33441  gsumfs2d  33449  archirngz  33577  isarchiofld  33587  unitprodclb  33770  elrspunidl  33804  drngidlhash  33809  ssmxidl  33825  1arithidom  33895  1arithufdlem4  33905  constrmon  34202  locfinreflem  34298  cmpcref  34308  fmcncfil  34389  xrge0iifiso  34393  elzdif0  34438  qqhval2lem  34439  esumcst  34521  esumrnmpt2  34526  esumpinfval  34531  esumpinfsum  34535  sigaclci  34590  insiga  34596  ldgenpisys  34625  measres  34681  measdivcstALTV  34684  dya2iocnrect  34740  dya2iocnei  34741  omssubadd  34759  carsggect  34777  carsgclctunlem2  34778  sitgclg  34801  eulerpartlemsv2  34817  eulerpartlemv  34823  eulerpartlemf  34829  eulerpartlemgh  34837  eulerpartlemgs2  34839  ballotlemfp1  34951  ballotlemfrcn0  34989  ftc2re  35054  fdvposlt  35055  fdvposle  35057  bnj1379  35287  bnj580  35370  bnj944  35395  bnj999  35415  bnj1204  35469  bnj1398  35491  onvfowev  35661  cusgredgex  35668  pthacycspth  35690  derangenlem  35704  subfacp1lem3  35715  resconn  35779  cvmliftlem3  35820  satfv0fvfmla0  35946  satfv1fvfmla1  35956  mrsub0  36049  cgrextend  36541  segconeq  36543  trisegint  36561  fwddifnp1  36698  onelssd  36734  nmuladdss  36746  ivthALT  36907  fnessref  36929  refssfne  36930  neibastop1  36931  filnetlem4  36953  ontgval  37003  weiunlem  37035  weiunse  37040  dfttc4  37102  unblimceq0lem  37156  unbdqndv2lem2  37160  unbdqndv2  37161  bj-babygodel  37257  bj-alrimd  37279  bj-exlimd  37291  bj-spim  37309  bj-spime  37310  bj-nnf-spime  37461  bj-spcimdv  37591  bj-spcimdvv  37592  bj-finsumval0  37990  bj-fvimacnv0  37991  dfgcd3  38029  relowlssretop  38070  relowlpssretop  38071  onsucuni3  38074  finxpreclem4  38101  poimirlem18  38350  poimirlem21  38353  poimirlem25  38357  ftc1cnnclem  38403  ftc1cnnc  38404  ftc2nc  38414  dvasin  38416  dvacos  38417  abrexdom  38443  indexdom  38447  mettrifi  38470  equivtotbnd  38491  totbndbnd  38502  prdstotbnd  38507  heibor1lem  38522  bfplem1  38535  bfplem2  38536  opidonOLD  38565  rngodm1dm2  38645  zerdivemp1x  38660  equid1  39735  omllaw5N  40083  cmtcomlemN  40084  cmtbr3N  40090  omlfh3N  40095  atlen0  40146  exatleN  40240  hlrelat3  40248  cvrexchlem  40255  atlelt  40274  cvrat4  40279  4atlem11b  40444  4atlem12b  40447  lneq2at  40614  cdlema1N  40627  cdlemblem  40629  paddss12  40655  paddasslem2  40657  paddasslem4  40659  paddasslem6  40661  paddasslem12  40667  paddunN  40763  poml4N  40789  poml5N  40790  osumcllem6N  40797  pexmidlem6N  40811  pl42lem2N  40816  ltrnu  40957  ltrneq2  40984  trlval2  40999  cdlemd6  41039  cdleme25b  41190  cdleme29b  41211  cdlemefr29exN  41238  ltrniotacnvval  41418  cdlemk28-3  41744  dochexmidlem7  42302  muldvds2d  42827  frlmsnic  43385  nna4b4nsq  43469  mzpsubmpt  43551  mzpsubst  43556  eqrabdioph  43585  rabdiophlem2  43606  elpell14qr2  43666  elpell1qr2  43676  pellfundre  43685  pellfundge  43686  pellfundglb  43689  pellfund14gap  43691  congabseq  43778  jm2.22  43799  jm2.23  43800  jm2.26lem3  43805  wepwsolem  43846  aomclem2  43859  aomclem4  43861  pwfi2f1o  43900  onexlimgt  44047  oaltublim  44094  oege1  44110  cantnfub2  44126  cantnfresb  44128  cantnf2  44129  oacl2g  44134  tfsconcatb0  44148  tfsconcatrev  44152  oaun3lem1  44178  oaun3lem2  44179  nadd2rabtr  44188  nadd1suc  44196  naddwordnexlem0  44200  naddwordnexlem3  44203  oawordex3  44204  naddwordnexlem4  44205  oaltom  44208  omltoe  44210  ss2iundf  44462  dssmapf1od  44824  neik0pk1imk0  44850  gneispace  44937  grur1cld  45033  cpcolld  45045  mnuop23d  45053  mnuprdlem1  45059  mnuprdlem2  45060  mnurndlem1  45068  grumnudlem  45072  radcnvrat  45101  sbiota1  45221  ordelordALT  45323  2pm13.193  45338  ee11an  45476  modelaxreplem2  45765  refsumcn  45827  rfcnnnub  45833  disjxp1  45866  xrnmnfpnf  45880  ssinc  45882  nssd  45900  disjf1o  45986  disjinfi  45987  choicefi  45994  axccdom  46015  dmrelrnrel  46019  monoords  46093  fperiodmullem  46099  xadd0ge  46115  xrssre  46141  xrlexaddrp  46145  xrred  46157  infxr  46159  xrnpnfmnf  46265  monoordxrv  46272  monoord2xrv  46274  cvgcaule  46282  fsumiunss  46368  fmul01  46373  fmuldfeqlem1  46375  fmuldfeq  46376  fmul01lt1lem1  46377  fmul01lt1lem2  46378  cncfmptss  46380  climinf  46399  climsuselem1  46400  climsuse  46401  limcperiod  46421  limcrecl  46422  sumnnodd  46423  limcleqr  46435  0ellimcdiv  46440  climleltrp  46467  limsuppnfdlem  46492  limsupresxr  46557  liminfresxr  46558  liminfvalxr  46574  cnrefiisplem  46620  xlimmnfvlem1  46623  xlimpnfvlem1  46627  cncfperiod  46670  icccncfext  46678  cncfiooicclem1  46684  dvbdfbdioolem1  46719  dvnmptdivc  46729  dvdsn1add  46730  dvnmptconst  46732  dvnmul  46734  dvmptfprodlem  46735  dvmptfprod  46736  dvnprodlem2  46738  iblspltprt  46764  itgsubsticclem  46766  itgspltprt  46770  itgsbtaddcnst  46773  stoweidlem3  46794  stoweidlem16  46807  stoweidlem17  46808  stoweidlem19  46810  stoweidlem20  46811  stoweidlem23  46814  stoweidlem25  46816  stoweidlem27  46818  stoweidlem31  46822  stoweidlem34  46825  stoweidlem42  46833  stoweidlem48  46839  stoweidlem51  46842  stoweidlem52  46843  stoweidlem59  46850  wallispilem1  46856  wallispilem3  46858  stirlinglem13  46877  fourierdlem16  46914  fourierdlem20  46918  fourierdlem21  46919  fourierdlem38  46936  fourierdlem42  46940  fourierdlem46  46943  fourierdlem48  46945  fourierdlem49  46946  fourierdlem50  46947  fourierdlem54  46951  fourierdlem68  46965  fourierdlem72  46969  fourierdlem73  46970  fourierdlem76  46973  fourierdlem79  46976  fourierdlem81  46978  fourierdlem86  46983  fourierdlem89  46986  fourierdlem90  46987  fourierdlem91  46988  fourierdlem92  46989  fourierdlem97  46994  fourierdlem101  46998  fourierdlem103  47000  fourierdlem104  47001  fourierdlem111  47008  etransclem24  47049  etransclem25  47050  etransclem28  47053  etransclem41  47066  etransclem44  47069  etransclem48  47073  salexct  47125  dfsalgen2  47132  sge0f1o  47173  sge0rnbnd  47184  sge0split  47200  sge0iunmptlemre  47206  sge0fodjrnlem  47207  sge0iunmpt  47209  nnfoctbdjlem  47246  iundjiunlem  47250  meadjiunlem  47256  ismeannd  47258  meaiuninclem  47271  carageniuncllem1  47312  caratheodorylem1  47317  hoidmvlelem4  47389  hoiqssbllem2  47414  salpreimagelt  47498  salpreimalegt  47500  pimdecfgtioc  47506  smfaddlem2  47555  smflimlem6  47567  nsssmfmbflem  47569  smfpimcclem  47598  quantgodelALT  47666  ormkglobd  47668  or2expropbilem1  47846  funressndmfvrn  47858  f1cof1b  47891  2leaddle2  48112  smonoord  48191  muldvdsfacgt  48200  uniimaprimaeqfv  48208  fundcmpsurbijinjpreimafv  48233  fundcmpsurinjALT  48238  iccpartf  48257  ich2exprop  48297  ichnreuop  48298  ichreuopeq  48299  sprbisymrel  48325  fmtnodvds  48373  proththdlem  48442  gbowgt5  48604  gboge9  48606  gbege6  48607  stgoldbwt  48618  sbgoldbalt  48623  bgoldbnnsum3prm  48646  grimgrtri  48791  grlimgrtri  48845  grlicsym  48855  clnbgr3stgrgrlim  48861  clnbgr3stgrgrlic  48862  gpg5gricstgr3  48932  uspgrbisymrelALT  48997  ssnn0ssfz  49205  ldepspr  49329  seposep  49780  upeu  50025  subthinc  50297  prsthinc  50318  iunord  50530  bnd2d  50535  setrecsss  50555