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  2057  equvel  2456  elex22  3461  spcedv  3548  rspcdf  3559  rspcdva  3573  rspc3dv  3591  spsbcd  3750  opth  5414  euotd  5451  wereu2  5611  unielrel  6221  frpomin  6287  tz7.7  6332  funmo  6497  fvelimad  6889  iinpreima  7002  fompt  7051  fnfvima  7167  resfvresima  7169  fliftfun  7246  fliftval  7250  weniso  7288  riota5f  7331  riotass2  7333  fovcld  7473  ofmpteq  7633  ssorduni  7712  nlimsucg  7772  tfisi  7789  zfrep6  7887  curry1  8034  curry2  8037  fnwelem  8061  funsssuppss  8120  frrlem4  8219  frrlem8  8223  frrlem10  8225  fprlem1  8230  fprlem2  8231  smogt  8287  tfrlem5  8299  omeulem1  8497  oeworde  8508  oelimcl  8515  oeeulem  8516  oeeui  8517  nnawordex  8552  oaabs2  8564  naddssim  8600  naddsuc2  8616  swoso  8656  qliftlem  8722  resixp  8857  domssl  8920  domssr  8921  xpdom3  8988  domunsncan  8990  omxpenlem  8991  domssex  9051  xpf1o  9052  mapdom3  9062  dif1en  9071  findcard  9073  f1dmvrnfibi  9225  fsuppss  9267  fiin  9306  marypha1lem  9317  marypha1  9318  fisupcl  9354  supgtoreq  9355  ordiso2  9401  ordtypelem2  9405  ordtypelem8  9411  wemapso2lem  9438  unxpwdom2  9474  cantnflt  9562  cantnfrescl  9566  oemapvali  9574  cantnflem1d  9578  wemapwe  9587  cnfcom  9590  ttrclss  9610  ttrclselem2  9616  frrlem15  9650  rankr1id  9755  tcrank  9777  cardmin2  9892  infxpenlem  9904  fseqen  9918  ween  9926  ac5num  9927  indcardi  9932  acni2  9937  fodomfi2  9951  infpwfien  9953  inffien  9954  iunfictbso  10005  acacni  10032  dfac12lem2  10036  djuinf  10080  infmap2  10108  ackbij1lem18  10127  ackbij1b  10129  fictb  10135  cfslb2n  10159  cofsmo  10160  cfsmolem  10161  coftr  10164  infpssrlem4  10197  domfin4  10202  fin2i2  10209  isfin2-2  10210  fincssdom  10214  ssfin3ds  10221  fin23lem20  10228  fin23lem30  10233  isf32lem3  10246  fin1a2lem12  10302  fin1a2lem13  10303  hsmexlem2  10318  axdc2lem  10339  imadomg  10425  fnct  10428  iundom2g  10431  iundomg  10432  iundom  10433  unirnfdomd  10458  konigthlem  10459  iunctb  10465  fpwwe2  10534  canthwelem  10541  pwfseqlem3  10551  pwfseqlem5  10554  winalim2  10587  wunelss  10599  r1wunlim  10628  wunex2  10629  tsksdom  10647  tskinf  10660  inttsk  10665  inar1  10666  tskcard  10672  tskurn  10680  gruina  10709  grur1a  10710  grur1  10711  addsrpr  10966  mulsrpr  10967  lemul12a  11979  lemulge11  11984  lediv12a  12015  fiminre2  12070  nngt0  12156  nn0ge2m1nn  12451  peano5uzi  12562  nn0ind-raph  12573  znnn0nn  12584  suprzub  12837  uzsupss  12838  rpge0  12904  fz0fzelfz0  13534  fz0fzdiffz0  13537  ige2m2fzo  13628  elfzodifsumelfzo  13631  elfzom1elp1fzo  13632  fzonfzoufzol  13671  flltdivnn0lt  13737  fldiv  13764  modaddmodup  13841  uzrdgsuci  13867  fzennn  13875  uzindi  13889  fsuppmapnn0fiubex  13899  expcl2lem  13980  leexp1a  14082  modexp  14145  faclbnd  14197  faclbnd6  14206  facavg  14208  hashginv  14241  hashf1rn  14259  hasheqf1od  14260  seqcoll  14371  hashge2el2dif  14387  wrdsymb0  14456  wrdlenge2n0  14459  ccatsymb  14490  swrdnd2  14563  swrdnd0  14565  pfxnd  14595  pfxccat1  14609  swrdpfx  14614  pfxpfx  14615  wrd2ind  14630  pfxccatin12  14640  pfxccat3  14641  swrdccat  14642  pfxccatpfx1  14643  pfxccatpfx2  14644  swrdccatin1d  14650  pfxccatin12d  14652  repswswrd  14691  cshwidxmod  14710  s2f1o  14823  f1oun2prg  14824  wwlktovfo  14865  relexpfld  14956  rtrclreclem3  14967  resqrex  15157  cau3lem  15262  reusq0  15372  rlimcld2  15485  climcn2  15500  isercoll  15575  climsup  15577  caurcvgr  15581  sumeq2ii  15600  summolem3  15621  zsum  15625  fsumadd  15647  fsumsplit1  15652  fsum2dlem  15677  fsum0diag2  15690  fsummulc2  15691  fsumabs  15708  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  qshash  15734  prodeq2ii  15818  prodmolem3  15840  fprodmul  15867  fproddiv  15868  fprod2dlem  15887  fprodsplit1f  15897  sin02gt0  16101  efieq1re  16108  p1modz1  16170  dvdsleabs2  16223  4dvdseven  16284  sumeven  16298  sumodd  16299  divalglem9  16312  smupvallem  16394  algfx  16491  eucalgcvga  16497  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmflefac  16559  qredeq  16568  dvdszzq  16632  fermltl  16695  modprm0  16717  pythagtriplem4  16731  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pythagtriplem16  16742  difsqpwdvds  16799  pcmpt  16804  prmreclem2  16829  4sqlem11  16867  vdwlem9  16901  vdwlem11  16903  vdwlem12  16904  0ram  16932  0ram2  16933  0ramcl  16935  ramcl  16941  prmolelcmf  16960  cshwsidrepsw  17005  cshwshashlem2  17008  prmlem1  17019  prmlem2  17031  strfvd  17111  strfv2d  17112  strssd  17116  firest  17336  prdsdsval3  17389  imasbas  17416  imasds  17417  imasaddfnlem  17432  imasaddvallem  17433  imasvscafn  17441  qusaddvallem  17455  qusaddflem  17456  qusaddval  17457  qusaddf  17458  qusmulval  17459  qusmulf  17460  catideu  17581  idinv  17696  brcici  17707  invfuc  17884  2initoinv  17917  initoeu1w  17919  initoeu2lem0  17920  2termoinv  17924  termoeu1w  17926  resspos  18335  resstos  18336  mod2ile  18400  lubss  18419  acsmapd  18460  chnso  18530  lidrididd  18578  gsumval2a  18593  mndind  18736  submefmnd  18803  mgm2nsgrplem4  18829  qusgrp2  18971  mulgnegnn  18997  pgrpsubgsymg  19321  fvcosymgeq  19341  gsmsymgreqlem1  19342  psgnunilem4  19409  pgpssslw  19526  sylow2alem2  19530  fislw  19537  efgsres  19650  rinvmod  19718  gsumval3lem2  19818  gsumzaddlem  19833  gsum2d  19884  nn0gsumfz  19896  telgsums  19905  dprddomcld  19915  ablfac2  20003  qusrng  20098  srgdilem  20110  o2timesd  20128  rglcom4d  20129  ringdilem  20167  qusring2  20252  orngsqr  20781  lssintcl  20897  lbsextlem3  21097  lbsextlem4  21098  zringlpirlem3  21401  psgnodpm  21525  psgndiflemB  21537  frlmup4  21738  lindff1  21757  lindfrn  21758  lmisfree  21779  evlseu  22018  mhpmulcl  22064  mptcoe1fsupp  22128  cply1coe0bi  22217  mpfpf1  22266  pf1mpf  22267  mat0dimscm  22384  mdetdiagid  22515  mdet1  22516  mdetunilem9  22535  slesolinv  22595  cramerimp  22601  cpmatmcllem  22633  mptcoe1matfsupp  22717  mp2pm2mp  22726  chpdmat  22756  cctop  22921  subbascn  23169  cnss2  23192  cmpcovf  23306  2ndcctbss  23370  2ndcomap  23373  2ndcsep  23374  comppfsc  23447  ptclsg  23530  dfac14  23533  txcnp  23535  ptcnplem  23536  uptx  23540  txtube  23555  tx2ndc  23566  xkococnlem  23574  elqtop  23612  qtoprest  23632  indishmph  23713  ptcmpfi  23728  kqhmph  23734  csdfil  23809  filssufilg  23826  ufilen  23845  rnelfm  23868  fmfnfmlem4  23872  alexsubALTlem4  23965  ptcmplem4  23970  cnextfvval  23980  cnextcn  23982  cnextfres  23984  tmdgsum2  24011  imasf1oxmet  24290  metss  24423  met2ndci  24437  prdsxmslem2  24444  metust  24473  cfilucfil  24474  metustbl  24481  psmetutop  24482  opnreen  24747  rectbntr0  24748  fsumcn  24788  rescncf  24817  xrhmeo  24871  cnllycmp  24882  lebnumlem1  24887  lebnumlem3  24889  cfilss  25197  iscmet3lem1  25218  iscmet3lem2  25219  ivthicc  25386  ovolsslem  25412  ovoliunlem2  25431  ovoliunnul  25435  ovolicc2lem4  25448  voliunlem3  25480  volsup  25484  uniiccdif  25506  uniioombllem2  25511  volivth  25535  mbfimaopnlem  25583  mbflimsup  25594  i1fd  25609  itg1addlem4  25627  itg2addlem  25686  itg2gt0  25688  limciun  25822  dvadd  25870  dvmul  25871  dvco  25878  dvrec  25886  dvcnv  25908  dvferm  25919  rollelem  25920  dvlip  25925  dvlip2  25927  c1liplem1  25928  c1lip2  25930  dvgt0lem1  25934  dvivthlem1  25940  lhop1lem  25945  dvcnvrelem1  25949  dvcnvrelem2  25950  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem4  25963  dvfsumrlim2  25966  dvfsum2  25968  ftc1cn  25977  ftc2ditglem  25979  itgsubstlem  25982  itgpowd  25984  mdegaddle  26006  mdegmullem  26010  deg1sublt  26042  ply1divmo  26068  fta1g  26102  dgrub  26166  dgrnznn  26179  dgradd2  26201  dvply1  26218  plyrem  26240  aalioulem4  26270  aalioulem5  26271  aalioulem6  26272  aaliou2  26275  taylf  26295  ulmdv  26339  psercn2  26359  psercn2OLD  26360  abelth  26378  abelth2  26379  reeff1olem  26383  efopn  26594  logreclem  26699  isosctrlem2  26756  xrlimcnp  26905  basellem4  27021  ppiwordi  27099  musum  27128  chpub  27158  gausslemma2dlem0c  27296  2sqlem6  27361  addsqnreup  27381  2sqreulem1  27384  2sqreunnlem1  27387  dchrisumlema  27426  dchrisumlem2  27428  dchrisumlem3  27429  pntlemp  27548  pntleml  27549  ostth3  27576  sltres  27601  noextenddif  27607  nolesgn2ores  27611  nogesgn1ores  27613  nosep1o  27620  nosep2o  27621  nosepeq  27624  nolt02o  27634  noresle  27636  nosupno  27642  nosupbday  27644  nosupres  27646  nosupbnd1lem1  27647  nosupbnd1lem4  27650  nosupbnd1  27653  nosupbnd2lem1  27654  nosupbnd2  27655  noinfno  27657  noinfbday  27659  noinfres  27661  noinfbnd1lem5  27666  noinfbnd1  27668  noinfbnd2lem1  27669  sltled  27708  madebday  27845  sleadd1  27932  precsexlem10  28154  noseqrdg0  28237  noseqrdgsuc  28238  elnnzs  28325  iscgrglt  28492  colline  28627  axlowdimlem16  28935  axlowdimlem17  28936  axcontlem3  28944  axcontlem10  28951  uhgr2edg  29186  nbupgruvtxres  29385  cusgrres  29427  cusgrfilem2  29435  vdumgr0  29459  frusgrnn0  29550  wlkp1lem8  29657  pthdivtx  29705  upgrwlkdvde  29715  spthonepeq  29730  usgr2pthlem  29741  cyclnumvtx  29778  lfgrn1cycl  29783  wwlknbp1  29822  wwlknllvtx  29824  wlkiswwlks2lem3  29849  umgr2adedgspth  29926  clwlkclwwlklem3  29981  clwwisshclwwslemlem  29993  clwwisshclwws  29995  clwwlkel  30026  wwlksubclwwlk  30038  eleclclwwlknlem1  30040  eleclclwwlknlem2  30041  erclwwlknref  30049  clwwlknonccat  30076  clwwlknonex2lem2  30088  3wlkdlem4  30142  vdn0conngrumgrv2  30176  eucrctshift  30223  frgrnbnb  30273  frgrncvvdeqlem2  30280  frgrncvvdeqlem3  30281  fusgreghash2wspv  30315  numclwwlk2lem1  30356  numclwlk2lem2f  30357  numclwwlk5  30368  numclwwlk7  30371  frgrreggt1  30373  minvecolem4b  30858  minvecolem4  30860  bcsiALT  31159  ococin  31388  spanpr  31560  pjorthi  31649  nmbdoplbi  32004  nmcoplbi  32008  nmbdfnlbi  32029  nmcfnlbi  32032  nmopcoi  32075  branmfn  32085  hstnmoc  32203  mdsl0  32290  atomli  32362  atcvat4i  32377  atabsi  32381  foresf1o  32484  rabfodom  32485  abrexdomjm  32487  elpreq  32508  ifeqeqx  32522  disjiunel  32576  ac6mapd  32606  aciunf1lem  32644  ffsrn  32711  xlt2addrd  32742  supxrnemnf  32751  ssnnssfz  32770  gsummptres2  33033  gsumfs2d  33035  archirngz  33158  isarchiofld  33168  unitprodclb  33354  elrspunidl  33393  drngidlhash  33399  prmidl2  33406  qsidomlem2  33418  ssmxidl  33439  1arithidom  33502  1arithufdlem4  33512  constrmon  33757  locfinreflem  33853  cmpcref  33863  fmcncfil  33944  xrge0iifiso  33948  elzdif0  33993  qqhval2lem  33994  esumcst  34076  esumrnmpt2  34081  esumpinfval  34086  esumpinfsum  34090  sigaclci  34145  insiga  34150  ldgenpisys  34179  measres  34235  measdivcstALTV  34238  dya2iocnrect  34294  dya2iocnei  34295  omssubadd  34313  carsggect  34331  carsgclctunlem2  34332  sitgclg  34355  eulerpartlemsv2  34371  eulerpartlemv  34377  eulerpartlemf  34383  eulerpartlemgh  34391  eulerpartlemgs2  34393  ballotlemfp1  34505  ballotlemfrcn0  34543  ftc2re  34611  fdvposlt  34612  fdvposle  34614  bnj1379  34842  bnj580  34925  bnj944  34950  bnj999  34970  bnj1204  35024  bnj1398  35046  cusgredgex  35166  pthacycspth  35201  derangenlem  35215  subfacp1lem3  35226  resconn  35290  cvmliftlem3  35331  satfv0fvfmla0  35457  satfv1fvfmla1  35467  mrsub0  35560  cgrextend  36052  segconeq  36054  trisegint  36072  fwddifnp1  36209  ivthALT  36379  fnessref  36401  refssfne  36402  neibastop1  36403  filnetlem4  36425  ontgval  36475  weiunlem2  36507  weiunse  36512  unblimceq0lem  36550  unbdqndv2lem2  36554  unbdqndv2  36555  bj-babygodel  36647  bj-alrimd  36664  bj-exlimd  36669  bj-spcimdv  36939  bj-spcimdvv  36940  bj-finsumval0  37329  bj-fvimacnv0  37330  dfgcd3  37368  relowlssretop  37407  relowlpssretop  37408  onsucuni3  37411  finxpreclem4  37438  poimirlem18  37688  poimirlem21  37691  poimirlem25  37695  ftc1cnnclem  37741  ftc1cnnc  37742  ftc2nc  37752  dvasin  37754  dvacos  37755  abrexdom  37780  indexdom  37784  mettrifi  37807  equivtotbnd  37828  totbndbnd  37839  prdstotbnd  37844  heibor1lem  37859  bfplem1  37872  bfplem2  37873  opidonOLD  37902  rngodm1dm2  37982  zerdivemp1x  37997  equid1  39008  omllaw5N  39356  cmtcomlemN  39357  cmtbr3N  39363  omlfh3N  39368  atlen0  39419  exatleN  39513  hlrelat3  39521  cvrexchlem  39528  atlelt  39547  cvrat4  39552  4atlem11b  39717  4atlem12b  39720  lneq2at  39887  cdlema1N  39900  cdlemblem  39902  paddss12  39928  paddasslem2  39930  paddasslem4  39932  paddasslem6  39934  paddasslem12  39940  paddunN  40036  poml4N  40062  poml5N  40063  osumcllem6N  40070  pexmidlem6N  40084  pl42lem2N  40089  ltrnu  40230  ltrneq2  40257  trlval2  40272  cdlemd6  40312  cdleme25b  40463  cdleme29b  40484  cdlemefr29exN  40511  ltrniotacnvval  40691  cdlemk28-3  41017  dochexmidlem7  41575  muldvds2d  42101  frlmsnic  42643  nna4b4nsq  42763  mzpsubmpt  42846  mzpsubst  42851  eqrabdioph  42880  rabdiophlem2  42905  elpell14qr2  42965  elpell1qr2  42975  pellfundre  42984  pellfundge  42985  pellfundglb  42988  pellfund14gap  42990  congabseq  43077  jm2.22  43098  jm2.23  43099  jm2.26lem3  43104  wepwsolem  43145  dnwech  43151  aomclem2  43158  aomclem4  43160  pwfi2f1o  43199  onexlimgt  43346  oaltublim  43393  oege1  43409  cantnfub2  43425  cantnfresb  43427  cantnf2  43428  oacl2g  43433  tfsconcatb0  43447  tfsconcatrev  43451  oaun3lem1  43477  oaun3lem2  43478  nadd2rabtr  43487  nadd1suc  43495  naddwordnexlem0  43499  naddwordnexlem3  43502  oawordex3  43503  naddwordnexlem4  43504  oaltom  43508  omltoe  43510  ss2iundf  43762  dssmapf1od  44124  neik0pk1imk0  44150  gneispace  44237  grur1cld  44335  cpcolld  44361  mnuop23d  44369  mnuprdlem1  44375  mnuprdlem2  44376  mnurndlem1  44384  grumnudlem  44388  radcnvrat  44417  sbiota1  44537  ordelordALT  44640  2pm13.193  44655  ee11an  44793  modelaxreplem2  45082  refsumcn  45137  rfcnnnub  45143  disjxp1  45176  xrnmnfpnf  45190  ssinc  45194  nssd  45212  disjf1o  45298  disjinfi  45299  choicefi  45307  axccdom  45329  dmrelrnrel  45333  monoords  45408  fperiodmullem  45414  xadd0ge  45430  xrssre  45457  xrlexaddrp  45461  xrred  45473  infxr  45475  xrnpnfmnf  45582  monoordxrv  45589  monoord2xrv  45591  cvgcaule  45599  fsumiunss  45685  fmul01  45690  fmuldfeqlem1  45692  fmuldfeq  45693  fmul01lt1lem1  45694  fmul01lt1lem2  45695  cncfmptss  45697  climinf  45716  climsuselem1  45717  climsuse  45718  limcperiod  45738  limcrecl  45739  sumnnodd  45740  limcleqr  45752  0ellimcdiv  45757  climleltrp  45784  limsuppnfdlem  45809  limsupresxr  45874  liminfresxr  45875  liminfvalxr  45891  cnrefiisplem  45937  xlimmnfvlem1  45940  xlimpnfvlem1  45944  cncfperiod  45987  icccncfext  45995  cncfiooicclem1  46001  dvbdfbdioolem1  46036  dvnmptdivc  46046  dvdsn1add  46047  dvnmptconst  46049  dvnmul  46051  dvmptfprodlem  46052  dvmptfprod  46053  dvnprodlem2  46055  iblspltprt  46081  itgsubsticclem  46083  itgspltprt  46087  itgsbtaddcnst  46090  stoweidlem3  46111  stoweidlem16  46124  stoweidlem17  46125  stoweidlem19  46127  stoweidlem20  46128  stoweidlem23  46131  stoweidlem25  46133  stoweidlem27  46135  stoweidlem31  46139  stoweidlem34  46142  stoweidlem42  46150  stoweidlem48  46156  stoweidlem51  46159  stoweidlem52  46160  stoweidlem59  46167  wallispilem1  46173  wallispilem3  46175  stirlinglem13  46194  fourierdlem16  46231  fourierdlem20  46235  fourierdlem21  46236  fourierdlem38  46253  fourierdlem42  46257  fourierdlem46  46260  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem54  46268  fourierdlem68  46282  fourierdlem72  46286  fourierdlem73  46287  fourierdlem76  46290  fourierdlem79  46293  fourierdlem81  46295  fourierdlem86  46300  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem92  46306  fourierdlem97  46311  fourierdlem101  46315  fourierdlem103  46317  fourierdlem104  46318  fourierdlem111  46325  etransclem24  46366  etransclem25  46367  etransclem28  46370  etransclem41  46383  etransclem44  46386  etransclem48  46390  salexct  46442  dfsalgen2  46449  sge0f1o  46490  sge0rnbnd  46501  sge0split  46517  sge0iunmptlemre  46523  sge0fodjrnlem  46524  sge0iunmpt  46526  nnfoctbdjlem  46563  iundjiunlem  46567  meadjiunlem  46573  ismeannd  46575  meaiuninclem  46588  omeiunle  46625  carageniuncllem1  46629  caratheodorylem1  46634  hoidmvlelem4  46706  hoiqssbllem2  46731  salpreimagelt  46815  salpreimalegt  46817  pimdecfgtioc  46823  smfaddlem2  46872  smflimlem6  46884  nsssmfmbflem  46886  smfpimcclem  46915  ormkglobd  46983  or2expropbilem1  47142  funressndmfvrn  47154  f1cof1b  47187  2leaddle2  47408  smonoord  47481  uniimaprimaeqfv  47492  fundcmpsurbijinjpreimafv  47517  fundcmpsurinjALT  47522  iccpartf  47541  ich2exprop  47581  ichnreuop  47582  ichreuopeq  47583  sprbisymrel  47609  fmtnodvds  47654  proththdlem  47723  gbowgt5  47872  gboge9  47874  gbege6  47875  stgoldbwt  47886  sbgoldbalt  47891  bgoldbnnsum3prm  47914  grimgrtri  48059  grlimgrtri  48113  grlicsym  48123  clnbgr3stgrgrlim  48129  clnbgr3stgrgrlic  48130  gpg5gricstgr3  48200  uspgrbisymrelALT  48265  ssnn0ssfz  48459  ldepspr  48584  seposep  49036  upeu  49282  subthinc  49554  prsthinc  49575  iunord  49787  bnd2d  49792  setrecsss  49812