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 ⊢ (𝜑 → 𝜃)

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  67  mpsyl  69  jc  162  jcnd  164  2thd  268  jca  520  syl2anc  595  aevlem0  2086  equvel  2488  elex22  3479  spcedv  3557  rspcdf  3568  rspcdva  3582  rspc3dv  3600  spsbcd  3758  opth  5458  euotd  5496  wereu2  5658  unielrel  6275  frpomin  6341  tz7.7  6386  funmo  6552  fvelimad  6948  iinpreima  7064  fompt  7113  fnfvima  7231  resfvresima  7233  fliftfun  7310  fliftval  7314  weniso  7352  riota5f  7395  riotass2  7397  fovcld  7537  ofmpteq  7697  ssorduni  7774  nlimsucg  7834  tfisi  7851  zfrep6OLD  7948  curry1  8095  curry2  8098  fnwelem  8123  funsssuppss  8182  frrlem4  8282  frrlem8  8286  frrlem10  8288  fprlem1  8293  fprlem2  8294  smogt  8350  tfrlem5  8362  omeulem1  8563  oeworde  8575  oelimcl  8582  oeeulem  8583  oeeui  8584  nnawordex  8619  oaabs2  8631  naddssim  8668  naddsuc2  8684  swoso  8725  qliftlem  8792  resixp  8927  domssl  8991  domssr  8992  xpdom3  9059  domunsncan  9061  omxpenlem  9062  domssex  9122  xpf1o  9123  mapdom3  9133  dif1en  9142  findcard  9144  f1dmvrnfibi  9294  fsuppss  9339  fiin  9378  marypha1lem  9389  marypha1  9390  fisupcl  9426  supgtoreq  9427  ordiso2  9473  ordtypelem2  9477  ordtypelem8  9483  wemapso2lem  9510  unxpwdom2  9546  cantnflt  9637  cantnfrescl  9641  oemapvali  9649  cantnflem1d  9653  wemapwe  9662  cnfcom  9665  ttrclss  9685  ttrclselem2  9691  frrlem15  9725  rankr1id  9830  tcrank  9852  cardmin2  9981  infxpenlem  9993  fseqen  10007  ween  10015  ac5num  10016  indcardi  10021  acni2  10026  fodomfi2  10040  infpwfien  10042  inffien  10043  iunfictbso  10094  acacni  10120  dfac12lem2  10124  djuinf  10168  infmap2  10196  ackbij1lem18  10215  ackbij1b  10217  fictb  10223  cfslb2n  10247  cofsmo  10248  cfsmolem  10249  coftr  10252  infpssrlem4  10285  domfin4  10290  fin2i2  10297  isfin2-2  10298  fincssdom  10302  ssfin3ds  10309  fin23lem20  10316  fin23lem30  10321  isf32lem3  10334  fin1a2lem12  10390  fin1a2lem13  10391  hsmexlem2  10406  axdc2lem  10427  imadomg  10513  fnct  10516  iundom2g  10519  iundomg  10520  iundom  10521  unirnfdomd  10547  konigthlem  10548  iunctb  10554  fpwwe2  10623  canthwelem  10630  pwfseqlem3  10640  pwfseqlem5  10643  winalim2  10676  wunelss  10688  r1wunlim  10717  wunex2  10718  tsksdom  10736  tskinf  10749  inttsk  10754  inar1  10755  tskcard  10761  tskurn  10769  gruina  10798  grur1a  10799  grur1  10800  addsrpr  11055  mulsrpr  11056  lemul12a  12068  lemulge11  12072  lediv12a  12103  fiminre2  12158  nngt0  12262  nn0ge2m1nn  12569  peano5uzi  12680  nn0ind-raph  12691  znnn0nn  12702  suprzub  12958  uzsupss  12959  rpge0  13025  fz0fzelfz0  13658  fz0fzdiffz0  13661  ige2m2fzo  13753  elfzodifsumelfzo  13756  elfzom1elp1fzo  13757  fzonfzoufzol  13796  flltdivnn0lt  13862  fldiv  13889  modaddmodup  13966  uzrdgsuci  13992  fzennn  14000  uzindi  14014  fsuppmapnn0fiubex  14024  expcl2lem  14105  leexp1a  14207  modexp  14270  faclbnd  14322  faclbnd6  14331  facavg  14333  hashginv  14366  hashf1rn  14384  hasheqf1od  14385  seqcoll  14497  hashge2el2dif  14513  wrdsymb0  14582  wrdlenge2n0  14585  ccatsymb  14616  swrdnd2  14689  swrdnd0  14691  pfxnd  14721  pfxccat1  14735  swrdpfx  14740  pfxpfx  14741  wrd2ind  14756  pfxccatin12  14766  pfxccat3  14767  swrdccat  14768  pfxccatpfx1  14769  pfxccatpfx2  14770  swrdccatin1d  14776  pfxccatin12d  14778  repswswrd  14817  cshwidxmod  14836  s2f1o  14949  f1oun2prg  14950  wwlktovfo  14991  relexpfld  15082  rtrclreclem3  15093  resqrex  15297  cau3lem  15402  reusq0  15512  rlimcld2  15625  climcn2  15640  isercoll  15715  climsup  15717  caurcvgr  15721  sumeq2ii  15740  summolem3  15761  zsum  15765  fsumadd  15787  fsumsplit1  15792  fsum2dlem  15817  fsum0diag2  15830  fsummulc2  15831  fsumabs  15849  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  qshash  15875  prodeq2ii  15961  prodmolem3  15983  fprodmul  16010  fproddiv  16011  fprod2dlem  16030  fprodsplit1f  16040  sin02gt0  16243  efieq1re  16250  p1modz1  16312  dvdsleabs2  16365  4dvdseven  16426  sumeven  16440  sumodd  16441  divalglem9  16454  smupvallem  16536  algfx  16633  eucalgcvga  16639  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmflefac  16701  qredeq  16710  dvdszzq  16775  fermltl  16838  modprm0  16860  pythagtriplem4  16874  pythagtriplem6  16876  pythagtriplem7  16877  pythagtriplem12  16881  pythagtriplem13  16882  pythagtriplem14  16883  pythagtriplem16  16885  difsqpwdvds  16942  pcmpt  16947  prmreclem2  16972  4sqlem11  17010  vdwlem9  17044  vdwlem11  17046  vdwlem12  17047  0ram  17075  0ram2  17076  0ramcl  17078  ramcl  17084  prmolelcmf  17103  cshwsidrepsw  17148  cshwshashlem2  17151  prmlem1  17162  prmlem2  17175  strfvd  17255  strfv2d  17256  strssd  17260  firest  17480  prdsdsval3  17533  imasbas  17561  imasds  17562  imasaddfnlem  17577  imasaddvallem  17578  imasvscafn  17586  qusaddvallem  17600  qusaddflem  17601  qusaddval  17602  qusaddf  17603  qusmulval  17604  qusmulf  17605  catideu  17726  idinv  17841  brcici  17852  invfuc  18029  2initoinv  18062  initoeu1w  18064  initoeu2lem0  18065  2termoinv  18069  termoeu1w  18071  resspos  18480  resstos  18481  mod2ile  18545  lubss  18564  acsmapd  18605  chnso  18675  lidrididd  18723  gsumval2a  18738  mndind  18882  submefmnd  18949  mgm2nsgrplem4  18978  qusgrp2  19119  mulgnegnn  19145  pgrpsubgsymg  19474  fvcosymgeq  19494  gsmsymgreqlem1  19495  psgnunilem4  19562  pgpssslw  19679  sylow2alem2  19683  fislw  19690  efgsres  19803  rinvmod  19871  gsumval3lem2  19971  gsumzaddlem  19986  gsum2d  20037  nn0gsumfz  20049  telgsums  20058  dprddomcld  20068  ablfac2  20156  qusrng  20253  srgdilem  20269  o2timesd  20287  rglcom4d  20288  ringdilem  20326  qusring2  20412  orngsqr  20969  lssintcl  21085  lbsextlem3  21284  lbsextlem4  21285  prmidl2  21466  qsidomlem2  21481  zringlpirlem3  21614  psgnodpm  21738  psgndiflemB  21750  frlmup4  21951  lindff1  21970  lindfrn  21971  lmisfree  21992  evlseu  22234  mhpmulcl  22312  mptcoe1fsupp  22375  cply1coe0bi  22462  mpfpf1  22511  pf1mpf  22512  mat0dimscm  22626  mdetdiagid  22757  mdet1  22758  mdetunilem9  22777  slesolinv  22837  cramerimp  22843  cpmatmcllem  22875  mptcoe1matfsupp  22959  mp2pm2mp  22968  chpdmat  22998  cctop  23163  subbascn  23411  cnss2  23434  cmpcovf  23548  2ndcctbss  23612  2ndcomap  23615  2ndcsep  23616  comppfsc  23689  ptclsg  23772  dfac14  23775  txcnp  23777  ptcnplem  23778  uptx  23782  txtube  23797  tx2ndc  23808  xkococnlem  23816  elqtop  23854  qtoprest  23874  indishmph  23955  ptcmpfi  23970  kqhmph  23976  csdfil  24051  filssufilg  24068  ufilen  24087  rnelfm  24110  fmfnfmlem4  24114  alexsubALTlem4  24207  ptcmplem4  24212  cnextfvval  24222  cnextcn  24224  cnextfres  24226  tmdgsum2  24253  imasf1oxmet  24532  metss  24665  met2ndci  24679  prdsxmslem2  24686  metust  24715  cfilucfil  24716  metustbl  24723  psmetutop  24724  opnreen  24989  rectbntr0  24990  fsumcn  25029  rescncf  25056  xrhmeo  25105  cnllycmp  25115  lebnumlem1  25120  lebnumlem3  25122  cfilss  25429  iscmet3lem1  25450  iscmet3lem2  25451  ivthicc  25617  ovolsslem  25643  ovoliunlem2  25662  ovoliunnul  25666  ovolicc2lem4  25679  voliunlem3  25711  volsup  25715  uniiccdif  25737  uniioombllem2  25742  volivth  25766  mbfimaopnlem  25814  mbflimsup  25825  i1fd  25840  itg1addlem4  25858  itg2addlem  25917  itg2gt0  25919  limciun  26053  dvadd  26099  dvmul  26100  dvco  26106  dvrec  26114  dvcnv  26136  dvferm  26147  rollelem  26148  dvlip  26152  dvlip2  26154  c1liplem1  26155  c1lip2  26157  dvgt0lem1  26161  dvivthlem1  26167  lhop1lem  26172  dvcnvrelem1  26176  dvcnvrelem2  26177  dvcvx  26179  dvfsumle  26180  dvfsumabs  26182  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem4  26188  dvfsumrlim2  26191  dvfsum2  26193  ftc1cn  26202  ftc2ditglem  26204  itgsubstlem  26207  itgpowd  26209  mdegaddle  26231  mdegmullem  26235  deg1sublt  26267  ply1divmo  26293  fta1g  26327  dgrub  26391  dgrnznn  26404  dgradd2  26425  dvply1  26445  plyrem  26466  aalioulem4  26498  aalioulem5  26499  aalioulem6  26500  aaliou2  26503  taylf  26524  ulmdv  26566  psercn2  26586  abelth  26604  abelth2  26605  reeff1olem  26609  efopn  26823  logreclem  26927  isosctrlem2  26984  xrlimcnp  27133  basellem4  27248  ppiwordi  27326  musum  27355  chpub  27384  gausslemma2dlem0c  27522  2sqlem6  27587  addsqnreup  27607  2sqreulem1  27610  2sqreunnlem1  27613  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  pntlemp  27774  pntleml  27775  ostth3  27802  ltsres  27826  noextenddif  27832  nolesgn2ores  27836  nogesgn1ores  27838  nosep1o  27845  nosep2o  27846  nosepeq  27849  nolt02o  27859  noresle  27861  nosupno  27867  nosupbday  27869  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem4  27875  nosupbnd1  27878  nosupbnd2lem1  27879  nosupbnd2  27880  noinfno  27882  noinfbday  27884  noinfres  27886  noinfbnd1lem5  27891  noinfbnd1  27893  noinfbnd2lem1  27894  ltlesd  27937  madebday  28093  leadds1  28182  precsexlem10  28409  noseqrdg0  28500  noseqrdgsuc  28501  elnnzs  28594  bdaypw2n0bndlem  28656  iscgrglt  28783  colline  28923  axlowdimlem16  29307  axlowdimlem17  29308  axcontlem3  29316  axcontlem10  29323  uhgr2edg  29558  nbupgruvtxres  29757  cusgrres  29798  cusgrfilem2  29806  vdumgr0  29830  frusgrnn0  29921  wlkp1lem8  30028  pthdivtx  30076  upgrwlkdvde  30086  spthonepeq  30101  usgr2pthlem  30112  cyclnumvtx  30149  lfgrn1cycl  30154  wwlknbp1  30193  wwlknllvtx  30195  wlkiswwlks2lem3  30220  umgr2adedgspth  30297  clwlkclwwlklem3  30352  clwwisshclwwslemlem  30364  clwwisshclwws  30366  clwwlkel  30397  wwlksubclwwlk  30409  eleclclwwlknlem1  30411  eleclclwwlknlem2  30412  erclwwlknref  30420  clwwlknonccat  30447  clwwlknonex2lem2  30459  3wlkdlem4  30513  vdn0conngrumgrv2  30547  eucrctshift  30594  frgrnbnb  30644  frgrncvvdeqlem2  30651  frgrncvvdeqlem3  30652  fusgreghash2wspv  30686  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwwlk5  30739  numclwwlk7  30742  frgrreggt1  30744  minvecolem4b  31230  minvecolem4  31232  bcsiALT  31531  ococin  31760  spanpr  31932  pjorthi  32021  nmbdoplbi  32376  nmcoplbi  32380  nmbdfnlbi  32401  nmcfnlbi  32404  nmopcoi  32447  branmfn  32457  hstnmoc  32575  mdsl0  32662  atomli  32734  atcvat4i  32749  atabsi  32753  foresf1o  32850  rabfodom  32851  abrexdomjm  32853  elpreq  32874  ifeqeqx  32888  disjiunel  32941  ac6mapd  32968  aciunf1lem  33007  ffsrn  33073  xlt2addrd  33104  supxrnemnf  33113  ssnnssfz  33132  gsummptres2  33373  gsumfs2d  33381  archirngz  33509  isarchiofld  33519  unitprodclb  33702  elrspunidl  33736  drngidlhash  33741  ssmxidl  33757  1arithidom  33827  1arithufdlem4  33837  constrmon  34134  locfinreflem  34230  cmpcref  34240  fmcncfil  34321  xrge0iifiso  34325  elzdif0  34370  qqhval2lem  34371  esumcst  34453  esumrnmpt2  34458  esumpinfval  34463  esumpinfsum  34467  sigaclci  34522  insiga  34527  ldgenpisys  34556  measres  34612  measdivcstALTV  34615  dya2iocnrect  34671  dya2iocnei  34672  omssubadd  34690  carsggect  34708  carsgclctunlem2  34709  sitgclg  34732  eulerpartlemsv2  34748  eulerpartlemv  34754  eulerpartlemf  34760  eulerpartlemgh  34768  eulerpartlemgs2  34770  ballotlemfp1  34882  ballotlemfrcn0  34920  ftc2re  34985  fdvposlt  34986  fdvposle  34988  bnj1379  35218  bnj580  35301  bnj944  35326  bnj999  35346  bnj1204  35400  bnj1398  35422  onvfowev  35600  cusgredgex  35614  pthacycspth  35649  derangenlem  35663  subfacp1lem3  35674  resconn  35738  cvmliftlem3  35779  satfv0fvfmla0  35905  satfv1fvfmla1  35915  mrsub0  36008  cgrextend  36500  segconeq  36502  trisegint  36520  fwddifnp1  36657  onelssd  36693  nmuladdss  36705  ivthALT  36866  fnessref  36888  refssfne  36889  neibastop1  36890  filnetlem4  36912  ontgval  36962  weiunlem  36994  weiunse  36999  dfttc4  37061  unblimceq0lem  37115  unbdqndv2lem2  37119  unbdqndv2  37120  bj-babygodel  37216  bj-alrimd  37238  bj-exlimd  37250  bj-spim  37268  bj-spime  37269  bj-nnf-spime  37420  bj-spcimdv  37550  bj-spcimdvv  37551  bj-finsumval0  37949  bj-fvimacnv0  37950  dfgcd3  37988  relowlssretop  38029  relowlpssretop  38030  onsucuni3  38033  finxpreclem4  38060  poimirlem18  38309  poimirlem21  38312  poimirlem25  38316  ftc1cnnclem  38362  ftc1cnnc  38363  ftc2nc  38373  dvasin  38375  dvacos  38376  abrexdom  38401  indexdom  38405  mettrifi  38428  equivtotbnd  38449  totbndbnd  38460  prdstotbnd  38465  heibor1lem  38480  bfplem1  38493  bfplem2  38494  opidonOLD  38523  rngodm1dm2  38603  zerdivemp1x  38618  equid1  39693  omllaw5N  40041  cmtcomlemN  40042  cmtbr3N  40048  omlfh3N  40053  atlen0  40104  exatleN  40198  hlrelat3  40206  cvrexchlem  40213  atlelt  40232  cvrat4  40237  4atlem11b  40402  4atlem12b  40405  lneq2at  40572  cdlema1N  40585  cdlemblem  40587  paddss12  40613  paddasslem2  40615  paddasslem4  40617  paddasslem6  40619  paddasslem12  40625  paddunN  40721  poml4N  40747  poml5N  40748  osumcllem6N  40755  pexmidlem6N  40769  pl42lem2N  40774  ltrnu  40915  ltrneq2  40942  trlval2  40957  cdlemd6  40997  cdleme25b  41148  cdleme29b  41169  cdlemefr29exN  41196  ltrniotacnvval  41376  cdlemk28-3  41702  dochexmidlem7  42260  muldvds2d  42785  frlmsnic  43328  nna4b4nsq  43412  mzpsubmpt  43494  mzpsubst  43499  eqrabdioph  43528  rabdiophlem2  43549  elpell14qr2  43609  elpell1qr2  43619  pellfundre  43628  pellfundge  43629  pellfundglb  43632  pellfund14gap  43634  congabseq  43721  jm2.22  43742  jm2.23  43743  jm2.26lem3  43748  wepwsolem  43789  dnwech  43795  aomclem2  43802  aomclem4  43804  pwfi2f1o  43843  onexlimgt  43990  oaltublim  44037  oege1  44053  cantnfub2  44069  cantnfresb  44071  cantnf2  44072  oacl2g  44077  tfsconcatb0  44091  tfsconcatrev  44095  oaun3lem1  44121  oaun3lem2  44122  nadd2rabtr  44131  nadd1suc  44139  naddwordnexlem0  44143  naddwordnexlem3  44146  oawordex3  44147  naddwordnexlem4  44148  oaltom  44151  omltoe  44153  ss2iundf  44405  dssmapf1od  44767  neik0pk1imk0  44793  gneispace  44880  grur1cld  44976  cpcolld  44988  mnuop23d  44996  mnuprdlem1  45002  mnuprdlem2  45003  mnurndlem1  45011  grumnudlem  45015  radcnvrat  45044  sbiota1  45164  ordelordALT  45266  2pm13.193  45281  ee11an  45419  modelaxreplem2  45708  refsumcn  45770  rfcnnnub  45776  disjxp1  45809  xrnmnfpnf  45823  ssinc  45825  nssd  45843  disjf1o  45929  disjinfi  45930  choicefi  45937  axccdom  45958  dmrelrnrel  45962  monoords  46036  fperiodmullem  46042  xadd0ge  46058  xrssre  46084  xrlexaddrp  46088  xrred  46100  infxr  46102  xrnpnfmnf  46208  monoordxrv  46215  monoord2xrv  46217  cvgcaule  46225  fsumiunss  46311  fmul01  46316  fmuldfeqlem1  46318  fmuldfeq  46319  fmul01lt1lem1  46320  fmul01lt1lem2  46321  cncfmptss  46323  climinf  46342  climsuselem1  46343  climsuse  46344  limcperiod  46364  limcrecl  46365  sumnnodd  46366  limcleqr  46378  0ellimcdiv  46383  climleltrp  46410  limsuppnfdlem  46435  limsupresxr  46500  liminfresxr  46501  liminfvalxr  46517  cnrefiisplem  46563  xlimmnfvlem1  46566  xlimpnfvlem1  46570  cncfperiod  46613  icccncfext  46621  cncfiooicclem1  46627  dvbdfbdioolem1  46662  dvnmptdivc  46672  dvdsn1add  46673  dvnmptconst  46675  dvnmul  46677  dvmptfprodlem  46678  dvmptfprod  46679  dvnprodlem2  46681  iblspltprt  46707  itgsubsticclem  46709  itgspltprt  46713  itgsbtaddcnst  46716  stoweidlem3  46737  stoweidlem16  46750  stoweidlem17  46751  stoweidlem19  46753  stoweidlem20  46754  stoweidlem23  46757  stoweidlem25  46759  stoweidlem27  46761  stoweidlem31  46765  stoweidlem34  46768  stoweidlem42  46776  stoweidlem48  46782  stoweidlem51  46785  stoweidlem52  46786  stoweidlem59  46793  wallispilem1  46799  wallispilem3  46801  stirlinglem13  46820  fourierdlem16  46857  fourierdlem20  46861  fourierdlem21  46862  fourierdlem38  46879  fourierdlem42  46883  fourierdlem46  46886  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem54  46894  fourierdlem68  46908  fourierdlem72  46912  fourierdlem73  46913  fourierdlem76  46916  fourierdlem79  46919  fourierdlem81  46921  fourierdlem86  46926  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  fourierdlem92  46932  fourierdlem97  46937  fourierdlem101  46941  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  etransclem24  46992  etransclem25  46993  etransclem28  46996  etransclem41  47009  etransclem44  47012  etransclem48  47016  salexct  47068  dfsalgen2  47075  sge0f1o  47116  sge0rnbnd  47127  sge0split  47143  sge0iunmptlemre  47149  sge0fodjrnlem  47150  sge0iunmpt  47152  nnfoctbdjlem  47189  iundjiunlem  47193  meadjiunlem  47199  ismeannd  47201  meaiuninclem  47214  omeiunle  47251  carageniuncllem1  47255  caratheodorylem1  47260  hoidmvlelem4  47332  hoiqssbllem2  47357  salpreimagelt  47441  salpreimalegt  47443  pimdecfgtioc  47449  smfaddlem2  47498  smflimlem6  47510  nsssmfmbflem  47512  smfpimcclem  47541  quantgodelALT  47609  ormkglobd  47611  or2expropbilem1  47789  funressndmfvrn  47801  f1cof1b  47834  2leaddle2  48055  smonoord  48134  muldvdsfacgt  48143  uniimaprimaeqfv  48151  fundcmpsurbijinjpreimafv  48176  fundcmpsurinjALT  48181  iccpartf  48200  ich2exprop  48240  ichnreuop  48241  ichreuopeq  48242  sprbisymrel  48268  fmtnodvds  48316  proththdlem  48385  gbowgt5  48547  gboge9  48549  gbege6  48550  stgoldbwt  48561  sbgoldbalt  48566  bgoldbnnsum3prm  48589  grimgrtri  48734  grlimgrtri  48788  grlicsym  48798  clnbgr3stgrgrlim  48804  clnbgr3stgrgrlic  48805  gpg5gricstgr3  48875  uspgrbisymrelALT  48940  ssnn0ssfz  49149  ldepspr  49273  seposep  49724  upeu  49969  subthinc  50241  prsthinc  50262  iunord  50474  bnd2d  50479  setrecsss  50499