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  267  jca  519  syl2anc  593  aevlem0  2077  equvel  2488  elex22  3479  spcedv  3558  rspcdf  3569  rspcdva  3583  rspc3dv  3601  spsbcd  3759  opth  5445  euotd  5483  wereu2  5645  unielrel  6262  frpomin  6328  tz7.7  6373  funmo  6538  fvelimad  6935  iinpreima  7051  fompt  7100  fnfvima  7218  resfvresima  7220  fliftfun  7297  fliftval  7301  weniso  7339  riota5f  7382  riotass2  7384  fovcld  7524  ofmpteq  7684  ssorduni  7763  nlimsucg  7823  tfisi  7840  zfrep6OLD  7937  curry1  8084  curry2  8087  fnwelem  8112  funsssuppss  8171  frrlem4  8271  frrlem8  8275  frrlem10  8277  fprlem1  8282  fprlem2  8283  smogt  8339  tfrlem5  8351  omeulem1  8552  oeworde  8564  oelimcl  8571  oeeulem  8572  oeeui  8573  nnawordex  8608  oaabs2  8620  naddssim  8657  naddsuc2  8673  swoso  8714  qliftlem  8781  resixp  8916  domssl  8980  domssr  8981  xpdom3  9048  domunsncan  9050  omxpenlem  9051  domssex  9111  xpf1o  9112  mapdom3  9122  dif1en  9131  findcard  9133  f1dmvrnfibi  9285  fsuppss  9330  fiin  9369  marypha1lem  9380  marypha1  9381  fisupcl  9417  supgtoreq  9418  ordiso2  9464  ordtypelem2  9468  ordtypelem8  9474  wemapso2lem  9501  unxpwdom2  9537  cantnflt  9628  cantnfrescl  9632  oemapvali  9640  cantnflem1d  9644  wemapwe  9653  cnfcom  9656  ttrclss  9676  ttrclselem2  9682  frrlem15  9716  rankr1id  9821  tcrank  9843  cardmin2  9958  infxpenlem  9970  fseqen  9984  ween  9992  ac5num  9993  indcardi  9998  acni2  10003  fodomfi2  10017  infpwfien  10019  inffien  10020  iunfictbso  10071  acacni  10098  dfac12lem2  10102  djuinf  10146  infmap2  10174  ackbij1lem18  10193  ackbij1b  10195  fictb  10201  cfslb2n  10226  cofsmo  10227  cfsmolem  10228  coftr  10231  infpssrlem4  10264  domfin4  10269  fin2i2  10276  isfin2-2  10277  fincssdom  10281  ssfin3ds  10288  fin23lem20  10295  fin23lem30  10300  isf32lem3  10313  fin1a2lem12  10369  fin1a2lem13  10370  hsmexlem2  10385  axdc2lem  10406  imadomg  10492  fnct  10495  iundom2g  10498  iundomg  10499  iundom  10500  unirnfdomd  10526  konigthlem  10527  iunctb  10533  fpwwe2  10602  canthwelem  10609  pwfseqlem3  10619  pwfseqlem5  10622  winalim2  10655  wunelss  10667  r1wunlim  10696  wunex2  10697  tsksdom  10715  tskinf  10728  inttsk  10733  inar1  10734  tskcard  10740  tskurn  10748  gruina  10777  grur1a  10778  grur1  10779  addsrpr  11034  mulsrpr  11035  lemul12a  12050  lemulge11  12055  lediv12a  12086  fiminre2  12141  nngt0  12245  nn0ge2m1nn  12552  peano5uzi  12663  nn0ind-raph  12674  znnn0nn  12685  suprzub  12941  uzsupss  12942  rpge0  13008  fz0fzelfz0  13640  fz0fzdiffz0  13643  ige2m2fzo  13735  elfzodifsumelfzo  13738  elfzom1elp1fzo  13739  fzonfzoufzol  13778  flltdivnn0lt  13844  fldiv  13871  modaddmodup  13948  uzrdgsuci  13974  fzennn  13982  uzindi  13996  fsuppmapnn0fiubex  14006  expcl2lem  14087  leexp1a  14189  modexp  14252  faclbnd  14304  faclbnd6  14313  facavg  14315  hashginv  14348  hashf1rn  14366  hasheqf1od  14367  seqcoll  14478  hashge2el2dif  14494  wrdsymb0  14563  wrdlenge2n0  14566  ccatsymb  14597  swrdnd2  14670  swrdnd0  14672  pfxnd  14702  pfxccat1  14716  swrdpfx  14721  pfxpfx  14722  wrd2ind  14737  pfxccatin12  14747  pfxccat3  14748  swrdccat  14749  pfxccatpfx1  14750  pfxccatpfx2  14751  swrdccatin1d  14757  pfxccatin12d  14759  repswswrd  14798  cshwidxmod  14817  s2f1o  14930  f1oun2prg  14931  wwlktovfo  14972  relexpfld  15063  rtrclreclem3  15074  resqrex  15278  cau3lem  15383  reusq0  15493  rlimcld2  15606  climcn2  15621  isercoll  15696  climsup  15698  caurcvgr  15702  sumeq2ii  15721  summolem3  15742  zsum  15746  fsumadd  15768  fsumsplit1  15773  fsum2dlem  15798  fsum0diag2  15811  fsummulc2  15812  fsumabs  15830  fsumrelem  15836  fsumrlim  15840  fsumo1  15841  o1fsum  15842  fsumiun  15850  qshash  15856  prodeq2ii  15942  prodmolem3  15964  fprodmul  15991  fproddiv  15992  fprod2dlem  16011  fprodsplit1f  16021  sin02gt0  16225  efieq1re  16232  p1modz1  16294  dvdsleabs2  16347  4dvdseven  16408  sumeven  16422  sumodd  16423  divalglem9  16436  smupvallem  16518  algfx  16615  eucalgcvga  16621  lcmfunsnlem1  16672  lcmfunsnlem2lem1  16673  lcmflefac  16683  qredeq  16692  dvdszzq  16757  fermltl  16820  modprm0  16842  pythagtriplem4  16856  pythagtriplem6  16858  pythagtriplem7  16859  pythagtriplem12  16863  pythagtriplem13  16864  pythagtriplem14  16865  pythagtriplem16  16867  difsqpwdvds  16924  pcmpt  16929  prmreclem2  16954  4sqlem11  16992  vdwlem9  17026  vdwlem11  17028  vdwlem12  17029  0ram  17057  0ram2  17058  0ramcl  17060  ramcl  17066  prmolelcmf  17085  cshwsidrepsw  17130  cshwshashlem2  17133  prmlem1  17144  prmlem2  17157  strfvd  17237  strfv2d  17238  strssd  17242  firest  17462  prdsdsval3  17515  imasbas  17543  imasds  17544  imasaddfnlem  17559  imasaddvallem  17560  imasvscafn  17568  qusaddvallem  17582  qusaddflem  17583  qusaddval  17584  qusaddf  17585  qusmulval  17586  qusmulf  17587  catideu  17708  idinv  17823  brcici  17834  invfuc  18011  2initoinv  18044  initoeu1w  18046  initoeu2lem0  18047  2termoinv  18051  termoeu1w  18053  resspos  18462  resstos  18463  mod2ile  18527  lubss  18546  acsmapd  18587  chnso  18657  lidrididd  18705  gsumval2a  18720  mndind  18863  submefmnd  18930  mgm2nsgrplem4  18959  qusgrp2  19101  mulgnegnn  19127  pgrpsubgsymg  19450  fvcosymgeq  19470  gsmsymgreqlem1  19471  psgnunilem4  19538  pgpssslw  19655  sylow2alem2  19659  fislw  19666  efgsres  19779  rinvmod  19847  gsumval3lem2  19947  gsumzaddlem  19962  gsum2d  20013  nn0gsumfz  20025  telgsums  20034  dprddomcld  20044  ablfac2  20132  qusrng  20227  srgdilem  20243  o2timesd  20261  rglcom4d  20262  ringdilem  20300  qusring2  20384  orngsqr  20916  lssintcl  21032  lbsextlem3  21231  lbsextlem4  21232  zringlpirlem3  21517  psgnodpm  21641  psgndiflemB  21653  frlmup4  21854  lindff1  21873  lindfrn  21874  lmisfree  21895  evlseu  22137  mhpmulcl  22215  mptcoe1fsupp  22278  cply1coe0bi  22366  mpfpf1  22415  pf1mpf  22416  mat0dimscm  22530  mdetdiagid  22661  mdet1  22662  mdetunilem9  22681  slesolinv  22741  cramerimp  22747  cpmatmcllem  22779  mptcoe1matfsupp  22863  mp2pm2mp  22872  chpdmat  22902  cctop  23067  subbascn  23315  cnss2  23338  cmpcovf  23452  2ndcctbss  23516  2ndcomap  23519  2ndcsep  23520  comppfsc  23593  ptclsg  23676  dfac14  23679  txcnp  23681  ptcnplem  23682  uptx  23686  txtube  23701  tx2ndc  23712  xkococnlem  23720  elqtop  23758  qtoprest  23778  indishmph  23859  ptcmpfi  23874  kqhmph  23880  csdfil  23955  filssufilg  23972  ufilen  23991  rnelfm  24014  fmfnfmlem4  24018  alexsubALTlem4  24111  ptcmplem4  24116  cnextfvval  24126  cnextcn  24128  cnextfres  24130  tmdgsum2  24157  imasf1oxmet  24436  metss  24569  met2ndci  24583  prdsxmslem2  24590  metust  24619  cfilucfil  24620  metustbl  24627  psmetutop  24628  opnreen  24893  rectbntr0  24894  fsumcn  24933  rescncf  24960  xrhmeo  25009  cnllycmp  25019  lebnumlem1  25024  lebnumlem3  25026  cfilss  25333  iscmet3lem1  25354  iscmet3lem2  25355  ivthicc  25521  ovolsslem  25547  ovoliunlem2  25566  ovoliunnul  25570  ovolicc2lem4  25583  voliunlem3  25615  volsup  25619  uniiccdif  25641  uniioombllem2  25646  volivth  25670  mbfimaopnlem  25718  mbflimsup  25729  i1fd  25744  itg1addlem4  25762  itg2addlem  25821  itg2gt0  25823  limciun  25957  dvadd  26003  dvmul  26004  dvco  26010  dvrec  26018  dvcnv  26040  dvferm  26051  rollelem  26052  dvlip  26056  dvlip2  26058  c1liplem1  26059  c1lip2  26061  dvgt0lem1  26065  dvivthlem1  26071  lhop1lem  26076  dvcnvrelem1  26080  dvcnvrelem2  26081  dvcvx  26083  dvfsumle  26084  dvfsumabs  26086  dvfsumlem1  26089  dvfsumlem2  26090  dvfsumlem4  26092  dvfsumrlim2  26095  dvfsum2  26097  ftc1cn  26106  ftc2ditglem  26108  itgsubstlem  26111  itgpowd  26113  mdegaddle  26135  mdegmullem  26139  deg1sublt  26171  ply1divmo  26197  fta1g  26231  dgrub  26295  dgrnznn  26308  dgradd2  26329  dvply1  26349  plyrem  26370  aalioulem4  26400  aalioulem5  26401  aalioulem6  26402  aaliou2  26405  taylf  26425  ulmdv  26467  psercn2  26487  abelth  26505  abelth2  26506  reeff1olem  26510  efopn  26724  logreclem  26828  isosctrlem2  26885  xrlimcnp  27034  basellem4  27149  ppiwordi  27227  musum  27256  chpub  27285  gausslemma2dlem0c  27423  2sqlem6  27488  addsqnreup  27508  2sqreulem1  27511  2sqreunnlem1  27514  dchrisumlema  27553  dchrisumlem2  27555  dchrisumlem3  27556  pntlemp  27675  pntleml  27676  ostth3  27703  ltsres  27727  noextenddif  27733  nolesgn2ores  27737  nogesgn1ores  27739  nosep1o  27746  nosep2o  27747  nosepeq  27750  nolt02o  27760  noresle  27762  nosupno  27768  nosupbday  27770  nosupres  27772  nosupbnd1lem1  27773  nosupbnd1lem4  27776  nosupbnd1  27779  nosupbnd2lem1  27780  nosupbnd2  27781  noinfno  27783  noinfbday  27785  noinfres  27787  noinfbnd1lem5  27792  noinfbnd1  27794  noinfbnd2lem1  27795  ltlesd  27838  madebday  27994  leadds1  28083  precsexlem10  28310  noseqrdg0  28401  noseqrdgsuc  28402  elnnzs  28495  bdaypw2n0bndlem  28557  iscgrglt  28684  colline  28820  axlowdimlem16  29159  axlowdimlem17  29160  axcontlem3  29168  axcontlem10  29175  uhgr2edg  29410  nbupgruvtxres  29609  cusgrres  29650  cusgrfilem2  29658  vdumgr0  29682  frusgrnn0  29773  wlkp1lem8  29880  pthdivtx  29928  upgrwlkdvde  29938  spthonepeq  29953  usgr2pthlem  29964  cyclnumvtx  30001  lfgrn1cycl  30006  wwlknbp1  30045  wwlknllvtx  30047  wlkiswwlks2lem3  30072  umgr2adedgspth  30149  clwlkclwwlklem3  30204  clwwisshclwwslemlem  30216  clwwisshclwws  30218  clwwlkel  30249  wwlksubclwwlk  30261  eleclclwwlknlem1  30263  eleclclwwlknlem2  30264  erclwwlknref  30272  clwwlknonccat  30299  clwwlknonex2lem2  30311  3wlkdlem4  30365  vdn0conngrumgrv2  30399  eucrctshift  30446  frgrnbnb  30496  frgrncvvdeqlem2  30503  frgrncvvdeqlem3  30504  fusgreghash2wspv  30538  numclwwlk2lem1  30579  numclwlk2lem2f  30580  numclwwlk5  30591  numclwwlk7  30594  frgrreggt1  30596  minvecolem4b  31082  minvecolem4  31084  bcsiALT  31383  ococin  31612  spanpr  31784  pjorthi  31873  nmbdoplbi  32228  nmcoplbi  32232  nmbdfnlbi  32253  nmcfnlbi  32256  nmopcoi  32299  branmfn  32309  hstnmoc  32427  mdsl0  32514  atomli  32586  atcvat4i  32601  atabsi  32605  foresf1o  32704  rabfodom  32705  abrexdomjm  32707  elpreq  32728  ifeqeqx  32742  disjiunel  32797  ac6mapd  32826  aciunf1lem  32865  ffsrn  32931  xlt2addrd  32962  supxrnemnf  32971  ssnnssfz  32990  gsummptres2  33234  gsumfs2d  33242  archirngz  33370  isarchiofld  33380  unitprodclb  33576  elrspunidl  33615  drngidlhash  33621  prmidl2  33628  qsidomlem2  33641  ssmxidl  33663  1arithidom  33734  1arithufdlem4  33744  constrmon  34042  locfinreflem  34138  cmpcref  34148  fmcncfil  34229  xrge0iifiso  34233  elzdif0  34278  qqhval2lem  34279  esumcst  34361  esumrnmpt2  34366  esumpinfval  34371  esumpinfsum  34375  sigaclci  34430  insiga  34435  ldgenpisys  34464  measres  34520  measdivcstALTV  34523  dya2iocnrect  34579  dya2iocnei  34580  omssubadd  34598  carsggect  34616  carsgclctunlem2  34617  sitgclg  34640  eulerpartlemsv2  34656  eulerpartlemv  34662  eulerpartlemf  34668  eulerpartlemgh  34676  eulerpartlemgs2  34678  ballotlemfp1  34790  ballotlemfrcn0  34828  ftc2re  34893  fdvposlt  34894  fdvposle  34896  bnj1379  35126  bnj580  35209  bnj944  35234  bnj999  35254  bnj1204  35308  bnj1398  35330  onvfowev  35460  cusgredgex  35473  pthacycspth  35508  derangenlem  35522  subfacp1lem3  35533  resconn  35597  cvmliftlem3  35638  satfv0fvfmla0  35764  satfv1fvfmla1  35774  mrsub0  35867  cgrextend  36359  segconeq  36361  trisegint  36379  fwddifnp1  36516  ivthALT  36696  fnessref  36718  refssfne  36719  neibastop1  36720  filnetlem4  36742  ontgval  36792  weiunlem  36824  weiunse  36829  dfttc4  36891  unblimceq0lem  36945  unbdqndv2lem2  36949  unbdqndv2  36950  bj-babygodel  37047  bj-alrimd  37069  bj-exlimd  37081  bj-spim  37099  bj-spime  37100  bj-nnf-spime  37251  bj-spcimdv  37381  bj-spcimdvv  37382  bj-finsumval0  37778  bj-fvimacnv0  37779  dfgcd3  37817  relowlssretop  37858  relowlpssretop  37859  onsucuni3  37862  finxpreclem4  37889  poimirlem18  38138  poimirlem21  38141  poimirlem25  38145  ftc1cnnclem  38191  ftc1cnnc  38192  ftc2nc  38202  dvasin  38204  dvacos  38205  abrexdom  38230  indexdom  38234  mettrifi  38257  equivtotbnd  38278  totbndbnd  38289  prdstotbnd  38294  heibor1lem  38309  bfplem1  38322  bfplem2  38323  opidonOLD  38352  rngodm1dm2  38432  zerdivemp1x  38447  equid1  39524  omllaw5N  39872  cmtcomlemN  39873  cmtbr3N  39879  omlfh3N  39884  atlen0  39935  exatleN  40029  hlrelat3  40037  cvrexchlem  40044  atlelt  40063  cvrat4  40068  4atlem11b  40233  4atlem12b  40236  lneq2at  40403  cdlema1N  40416  cdlemblem  40418  paddss12  40444  paddasslem2  40446  paddasslem4  40448  paddasslem6  40450  paddasslem12  40456  paddunN  40552  poml4N  40578  poml5N  40579  osumcllem6N  40586  pexmidlem6N  40600  pl42lem2N  40605  ltrnu  40746  ltrneq2  40773  trlval2  40788  cdlemd6  40828  cdleme25b  40979  cdleme29b  41000  cdlemefr29exN  41027  ltrniotacnvval  41207  cdlemk28-3  41533  dochexmidlem7  42091  muldvds2d  42616  frlmsnic  43159  nna4b4nsq  43243  mzpsubmpt  43325  mzpsubst  43330  eqrabdioph  43359  rabdiophlem2  43380  elpell14qr2  43440  elpell1qr2  43450  pellfundre  43459  pellfundge  43460  pellfundglb  43463  pellfund14gap  43465  congabseq  43552  jm2.22  43573  jm2.23  43574  jm2.26lem3  43579  wepwsolem  43620  dnwech  43626  aomclem2  43633  aomclem4  43635  pwfi2f1o  43674  onexlimgt  43821  oaltublim  43868  oege1  43884  cantnfub2  43900  cantnfresb  43902  cantnf2  43903  oacl2g  43908  tfsconcatb0  43922  tfsconcatrev  43926  oaun3lem1  43952  oaun3lem2  43953  nadd2rabtr  43962  nadd1suc  43970  naddwordnexlem0  43974  naddwordnexlem3  43977  oawordex3  43978  naddwordnexlem4  43979  oaltom  43982  omltoe  43984  ss2iundf  44236  dssmapf1od  44598  neik0pk1imk0  44624  gneispace  44711  grur1cld  44809  cpcolld  44835  mnuop23d  44843  mnuprdlem1  44849  mnuprdlem2  44850  mnurndlem1  44858  grumnudlem  44862  radcnvrat  44891  sbiota1  45011  ordelordALT  45114  2pm13.193  45129  ee11an  45267  modelaxreplem2  45556  refsumcn  45611  rfcnnnub  45617  disjxp1  45650  xrnmnfpnf  45664  ssinc  45666  nssd  45684  disjf1o  45770  disjinfi  45771  choicefi  45778  axccdom  45799  dmrelrnrel  45803  monoords  45877  fperiodmullem  45883  xadd0ge  45899  xrssre  45925  xrlexaddrp  45929  xrred  45941  infxr  45943  xrnpnfmnf  46049  monoordxrv  46056  monoord2xrv  46058  cvgcaule  46066  fsumiunss  46152  fmul01  46157  fmuldfeqlem1  46159  fmuldfeq  46160  fmul01lt1lem1  46161  fmul01lt1lem2  46162  cncfmptss  46164  climinf  46183  climsuselem1  46184  climsuse  46185  limcperiod  46205  limcrecl  46206  sumnnodd  46207  limcleqr  46219  0ellimcdiv  46224  climleltrp  46251  limsuppnfdlem  46276  limsupresxr  46341  liminfresxr  46342  liminfvalxr  46358  cnrefiisplem  46404  xlimmnfvlem1  46407  xlimpnfvlem1  46411  cncfperiod  46454  icccncfext  46462  cncfiooicclem1  46468  dvbdfbdioolem1  46503  dvnmptdivc  46513  dvdsn1add  46514  dvnmptconst  46516  dvnmul  46518  dvmptfprodlem  46519  dvmptfprod  46520  dvnprodlem2  46522  iblspltprt  46548  itgsubsticclem  46550  itgspltprt  46554  itgsbtaddcnst  46557  stoweidlem3  46578  stoweidlem16  46591  stoweidlem17  46592  stoweidlem19  46594  stoweidlem20  46595  stoweidlem23  46598  stoweidlem25  46600  stoweidlem27  46602  stoweidlem31  46606  stoweidlem34  46609  stoweidlem42  46617  stoweidlem48  46623  stoweidlem51  46626  stoweidlem52  46627  stoweidlem59  46634  wallispilem1  46640  wallispilem3  46642  stirlinglem13  46661  fourierdlem16  46698  fourierdlem20  46702  fourierdlem21  46703  fourierdlem38  46720  fourierdlem42  46724  fourierdlem46  46727  fourierdlem48  46729  fourierdlem49  46730  fourierdlem50  46731  fourierdlem54  46735  fourierdlem68  46749  fourierdlem72  46753  fourierdlem73  46754  fourierdlem76  46757  fourierdlem79  46760  fourierdlem81  46762  fourierdlem86  46767  fourierdlem89  46770  fourierdlem90  46771  fourierdlem91  46772  fourierdlem92  46773  fourierdlem97  46778  fourierdlem101  46782  fourierdlem103  46784  fourierdlem104  46785  fourierdlem111  46792  etransclem24  46833  etransclem25  46834  etransclem28  46837  etransclem41  46850  etransclem44  46853  etransclem48  46857  salexct  46909  dfsalgen2  46916  sge0f1o  46957  sge0rnbnd  46968  sge0split  46984  sge0iunmptlemre  46990  sge0fodjrnlem  46991  sge0iunmpt  46993  nnfoctbdjlem  47030  iundjiunlem  47034  meadjiunlem  47040  ismeannd  47042  meaiuninclem  47055  omeiunle  47092  carageniuncllem1  47096  caratheodorylem1  47101  hoidmvlelem4  47173  hoiqssbllem2  47198  salpreimagelt  47282  salpreimalegt  47284  pimdecfgtioc  47290  smfaddlem2  47339  smflimlem6  47351  nsssmfmbflem  47353  smfpimcclem  47382  quantgodelALT  47450  ormkglobd  47452  or2expropbilem1  47627  funressndmfvrn  47639  f1cof1b  47672  2leaddle2  47893  smonoord  47972  muldvdsfacgt  47981  uniimaprimaeqfv  47989  fundcmpsurbijinjpreimafv  48014  fundcmpsurinjALT  48019  iccpartf  48038  ich2exprop  48078  ichnreuop  48079  ichreuopeq  48080  sprbisymrel  48106  fmtnodvds  48154  proththdlem  48223  gbowgt5  48385  gboge9  48387  gbege6  48388  stgoldbwt  48399  sbgoldbalt  48404  bgoldbnnsum3prm  48427  grimgrtri  48572  grlimgrtri  48626  grlicsym  48636  clnbgr3stgrgrlim  48642  clnbgr3stgrgrlic  48643  gpg5gricstgr3  48713  uspgrbisymrelALT  48778  ssnn0ssfz  48972  ldepspr  49096  seposep  49548  upeu  49793  subthinc  50065  prsthinc  50086  iunord  50298  bnd2d  50303  setrecsss  50323