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  2055  equvel  2454  elex22  3461  spcedv  3553  rspcdf  3564  rspcdva  3578  rspc3dv  3596  spsbcd  3756  opth  5419  euotd  5456  wereu2  5616  unielrel  6222  frpomin  6288  tz7.7  6333  funmo  6498  fvelimad  6890  iinpreima  7003  fompt  7052  fnfvima  7169  resfvresima  7171  fliftfun  7249  fliftval  7253  weniso  7291  riota5f  7334  riotass2  7336  fovcld  7476  ofmpteq  7636  ssorduni  7715  nlimsucg  7775  tfisi  7792  zfrep6  7890  curry1  8037  curry2  8040  fnwelem  8064  funsssuppss  8123  frrlem4  8222  frrlem8  8226  frrlem10  8228  fprlem1  8233  fprlem2  8234  smogt  8290  tfrlem5  8302  omeulem1  8500  oeworde  8511  oelimcl  8518  oeeulem  8519  oeeui  8520  nnawordex  8555  oaabs2  8567  naddssim  8603  naddsuc2  8619  swoso  8659  qliftlem  8725  resixp  8860  domssl  8923  domssr  8924  xpdom3  8992  domunsncan  8994  omxpenlem  8995  domssex  9055  xpf1o  9056  mapdom3  9066  dif1en  9075  findcard  9077  f1dmvrnfibi  9231  fsuppss  9273  fiin  9312  marypha1lem  9323  marypha1  9324  fisupcl  9360  supgtoreq  9361  ordiso2  9407  ordtypelem2  9411  ordtypelem8  9417  wemapso2lem  9444  unxpwdom2  9480  cantnflt  9568  cantnfrescl  9572  oemapvali  9580  cantnflem1d  9584  wemapwe  9593  cnfcom  9596  ttrclss  9616  ttrclselem2  9622  frrlem15  9653  rankr1id  9758  tcrank  9780  cardmin2  9895  infxpenlem  9907  fseqen  9921  ween  9929  ac5num  9930  indcardi  9935  acni2  9940  fodomfi2  9954  infpwfien  9956  inffien  9957  iunfictbso  10008  acacni  10035  dfac12lem2  10039  djuinf  10083  infmap2  10111  ackbij1lem18  10130  ackbij1b  10132  fictb  10138  cfslb2n  10162  cofsmo  10163  cfsmolem  10164  coftr  10167  infpssrlem4  10200  domfin4  10205  fin2i2  10212  isfin2-2  10213  fincssdom  10217  ssfin3ds  10224  fin23lem20  10231  fin23lem30  10236  isf32lem3  10249  fin1a2lem12  10305  fin1a2lem13  10306  hsmexlem2  10321  axdc2lem  10342  imadomg  10428  fnct  10431  iundom2g  10434  iundomg  10435  iundom  10436  unirnfdomd  10461  konigthlem  10462  iunctb  10468  fpwwe2  10537  canthwelem  10544  pwfseqlem3  10554  pwfseqlem5  10557  winalim2  10590  wunelss  10602  r1wunlim  10631  wunex2  10632  tsksdom  10650  tskinf  10663  inttsk  10668  inar1  10669  tskcard  10675  tskurn  10683  gruina  10712  grur1a  10713  grur1  10714  addsrpr  10969  mulsrpr  10970  lemul12a  11982  lemulge11  11987  lediv12a  12018  fiminre2  12073  nngt0  12159  nn0ge2m1nn  12454  peano5uzi  12565  nn0ind-raph  12576  znnn0nn  12587  suprzub  12840  uzsupss  12841  rpge0  12907  fz0fzelfz0  13537  fz0fzdiffz0  13540  ige2m2fzo  13631  elfzodifsumelfzo  13634  elfzom1elp1fzo  13635  fzonfzoufzol  13673  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  14489  swrdnd2  14562  swrdnd0  14564  pfxnd  14594  pfxccat1  14608  swrdpfx  14613  pfxpfx  14614  wrd2ind  14629  pfxccatin12  14639  pfxccat3  14640  swrdccat  14641  pfxccatpfx1  14642  pfxccatpfx2  14643  swrdccatin1d  14649  pfxccatin12d  14651  repswswrd  14690  cshwidxmod  14709  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  lidrididd  18544  gsumval2a  18559  mndind  18702  submefmnd  18769  mgm2nsgrplem4  18795  qusgrp2  18937  mulgnegnn  18963  pgrpsubgsymg  19288  fvcosymgeq  19308  gsmsymgreqlem1  19309  psgnunilem4  19376  pgpssslw  19493  sylow2alem2  19497  fislw  19504  efgsres  19617  rinvmod  19685  gsumval3lem2  19785  gsumzaddlem  19800  gsum2d  19851  nn0gsumfz  19863  telgsums  19872  dprddomcld  19882  ablfac2  19970  qusrng  20065  srgdilem  20077  o2timesd  20095  rglcom4d  20096  ringdilem  20134  qusring2  20219  orngsqr  20751  lssintcl  20867  lbsextlem3  21067  lbsextlem4  21068  zringlpirlem3  21371  psgnodpm  21495  psgndiflemB  21507  frlmup4  21708  lindff1  21727  lindfrn  21728  lmisfree  21749  evlseu  21988  mhpmulcl  22034  mptcoe1fsupp  22098  cply1coe0bi  22187  mpfpf1  22236  pf1mpf  22237  mat0dimscm  22354  mdetdiagid  22485  mdet1  22486  mdetunilem9  22505  slesolinv  22565  cramerimp  22571  cpmatmcllem  22603  mptcoe1matfsupp  22687  mp2pm2mp  22696  chpdmat  22726  cctop  22891  subbascn  23139  cnss2  23162  cmpcovf  23276  2ndcctbss  23340  2ndcomap  23343  2ndcsep  23344  comppfsc  23417  ptclsg  23500  dfac14  23503  txcnp  23505  ptcnplem  23506  uptx  23510  txtube  23525  tx2ndc  23536  xkococnlem  23544  elqtop  23582  qtoprest  23602  indishmph  23683  ptcmpfi  23698  kqhmph  23704  csdfil  23779  filssufilg  23796  ufilen  23815  rnelfm  23838  fmfnfmlem4  23842  alexsubALTlem4  23935  ptcmplem4  23940  cnextfvval  23950  cnextcn  23952  cnextfres  23954  tmdgsum2  23981  imasf1oxmet  24261  metss  24394  met2ndci  24408  prdsxmslem2  24415  metust  24444  cfilucfil  24445  metustbl  24452  psmetutop  24453  opnreen  24718  rectbntr0  24719  fsumcn  24759  rescncf  24788  xrhmeo  24842  cnllycmp  24853  lebnumlem1  24858  lebnumlem3  24860  cfilss  25168  iscmet3lem1  25189  iscmet3lem2  25190  ivthicc  25357  ovolsslem  25383  ovoliunlem2  25402  ovoliunnul  25406  ovolicc2lem4  25419  voliunlem3  25451  volsup  25455  uniiccdif  25477  uniioombllem2  25482  volivth  25506  mbfimaopnlem  25554  mbflimsup  25565  i1fd  25580  itg1addlem4  25598  itg2addlem  25657  itg2gt0  25659  limciun  25793  dvadd  25841  dvmul  25842  dvco  25849  dvrec  25857  dvcnv  25879  dvferm  25890  rollelem  25891  dvlip  25896  dvlip2  25898  c1liplem1  25899  c1lip2  25901  dvgt0lem1  25905  dvivthlem1  25911  lhop1lem  25916  dvcnvrelem1  25920  dvcnvrelem2  25921  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  dvfsumrlim2  25937  dvfsum2  25939  ftc1cn  25948  ftc2ditglem  25950  itgsubstlem  25953  itgpowd  25955  mdegaddle  25977  mdegmullem  25981  deg1sublt  26013  ply1divmo  26039  fta1g  26073  dgrub  26137  dgrnznn  26150  dgradd2  26172  dvply1  26189  plyrem  26211  aalioulem4  26241  aalioulem5  26242  aalioulem6  26243  aaliou2  26246  taylf  26266  ulmdv  26310  psercn2  26330  psercn2OLD  26331  abelth  26349  abelth2  26350  reeff1olem  26354  efopn  26565  logreclem  26670  isosctrlem2  26727  xrlimcnp  26876  basellem4  26992  ppiwordi  27070  musum  27099  chpub  27129  gausslemma2dlem0c  27267  2sqlem6  27332  addsqnreup  27352  2sqreulem1  27355  2sqreunnlem1  27358  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  pntlemp  27519  pntleml  27520  ostth3  27547  sltres  27572  noextenddif  27578  nolesgn2ores  27582  nogesgn1ores  27584  nosep1o  27591  nosep2o  27592  nosepeq  27595  nolt02o  27605  noresle  27607  nosupno  27613  nosupbday  27615  nosupres  27617  nosupbnd1lem1  27618  nosupbnd1lem4  27621  nosupbnd1  27624  nosupbnd2lem1  27625  nosupbnd2  27626  noinfno  27628  noinfbday  27630  noinfres  27632  noinfbnd1lem5  27637  noinfbnd1  27639  noinfbnd2lem1  27640  sltled  27679  madebday  27814  sleadd1  27901  precsexlem10  28123  noseqrdg0  28206  noseqrdgsuc  28207  elnnzs  28294  iscgrglt  28459  colline  28594  axlowdimlem16  28902  axlowdimlem17  28903  axcontlem3  28911  axcontlem10  28918  uhgr2edg  29153  nbupgruvtxres  29352  cusgrres  29394  cusgrfilem2  29402  vdumgr0  29426  frusgrnn0  29517  wlkp1lem8  29624  pthdivtx  29672  upgrwlkdvde  29682  spthonepeq  29697  usgr2pthlem  29708  cyclnumvtx  29745  lfgrn1cycl  29750  wwlknbp1  29789  wwlknllvtx  29791  wlkiswwlks2lem3  29816  umgr2adedgspth  29893  clwlkclwwlklem3  29945  clwwisshclwwslemlem  29957  clwwisshclwws  29959  clwwlkel  29990  wwlksubclwwlk  30002  eleclclwwlknlem1  30004  eleclclwwlknlem2  30005  erclwwlknref  30013  clwwlknonccat  30040  clwwlknonex2lem2  30052  3wlkdlem4  30106  vdn0conngrumgrv2  30140  eucrctshift  30187  frgrnbnb  30237  frgrncvvdeqlem2  30244  frgrncvvdeqlem3  30245  fusgreghash2wspv  30279  numclwwlk2lem1  30320  numclwlk2lem2f  30321  numclwwlk5  30332  numclwwlk7  30335  frgrreggt1  30337  minvecolem4b  30822  minvecolem4  30824  bcsiALT  31123  ococin  31352  spanpr  31524  pjorthi  31613  nmbdoplbi  31968  nmcoplbi  31972  nmbdfnlbi  31993  nmcfnlbi  31996  nmopcoi  32039  branmfn  32049  hstnmoc  32167  mdsl0  32254  atomli  32326  atcvat4i  32341  atabsi  32345  foresf1o  32448  rabfodom  32449  abrexdomjm  32451  elpreq  32472  ifeqeqx  32486  disjiunel  32540  ac6mapd  32568  aciunf1lem  32606  ffsrn  32673  xlt2addrd  32703  supxrnemnf  32712  ssnnssfz  32731  chnso  32957  gsummptres2  33007  gsumfs2d  33009  archirngz  33132  isarchiofld  33142  unitprodclb  33327  elrspunidl  33366  drngidlhash  33372  prmidl2  33379  qsidomlem2  33391  ssmxidl  33412  1arithidom  33475  1arithufdlem4  33485  constrmon  33717  locfinreflem  33813  cmpcref  33823  fmcncfil  33904  xrge0iifiso  33908  elzdif0  33953  qqhval2lem  33954  esumcst  34036  esumrnmpt2  34041  esumpinfval  34046  esumpinfsum  34050  sigaclci  34105  insiga  34110  ldgenpisys  34139  measres  34195  measdivcstALTV  34198  dya2iocnrect  34255  dya2iocnei  34256  omssubadd  34274  carsggect  34292  carsgclctunlem2  34293  sitgclg  34316  eulerpartlemsv2  34332  eulerpartlemv  34338  eulerpartlemf  34344  eulerpartlemgh  34352  eulerpartlemgs2  34354  ballotlemfp1  34466  ballotlemfrcn0  34504  ftc2re  34572  fdvposlt  34573  fdvposle  34575  bnj1379  34803  bnj580  34886  bnj944  34911  bnj999  34931  bnj1204  34985  bnj1398  35007  cusgredgex  35105  pthacycspth  35140  derangenlem  35154  subfacp1lem3  35165  resconn  35229  cvmliftlem3  35270  satfv0fvfmla0  35396  satfv1fvfmla1  35406  mrsub0  35499  cgrextend  35992  segconeq  35994  trisegint  36012  fwddifnp1  36149  ivthALT  36319  fnessref  36341  refssfne  36342  neibastop1  36343  filnetlem4  36365  ontgval  36415  weiunlem2  36447  weiunse  36452  unblimceq0lem  36490  unbdqndv2lem2  36494  unbdqndv2  36495  bj-babygodel  36587  bj-alrimd  36604  bj-exlimd  36609  bj-spcimdv  36879  bj-spcimdvv  36880  bj-finsumval0  37269  bj-fvimacnv0  37270  dfgcd3  37308  relowlssretop  37347  relowlpssretop  37348  onsucuni3  37351  finxpreclem4  37378  poimirlem18  37628  poimirlem21  37631  poimirlem25  37635  ftc1cnnclem  37681  ftc1cnnc  37682  ftc2nc  37692  dvasin  37694  dvacos  37695  abrexdom  37720  indexdom  37724  mettrifi  37747  equivtotbnd  37768  totbndbnd  37779  prdstotbnd  37784  heibor1lem  37799  bfplem1  37812  bfplem2  37813  opidonOLD  37842  rngodm1dm2  37922  zerdivemp1x  37937  equid1  38888  omllaw5N  39236  cmtcomlemN  39237  cmtbr3N  39243  omlfh3N  39248  atlen0  39299  exatleN  39393  hlrelat3  39401  cvrexchlem  39408  atlelt  39427  cvrat4  39432  4atlem11b  39597  4atlem12b  39600  lneq2at  39767  cdlema1N  39780  cdlemblem  39782  paddss12  39808  paddasslem2  39810  paddasslem4  39812  paddasslem6  39814  paddasslem12  39820  paddunN  39916  poml4N  39942  poml5N  39943  osumcllem6N  39950  pexmidlem6N  39964  pl42lem2N  39969  ltrnu  40110  ltrneq2  40137  trlval2  40152  cdlemd6  40192  cdleme25b  40343  cdleme29b  40364  cdlemefr29exN  40391  ltrniotacnvval  40571  cdlemk28-3  40897  dochexmidlem7  41455  muldvds2d  41981  frlmsnic  42523  nna4b4nsq  42643  mzpsubmpt  42726  mzpsubst  42731  eqrabdioph  42760  rabdiophlem2  42785  elpell14qr2  42845  elpell1qr2  42855  pellfundre  42864  pellfundge  42865  pellfundglb  42868  pellfund14gap  42870  congabseq  42957  jm2.22  42978  jm2.23  42979  jm2.26lem3  42984  wepwsolem  43025  dnwech  43031  aomclem2  43038  aomclem4  43040  pwfi2f1o  43079  onexlimgt  43226  oaltublim  43273  oege1  43289  cantnfub2  43305  cantnfresb  43307  cantnf2  43308  oacl2g  43313  tfsconcatb0  43327  tfsconcatrev  43331  oaun3lem1  43357  oaun3lem2  43358  nadd2rabtr  43367  nadd1suc  43375  naddwordnexlem0  43379  naddwordnexlem3  43382  oawordex3  43383  naddwordnexlem4  43384  oaltom  43388  omltoe  43390  ss2iundf  43642  dssmapf1od  44004  neik0pk1imk0  44030  gneispace  44117  grur1cld  44215  cpcolld  44241  mnuop23d  44249  mnuprdlem1  44255  mnuprdlem2  44256  mnurndlem1  44264  grumnudlem  44268  radcnvrat  44297  sbiota1  44417  ordelordALT  44521  2pm13.193  44536  ee11an  44674  modelaxreplem2  44963  refsumcn  45018  rfcnnnub  45024  disjxp1  45057  xrnmnfpnf  45071  ssinc  45075  nssd  45093  disjf1o  45179  disjinfi  45180  choicefi  45188  axccdom  45210  dmrelrnrel  45214  monoords  45289  fperiodmullem  45295  xadd0ge  45311  xrssre  45338  xrlexaddrp  45342  xrred  45354  infxr  45356  xrnpnfmnf  45463  monoordxrv  45470  monoord2xrv  45472  cvgcaule  45480  fsumiunss  45566  fmul01  45571  fmuldfeqlem1  45573  fmuldfeq  45574  fmul01lt1lem1  45575  fmul01lt1lem2  45576  cncfmptss  45578  climinf  45597  climsuselem1  45598  climsuse  45599  limcperiod  45619  limcrecl  45620  sumnnodd  45621  limcleqr  45635  0ellimcdiv  45640  climleltrp  45667  limsuppnfdlem  45692  limsupresxr  45757  liminfresxr  45758  liminfvalxr  45774  cnrefiisplem  45820  xlimmnfvlem1  45823  xlimpnfvlem1  45827  cncfperiod  45870  icccncfext  45878  cncfiooicclem1  45884  dvbdfbdioolem1  45919  dvnmptdivc  45929  dvdsn1add  45930  dvnmptconst  45932  dvnmul  45934  dvmptfprodlem  45935  dvmptfprod  45936  dvnprodlem2  45938  iblspltprt  45964  itgsubsticclem  45966  itgspltprt  45970  itgsbtaddcnst  45973  stoweidlem3  45994  stoweidlem16  46007  stoweidlem17  46008  stoweidlem19  46010  stoweidlem20  46011  stoweidlem23  46014  stoweidlem25  46016  stoweidlem27  46018  stoweidlem31  46022  stoweidlem34  46025  stoweidlem42  46033  stoweidlem48  46039  stoweidlem51  46042  stoweidlem52  46043  stoweidlem59  46050  wallispilem1  46056  wallispilem3  46058  stirlinglem13  46077  fourierdlem16  46114  fourierdlem20  46118  fourierdlem21  46119  fourierdlem38  46136  fourierdlem42  46140  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem54  46151  fourierdlem68  46165  fourierdlem72  46169  fourierdlem73  46170  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem86  46183  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem92  46189  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  etransclem24  46249  etransclem25  46250  etransclem28  46253  etransclem41  46266  etransclem44  46269  etransclem48  46273  salexct  46325  dfsalgen2  46332  sge0f1o  46373  sge0rnbnd  46384  sge0split  46400  sge0iunmptlemre  46406  sge0fodjrnlem  46407  sge0iunmpt  46409  nnfoctbdjlem  46446  iundjiunlem  46450  meadjiunlem  46456  ismeannd  46458  meaiuninclem  46471  omeiunle  46508  carageniuncllem1  46512  caratheodorylem1  46517  hoidmvlelem4  46589  hoiqssbllem2  46614  salpreimagelt  46698  salpreimalegt  46700  pimdecfgtioc  46706  smfaddlem2  46755  smflimlem6  46767  nsssmfmbflem  46769  smfpimcclem  46798  ormkglobd  46866  or2expropbilem1  47026  funressndmfvrn  47038  f1cof1b  47071  2leaddle2  47292  smonoord  47365  uniimaprimaeqfv  47376  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjALT  47406  iccpartf  47425  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  sprbisymrel  47493  fmtnodvds  47538  proththdlem  47607  gbowgt5  47756  gboge9  47758  gbege6  47759  stgoldbwt  47770  sbgoldbalt  47775  bgoldbnnsum3prm  47798  grimgrtri  47943  grlimgrtri  47997  grlicsym  48007  clnbgr3stgrgrlim  48013  clnbgr3stgrgrlic  48014  gpg5gricstgr3  48084  uspgrbisymrelALT  48149  ssnn0ssfz  48343  ldepspr  48468  seposep  48920  upeu  49166  subthinc  49438  prsthinc  49459  iunord  49671  bnd2d  49676  setrecsss  49696