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  2083  equvel  2494  elex22  3487  spcedv  3566  rspcdf  3577  rspcdva  3591  rspc3dv  3609  spsbcd  3767  opth  5459  euotd  5497  wereu2  5659  unielrel  6276  frpomin  6342  tz7.7  6387  funmo  6553  fvelimad  6949  iinpreima  7065  fompt  7114  fnfvima  7232  resfvresima  7234  fliftfun  7311  fliftval  7315  weniso  7353  riota5f  7396  riotass2  7398  fovcld  7538  ofmpteq  7698  ssorduni  7778  nlimsucg  7838  tfisi  7855  zfrep6OLD  7952  curry1  8099  curry2  8102  fnwelem  8127  funsssuppss  8186  frrlem4  8286  frrlem8  8290  frrlem10  8292  fprlem1  8297  fprlem2  8298  smogt  8354  tfrlem5  8366  omeulem1  8567  oeworde  8579  oelimcl  8586  oeeulem  8587  oeeui  8588  nnawordex  8623  oaabs2  8635  naddssim  8672  naddsuc2  8688  swoso  8729  qliftlem  8796  resixp  8931  domssl  8995  domssr  8996  xpdom3  9063  domunsncan  9065  omxpenlem  9066  domssex  9126  xpf1o  9127  mapdom3  9137  dif1en  9146  findcard  9148  f1dmvrnfibi  9298  fsuppss  9343  fiin  9382  marypha1lem  9393  marypha1  9394  fisupcl  9430  supgtoreq  9431  ordiso2  9477  ordtypelem2  9481  ordtypelem8  9487  wemapso2lem  9514  unxpwdom2  9550  cantnflt  9641  cantnfrescl  9645  oemapvali  9653  cantnflem1d  9657  wemapwe  9666  cnfcom  9669  ttrclss  9689  ttrclselem2  9695  frrlem15  9729  rankr1id  9834  tcrank  9856  cardmin2  9985  infxpenlem  9997  fseqen  10011  ween  10019  ac5num  10020  indcardi  10025  acni2  10030  fodomfi2  10044  infpwfien  10046  inffien  10047  iunfictbso  10098  acacni  10124  dfac12lem2  10128  djuinf  10172  infmap2  10200  ackbij1lem18  10219  ackbij1b  10221  fictb  10227  cfslb2n  10252  cofsmo  10253  cfsmolem  10254  coftr  10257  infpssrlem4  10290  domfin4  10295  fin2i2  10302  isfin2-2  10303  fincssdom  10307  ssfin3ds  10314  fin23lem20  10321  fin23lem30  10326  isf32lem3  10339  fin1a2lem12  10395  fin1a2lem13  10396  hsmexlem2  10411  axdc2lem  10432  imadomg  10518  fnct  10521  iundom2g  10524  iundomg  10525  iundom  10526  unirnfdomd  10552  konigthlem  10553  iunctb  10559  fpwwe2  10628  canthwelem  10635  pwfseqlem3  10645  pwfseqlem5  10648  winalim2  10681  wunelss  10693  r1wunlim  10722  wunex2  10723  tsksdom  10741  tskinf  10754  inttsk  10759  inar1  10760  tskcard  10766  tskurn  10774  gruina  10803  grur1a  10804  grur1  10805  addsrpr  11060  mulsrpr  11061  lemul12a  12073  lemulge11  12077  lediv12a  12108  fiminre2  12163  nngt0  12267  nn0ge2m1nn  12574  peano5uzi  12685  nn0ind-raph  12696  znnn0nn  12707  suprzub  12963  uzsupss  12964  rpge0  13030  fz0fzelfz0  13662  fz0fzdiffz0  13665  ige2m2fzo  13757  elfzodifsumelfzo  13760  elfzom1elp1fzo  13761  fzonfzoufzol  13800  flltdivnn0lt  13866  fldiv  13893  modaddmodup  13970  uzrdgsuci  13996  fzennn  14004  uzindi  14018  fsuppmapnn0fiubex  14028  expcl2lem  14109  leexp1a  14211  modexp  14274  faclbnd  14326  faclbnd6  14335  facavg  14337  hashginv  14370  hashf1rn  14388  hasheqf1od  14389  seqcoll  14501  hashge2el2dif  14517  wrdsymb0  14586  wrdlenge2n0  14589  ccatsymb  14620  swrdnd2  14693  swrdnd0  14695  pfxnd  14725  pfxccat1  14739  swrdpfx  14744  pfxpfx  14745  wrd2ind  14760  pfxccatin12  14770  pfxccat3  14771  swrdccat  14772  pfxccatpfx1  14773  pfxccatpfx2  14774  swrdccatin1d  14780  pfxccatin12d  14782  repswswrd  14821  cshwidxmod  14840  s2f1o  14953  f1oun2prg  14954  wwlktovfo  14995  relexpfld  15086  rtrclreclem3  15097  resqrex  15301  cau3lem  15406  reusq0  15516  rlimcld2  15629  climcn2  15644  isercoll  15719  climsup  15721  caurcvgr  15725  sumeq2ii  15744  summolem3  15765  zsum  15769  fsumadd  15791  fsumsplit1  15796  fsum2dlem  15821  fsum0diag2  15834  fsummulc2  15835  fsumabs  15853  fsumrelem  15859  fsumrlim  15863  fsumo1  15864  o1fsum  15865  fsumiun  15873  qshash  15879  prodeq2ii  15965  prodmolem3  15987  fprodmul  16014  fproddiv  16015  fprod2dlem  16034  fprodsplit1f  16044  sin02gt0  16248  efieq1re  16255  p1modz1  16317  dvdsleabs2  16370  4dvdseven  16431  sumeven  16445  sumodd  16446  divalglem9  16459  smupvallem  16541  algfx  16638  eucalgcvga  16644  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  lcmflefac  16706  qredeq  16715  dvdszzq  16780  fermltl  16843  modprm0  16865  pythagtriplem4  16879  pythagtriplem6  16881  pythagtriplem7  16882  pythagtriplem12  16886  pythagtriplem13  16887  pythagtriplem14  16888  pythagtriplem16  16890  difsqpwdvds  16947  pcmpt  16952  prmreclem2  16977  4sqlem11  17015  vdwlem9  17049  vdwlem11  17051  vdwlem12  17052  0ram  17080  0ram2  17081  0ramcl  17083  ramcl  17089  prmolelcmf  17108  cshwsidrepsw  17153  cshwshashlem2  17156  prmlem1  17167  prmlem2  17180  strfvd  17260  strfv2d  17261  strssd  17265  firest  17485  prdsdsval3  17538  imasbas  17566  imasds  17567  imasaddfnlem  17582  imasaddvallem  17583  imasvscafn  17591  qusaddvallem  17605  qusaddflem  17606  qusaddval  17607  qusaddf  17608  qusmulval  17609  qusmulf  17610  catideu  17731  idinv  17846  brcici  17857  invfuc  18034  2initoinv  18067  initoeu1w  18069  initoeu2lem0  18070  2termoinv  18074  termoeu1w  18076  resspos  18485  resstos  18486  mod2ile  18550  lubss  18569  acsmapd  18610  chnso  18680  lidrididd  18728  gsumval2a  18743  mndind  18887  submefmnd  18954  mgm2nsgrplem4  18983  qusgrp2  19124  mulgnegnn  19150  pgrpsubgsymg  19479  fvcosymgeq  19499  gsmsymgreqlem1  19500  psgnunilem4  19567  pgpssslw  19684  sylow2alem2  19688  fislw  19695  efgsres  19808  rinvmod  19876  gsumval3lem2  19976  gsumzaddlem  19991  gsum2d  20042  nn0gsumfz  20054  telgsums  20063  dprddomcld  20073  ablfac2  20161  qusrng  20258  srgdilem  20274  o2timesd  20292  rglcom4d  20293  ringdilem  20331  qusring2  20416  orngsqr  20947  lssintcl  21063  lbsextlem3  21262  lbsextlem4  21263  prmidl2  21437  qsidomlem2  21450  zringlpirlem3  21583  psgnodpm  21707  psgndiflemB  21719  frlmup4  21920  lindff1  21939  lindfrn  21940  lmisfree  21961  evlseu  22203  mhpmulcl  22281  mptcoe1fsupp  22344  cply1coe0bi  22431  mpfpf1  22480  pf1mpf  22481  mat0dimscm  22595  mdetdiagid  22726  mdet1  22727  mdetunilem9  22746  slesolinv  22806  cramerimp  22812  cpmatmcllem  22844  mptcoe1matfsupp  22928  mp2pm2mp  22937  chpdmat  22967  cctop  23132  subbascn  23380  cnss2  23403  cmpcovf  23517  2ndcctbss  23581  2ndcomap  23584  2ndcsep  23585  comppfsc  23658  ptclsg  23741  dfac14  23744  txcnp  23746  ptcnplem  23747  uptx  23751  txtube  23766  tx2ndc  23777  xkococnlem  23785  elqtop  23823  qtoprest  23843  indishmph  23924  ptcmpfi  23939  kqhmph  23945  csdfil  24020  filssufilg  24037  ufilen  24056  rnelfm  24079  fmfnfmlem4  24083  alexsubALTlem4  24176  ptcmplem4  24181  cnextfvval  24191  cnextcn  24193  cnextfres  24195  tmdgsum2  24222  imasf1oxmet  24501  metss  24634  met2ndci  24648  prdsxmslem2  24655  metust  24684  cfilucfil  24685  metustbl  24692  psmetutop  24693  opnreen  24958  rectbntr0  24959  fsumcn  24998  rescncf  25025  xrhmeo  25074  cnllycmp  25084  lebnumlem1  25089  lebnumlem3  25091  cfilss  25398  iscmet3lem1  25419  iscmet3lem2  25420  ivthicc  25586  ovolsslem  25612  ovoliunlem2  25631  ovoliunnul  25635  ovolicc2lem4  25648  voliunlem3  25680  volsup  25684  uniiccdif  25706  uniioombllem2  25711  volivth  25735  mbfimaopnlem  25783  mbflimsup  25794  i1fd  25809  itg1addlem4  25827  itg2addlem  25886  itg2gt0  25888  limciun  26022  dvadd  26068  dvmul  26069  dvco  26075  dvrec  26083  dvcnv  26105  dvferm  26116  rollelem  26117  dvlip  26121  dvlip2  26123  c1liplem1  26124  c1lip2  26126  dvgt0lem1  26130  dvivthlem1  26136  lhop1lem  26141  dvcnvrelem1  26145  dvcnvrelem2  26146  dvcvx  26148  dvfsumle  26149  dvfsumabs  26151  dvfsumlem1  26154  dvfsumlem2  26155  dvfsumlem4  26157  dvfsumrlim2  26160  dvfsum2  26162  ftc1cn  26171  ftc2ditglem  26173  itgsubstlem  26176  itgpowd  26178  mdegaddle  26200  mdegmullem  26204  deg1sublt  26236  ply1divmo  26262  fta1g  26296  dgrub  26360  dgrnznn  26373  dgradd2  26394  dvply1  26414  plyrem  26435  aalioulem4  26465  aalioulem5  26466  aalioulem6  26467  aaliou2  26470  taylf  26490  ulmdv  26532  psercn2  26552  abelth  26570  abelth2  26571  reeff1olem  26575  efopn  26789  logreclem  26893  isosctrlem2  26950  xrlimcnp  27099  basellem4  27214  ppiwordi  27292  musum  27321  chpub  27350  gausslemma2dlem0c  27488  2sqlem6  27553  addsqnreup  27573  2sqreulem1  27576  2sqreunnlem1  27579  dchrisumlema  27618  dchrisumlem2  27620  dchrisumlem3  27621  pntlemp  27740  pntleml  27741  ostth3  27768  ltsres  27792  noextenddif  27798  nolesgn2ores  27802  nogesgn1ores  27804  nosep1o  27811  nosep2o  27812  nosepeq  27815  nolt02o  27825  noresle  27827  nosupno  27833  nosupbday  27835  nosupres  27837  nosupbnd1lem1  27838  nosupbnd1lem4  27841  nosupbnd1  27844  nosupbnd2lem1  27845  nosupbnd2  27846  noinfno  27848  noinfbday  27850  noinfres  27852  noinfbnd1lem5  27857  noinfbnd1  27859  noinfbnd2lem1  27860  ltlesd  27903  madebday  28059  leadds1  28148  precsexlem10  28375  noseqrdg0  28466  noseqrdgsuc  28467  elnnzs  28560  bdaypw2n0bndlem  28622  iscgrglt  28749  colline  28885  axlowdimlem16  29248  axlowdimlem17  29249  axcontlem3  29257  axcontlem10  29264  uhgr2edg  29499  nbupgruvtxres  29698  cusgrres  29739  cusgrfilem2  29747  vdumgr0  29771  frusgrnn0  29862  wlkp1lem8  29969  pthdivtx  30017  upgrwlkdvde  30027  spthonepeq  30042  usgr2pthlem  30053  cyclnumvtx  30090  lfgrn1cycl  30095  wwlknbp1  30134  wwlknllvtx  30136  wlkiswwlks2lem3  30161  umgr2adedgspth  30238  clwlkclwwlklem3  30293  clwwisshclwwslemlem  30305  clwwisshclwws  30307  clwwlkel  30338  wwlksubclwwlk  30350  eleclclwwlknlem1  30352  eleclclwwlknlem2  30353  erclwwlknref  30361  clwwlknonccat  30388  clwwlknonex2lem2  30400  3wlkdlem4  30454  vdn0conngrumgrv2  30488  eucrctshift  30535  frgrnbnb  30585  frgrncvvdeqlem2  30592  frgrncvvdeqlem3  30593  fusgreghash2wspv  30627  numclwwlk2lem1  30668  numclwlk2lem2f  30669  numclwwlk5  30680  numclwwlk7  30683  frgrreggt1  30685  minvecolem4b  31171  minvecolem4  31173  bcsiALT  31472  ococin  31701  spanpr  31873  pjorthi  31962  nmbdoplbi  32317  nmcoplbi  32321  nmbdfnlbi  32342  nmcfnlbi  32345  nmopcoi  32388  branmfn  32398  hstnmoc  32516  mdsl0  32603  atomli  32675  atcvat4i  32690  atabsi  32694  foresf1o  32791  rabfodom  32792  abrexdomjm  32794  elpreq  32815  ifeqeqx  32829  disjiunel  32882  ac6mapd  32909  aciunf1lem  32948  ffsrn  33014  xlt2addrd  33045  supxrnemnf  33054  ssnnssfz  33073  gsummptres2  33314  gsumfs2d  33322  archirngz  33450  isarchiofld  33460  unitprodclb  33646  elrspunidl  33680  drngidlhash  33686  ssmxidl  33702  1arithidom  33772  1arithufdlem4  33782  constrmon  34079  locfinreflem  34175  cmpcref  34185  fmcncfil  34266  xrge0iifiso  34270  elzdif0  34315  qqhval2lem  34316  esumcst  34398  esumrnmpt2  34403  esumpinfval  34408  esumpinfsum  34412  sigaclci  34467  insiga  34472  ldgenpisys  34501  measres  34557  measdivcstALTV  34560  dya2iocnrect  34616  dya2iocnei  34617  omssubadd  34635  carsggect  34653  carsgclctunlem2  34654  sitgclg  34677  eulerpartlemsv2  34693  eulerpartlemv  34699  eulerpartlemf  34705  eulerpartlemgh  34713  eulerpartlemgs2  34715  ballotlemfp1  34827  ballotlemfrcn0  34865  ftc2re  34930  fdvposlt  34931  fdvposle  34933  bnj1379  35163  bnj580  35246  bnj944  35271  bnj999  35291  bnj1204  35345  bnj1398  35367  onvfowev  35533  cusgredgex  35547  pthacycspth  35582  derangenlem  35596  subfacp1lem3  35607  resconn  35671  cvmliftlem3  35712  satfv0fvfmla0  35838  satfv1fvfmla1  35848  mrsub0  35941  cgrextend  36433  segconeq  36435  trisegint  36453  fwddifnp1  36590  ivthALT  36769  fnessref  36791  refssfne  36792  neibastop1  36793  filnetlem4  36815  ontgval  36865  weiunlem  36897  weiunse  36902  dfttc4  36964  unblimceq0lem  37018  unbdqndv2lem2  37022  unbdqndv2  37023  bj-babygodel  37119  bj-alrimd  37141  bj-exlimd  37153  bj-spim  37171  bj-spime  37172  bj-nnf-spime  37323  bj-spcimdv  37453  bj-spcimdvv  37454  bj-finsumval0  37851  bj-fvimacnv0  37852  dfgcd3  37890  relowlssretop  37931  relowlpssretop  37932  onsucuni3  37935  finxpreclem4  37962  poimirlem18  38211  poimirlem21  38214  poimirlem25  38218  ftc1cnnclem  38264  ftc1cnnc  38265  ftc2nc  38275  dvasin  38277  dvacos  38278  abrexdom  38303  indexdom  38307  mettrifi  38330  equivtotbnd  38351  totbndbnd  38362  prdstotbnd  38367  heibor1lem  38382  bfplem1  38395  bfplem2  38396  opidonOLD  38425  rngodm1dm2  38505  zerdivemp1x  38520  equid1  39597  omllaw5N  39945  cmtcomlemN  39946  cmtbr3N  39952  omlfh3N  39957  atlen0  40008  exatleN  40102  hlrelat3  40110  cvrexchlem  40117  atlelt  40136  cvrat4  40141  4atlem11b  40306  4atlem12b  40309  lneq2at  40476  cdlema1N  40489  cdlemblem  40491  paddss12  40517  paddasslem2  40519  paddasslem4  40521  paddasslem6  40523  paddasslem12  40529  paddunN  40625  poml4N  40651  poml5N  40652  osumcllem6N  40659  pexmidlem6N  40673  pl42lem2N  40678  ltrnu  40819  ltrneq2  40846  trlval2  40861  cdlemd6  40901  cdleme25b  41052  cdleme29b  41073  cdlemefr29exN  41100  ltrniotacnvval  41280  cdlemk28-3  41606  dochexmidlem7  42164  muldvds2d  42689  frlmsnic  43234  nna4b4nsq  43318  mzpsubmpt  43400  mzpsubst  43405  eqrabdioph  43434  rabdiophlem2  43455  elpell14qr2  43515  elpell1qr2  43525  pellfundre  43534  pellfundge  43535  pellfundglb  43538  pellfund14gap  43540  congabseq  43627  jm2.22  43648  jm2.23  43649  jm2.26lem3  43654  wepwsolem  43695  dnwech  43701  aomclem2  43708  aomclem4  43710  pwfi2f1o  43749  onexlimgt  43896  oaltublim  43943  oege1  43959  cantnfub2  43975  cantnfresb  43977  cantnf2  43978  oacl2g  43983  tfsconcatb0  43997  tfsconcatrev  44001  oaun3lem1  44027  oaun3lem2  44028  nadd2rabtr  44037  nadd1suc  44045  naddwordnexlem0  44049  naddwordnexlem3  44052  oawordex3  44053  naddwordnexlem4  44054  oaltom  44057  omltoe  44059  ss2iundf  44311  dssmapf1od  44673  neik0pk1imk0  44699  gneispace  44786  grur1cld  44882  cpcolld  44894  mnuop23d  44902  mnuprdlem1  44908  mnuprdlem2  44909  mnurndlem1  44917  grumnudlem  44921  radcnvrat  44950  sbiota1  45070  ordelordALT  45172  2pm13.193  45187  ee11an  45325  modelaxreplem2  45614  refsumcn  45676  rfcnnnub  45682  disjxp1  45715  xrnmnfpnf  45729  ssinc  45731  nssd  45749  disjf1o  45835  disjinfi  45836  choicefi  45843  axccdom  45864  dmrelrnrel  45868  monoords  45942  fperiodmullem  45948  xadd0ge  45964  xrssre  45990  xrlexaddrp  45994  xrred  46006  infxr  46008  xrnpnfmnf  46114  monoordxrv  46121  monoord2xrv  46123  cvgcaule  46131  fsumiunss  46217  fmul01  46222  fmuldfeqlem1  46224  fmuldfeq  46225  fmul01lt1lem1  46226  fmul01lt1lem2  46227  cncfmptss  46229  climinf  46248  climsuselem1  46249  climsuse  46250  limcperiod  46270  limcrecl  46271  sumnnodd  46272  limcleqr  46284  0ellimcdiv  46289  climleltrp  46316  limsuppnfdlem  46341  limsupresxr  46406  liminfresxr  46407  liminfvalxr  46423  cnrefiisplem  46469  xlimmnfvlem1  46472  xlimpnfvlem1  46476  cncfperiod  46519  icccncfext  46527  cncfiooicclem1  46533  dvbdfbdioolem1  46568  dvnmptdivc  46578  dvdsn1add  46579  dvnmptconst  46581  dvnmul  46583  dvmptfprodlem  46584  dvmptfprod  46585  dvnprodlem2  46587  iblspltprt  46613  itgsubsticclem  46615  itgspltprt  46619  itgsbtaddcnst  46622  stoweidlem3  46643  stoweidlem16  46656  stoweidlem17  46657  stoweidlem19  46659  stoweidlem20  46660  stoweidlem23  46663  stoweidlem25  46665  stoweidlem27  46667  stoweidlem31  46671  stoweidlem34  46674  stoweidlem42  46682  stoweidlem48  46688  stoweidlem51  46691  stoweidlem52  46692  stoweidlem59  46699  wallispilem1  46705  wallispilem3  46707  stirlinglem13  46726  fourierdlem16  46763  fourierdlem20  46767  fourierdlem21  46768  fourierdlem38  46785  fourierdlem42  46789  fourierdlem46  46792  fourierdlem48  46794  fourierdlem49  46795  fourierdlem50  46796  fourierdlem54  46800  fourierdlem68  46814  fourierdlem72  46818  fourierdlem73  46819  fourierdlem76  46822  fourierdlem79  46825  fourierdlem81  46827  fourierdlem86  46832  fourierdlem89  46835  fourierdlem90  46836  fourierdlem91  46837  fourierdlem92  46838  fourierdlem97  46843  fourierdlem101  46847  fourierdlem103  46849  fourierdlem104  46850  fourierdlem111  46857  etransclem24  46898  etransclem25  46899  etransclem28  46902  etransclem41  46915  etransclem44  46918  etransclem48  46922  salexct  46974  dfsalgen2  46981  sge0f1o  47022  sge0rnbnd  47033  sge0split  47049  sge0iunmptlemre  47055  sge0fodjrnlem  47056  sge0iunmpt  47058  nnfoctbdjlem  47095  iundjiunlem  47099  meadjiunlem  47105  ismeannd  47107  meaiuninclem  47120  omeiunle  47157  carageniuncllem1  47161  caratheodorylem1  47166  hoidmvlelem4  47238  hoiqssbllem2  47263  salpreimagelt  47347  salpreimalegt  47349  pimdecfgtioc  47355  smfaddlem2  47404  smflimlem6  47416  nsssmfmbflem  47418  smfpimcclem  47447  quantgodelALT  47515  ormkglobd  47517  or2expropbilem1  47692  funressndmfvrn  47704  f1cof1b  47737  2leaddle2  47958  smonoord  48037  muldvdsfacgt  48046  uniimaprimaeqfv  48054  fundcmpsurbijinjpreimafv  48079  fundcmpsurinjALT  48084  iccpartf  48103  ich2exprop  48143  ichnreuop  48144  ichreuopeq  48145  sprbisymrel  48171  fmtnodvds  48219  proththdlem  48288  gbowgt5  48450  gboge9  48452  gbege6  48453  stgoldbwt  48464  sbgoldbalt  48469  bgoldbnnsum3prm  48492  grimgrtri  48637  grlimgrtri  48691  grlicsym  48701  clnbgr3stgrgrlim  48707  clnbgr3stgrgrlic  48708  gpg5gricstgr3  48778  uspgrbisymrelALT  48843  ssnn0ssfz  49048  ldepspr  49172  seposep  49623  upeu  49868  subthinc  50140  prsthinc  50161  iunord  50373  bnd2d  50378  setrecsss  50398