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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl3c  67  mpsyl  69  jc  162  jcnd  164  2thd  268  jca  521  syl2anc  596  aevlem0  2089  equvel  2485  elex22  3474  spcedv  3552  rspcdf  3563  rspcdva  3577  rspc3dv  3595  spsbcd  3753  opth  5452  euotd  5490  wereu2  5652  unielrel  6271  frpomin  6338  tz7.7  6383  funmo  6549  fvelimad  6946  iinpreima  7063  fompt  7112  fnfvima  7233  resfvresima  7235  fliftfun  7314  fliftval  7318  weniso  7358  riota5f  7399  riotass2  7401  fovcld  7541  ofmpteq  7702  ssorduni  7779  nlimsucg  7839  tfisi  7856  zfrep6OLD  7953  curry1  8102  curry2  8105  fnwelem  8130  funsssuppss  8189  frrlem4  8289  frrlem8  8293  frrlem10  8295  fprlem1  8300  fprlem2  8301  smogt  8357  tfrlem5  8369  omeulem1  8572  oeworde  8584  oelimcl  8591  oeeulem  8592  oeeui  8593  nnawordex  8628  oaabs2  8640  naddssim  8677  naddsuc2  8693  swoso  8734  qliftlem  8801  resixp  8943  domssl  9007  domssr  9008  xpdom3  9076  domunsncan  9078  omxpenlem  9079  domssex  9139  xpf1o  9140  mapdom3  9150  dif1en  9159  findcard  9161  f1dmvrnfibi  9311  fsuppss  9356  fiin  9395  marypha1lem  9406  marypha1  9407  fisupcl  9443  supgtoreq  9444  ordiso2  9490  ordtypelem2  9494  ordtypelem8  9500  wemapso2lem  9527  unxpwdom2  9563  cantnflt  9654  cantnfrescl  9658  oemapvali  9666  cantnflem1d  9670  wemapwe  9679  cnfcom  9682  ttrclss  9702  ttrclselem2  9708  frrlem15  9742  rankr1id  9847  tcrank  9869  cardmin2  10007  infxpenlem  10019  fseqen  10033  ween  10041  ac5num  10042  indcardi  10047  acni2  10052  fodomfi2  10066  infpwfien  10068  inffien  10069  iunfictbso  10120  acacni  10146  dfac12lem2  10150  djuinf  10194  infmap2  10222  ackbij1lem18  10241  ackbij1b  10243  fictb  10249  cfslb2n  10273  cofsmo  10274  cfsmolem  10275  coftr  10278  infpssrlem4  10311  domfin4  10316  fin2i2  10323  isfin2-2  10324  fincssdom  10328  ssfin3ds  10335  fin23lem20  10342  fin23lem30  10347  isf32lem3  10360  fin1a2lem12  10416  fin1a2lem13  10417  hsmexlem2  10432  axdc2lem  10453  imadomg  10540  imadomnum  10541  fimact  10542  fnct  10547  fnctOLD  10548  iundom2g  10551  iundomg  10552  iundom  10553  unirnfdomd  10579  konigthlem  10580  iunctb  10586  fpwwe2  10655  canthwelem  10662  pwfseqlem3  10672  pwfseqlem5  10675  winalim2  10708  wunelss  10720  r1wunlim  10749  wunex2  10750  tsksdom  10768  tskinf  10781  inttsk  10786  inar1  10787  tskcard  10793  tskurn  10801  gruina  10830  grur1a  10831  grur1  10832  addsrpr  11087  mulsrpr  11088  lemul12a  12100  lemulge11  12104  lediv12a  12135  fiminre2  12190  nngt0  12294  nn0ge2m1nn  12601  peano5uzi  12713  nn0ind-raph  12724  znnn0nn  12735  suprzub  12991  uzsupss  12992  rpge0  13059  fz0fzelfz0  13692  fz0fzdiffz0  13695  ige2m2fzo  13787  elfzodifsumelfzo  13790  elfzom1elp1fzo  13791  fzonfzoufzol  13830  flltdivnn0lt  13897  fldiv  13924  modaddmodup  14001  uzrdgsuci  14027  fzennn  14035  uzindi  14049  fsuppmapnn0fiubex  14059  expcl2lem  14140  leexp1a  14242  modexp  14305  faclbnd  14357  faclbnd6  14366  facavg  14368  hashginv  14401  hashf1rn  14419  hasheqf1od  14420  seqcoll  14532  hashge2el2dif  14548  wrdsymb0  14617  wrdlenge2n0  14620  ccatsymb  14651  swrdnd2  14728  swrdnd0  14730  pfxnd  14760  pfxccat1  14774  swrdpfx  14779  pfxpfx  14780  wrd2ind  14795  pfxccatin12  14805  pfxccat3  14806  swrdccat  14807  pfxccatpfx1  14808  pfxccatpfx2  14809  swrdccatin1d  14815  pfxccatin12d  14817  repswswrd  14858  cshwidxmod  14877  s2f1o  14990  f1oun2prg  14991  wwlktovfo  15034  relexpfld  15125  rtrclreclem3  15136  resqrex  15340  cau3lem  15445  reusq0  15555  rlimcld2  15668  climcn2  15683  isercoll  15758  climsup  15760  caurcvgr  15764  sumeq2ii  15783  summolem3  15803  zsum  15807  fsumadd  15829  fsumsplit1  15834  fsum2dlem  15859  fsum0diag2  15872  fsummulc2  15873  fsumabs  15891  fsumrelem  15897  fsumrlim  15901  fsumo1  15902  o1fsum  15903  fsumiun  15911  qshash  15917  prodeq2ii  16003  prodmolem3  16023  fprodmul  16050  fproddiv  16051  fprod2dlem  16070  fprodsplit1f  16080  sin02gt0  16283  efieq1re  16290  p1modz1  16352  dvdsleabs2  16405  4dvdseven  16466  sumeven  16480  sumodd  16481  divalglem9  16494  smupvallem  16576  algfx  16673  eucalgcvga  16679  lcmfunsnlem1  16730  lcmfunsnlem2lem1  16731  lcmflefac  16741  qredeq  16750  dvdszzq  16815  fermltl  16878  modprm0  16900  pythagtriplem4  16914  pythagtriplem6  16916  pythagtriplem7  16917  pythagtriplem12  16921  pythagtriplem13  16922  pythagtriplem14  16923  pythagtriplem16  16925  difsqpwdvds  16982  pcmpt  16987  prmreclem2  17012  4sqlem11  17050  vdwlem9  17084  vdwlem11  17086  vdwlem12  17087  0ram  17115  0ram2  17116  0ramcl  17118  ramcl  17124  prmolelcmf  17143  cshwsidrepsw  17188  cshwshashlem2  17191  prmlem1  17202  prmlem2  17215  strfvd  17295  strfv2d  17296  strssd  17300  firest  17520  prdsdsval3  17573  imasbas  17601  imasds  17602  imasaddfnlem  17617  imasaddvallem  17618  imasvscafn  17626  qusaddvallem  17640  qusaddflem  17641  qusaddval  17642  qusaddf  17643  qusmulval  17644  qusmulf  17645  catideu  17766  idinv  17881  brcici  17892  invfuc  18069  2initoinv  18102  initoeu1w  18104  initoeu2lem0  18105  2termoinv  18109  termoeu1w  18111  resspos  18520  resstos  18521  mod2ile  18585  lubss  18604  acsmapd  18645  chnso  18715  lidrididd  18767  qusmgm  18780  gsumval2a  18790  qusmnd  18891  mndind  18940  submefmnd  19007  mgm2nsgrplem4  19036  qusgrp2  19184  mulgnegnn  19210  pgrpsubgsymg  19539  fvcosymgeq  19559  gsmsymgreqlem1  19560  psgnunilem4  19627  pgpssslw  19744  sylow2alem2  19748  fislw  19755  efgsres  19868  rinvmod  19936  gsumval3lem2  20036  gsumzaddlem  20051  gsum2d  20102  nn0gsumfz  20114  telgsums  20123  dprddomcld  20133  ablfac2  20221  qusrng  20318  srgdilem  20334  o2timesd  20352  rglcom4d  20353  ringdilem  20391  qusring2  20478  orngsqr  21035  lssintcl  21151  lbsextlem3  21350  lbsextlem4  21351  prmidl2  21532  qsidomlem2  21547  zringlpirlem3  21680  psgnodpm  21804  psgndiflemB  21816  frlmup4  22017  lindff1  22036  lindfrn  22037  lmisfree  22058  evlseu  22302  mhpmulcl  22380  mptcoe1fsupp  22443  cply1coe0bi  22530  mpfpf1  22579  pf1mpf  22580  mat0dimscm  22694  mdetdiagid  22825  mdet1  22826  mdetunilem9  22845  slesolinv  22908  cramerimp  22914  cpmatmcllem  22946  mptcoe1matfsupp  23030  mp2pm2mp  23039  chpdmat  23069  cctop  23234  subbascn  23482  cnss2  23505  cmpcovf  23619  2ndcctbss  23684  2ndcomap  23687  2ndcsep  23688  comppfsc  23761  ptclsg  23844  dfac14  23847  txcnp  23849  ptcnplem  23850  uptx  23854  txtube  23869  tx2ndc  23880  xkococnlem  23888  elqtop  23926  qtoprest  23946  indishmph  24027  ptcmpfi  24042  kqhmph  24048  csdfil  24123  filssufilg  24140  ufilen  24159  rnelfm  24182  fmfnfmlem4  24186  alexsubALTlem4  24279  ptcmplem4  24284  cnextfvval  24294  cnextcn  24296  cnextfres  24298  tmdgsum2  24325  imasf1oxmet  24604  metss  24737  met2ndci  24751  prdsxmslem2  24758  metust  24787  cfilucfil  24788  metustbl  24795  psmetutop  24796  opnreen  25061  rectbntr0  25062  fsumcn  25101  rescncf  25128  xrhmeo  25177  cnllycmp  25187  lebnumlem1  25192  lebnumlem3  25194  cfilss  25501  iscmet3lem1  25522  iscmet3lem2  25523  ivthicc  25689  ovolsslem  25715  ovoliunlem2  25734  ovoliunnul  25738  ovolicc2lem4  25751  voliunlem3  25783  volsup  25787  uniiccdif  25809  uniioombllem2  25814  volivth  25838  mbfimaopnlem  25886  mbflimsup  25897  i1fd  25912  itg1addlem4  25930  itg2addlem  25989  itg2gt0  25991  limciun  26124  dvadd  26170  dvmul  26171  dvco  26177  dvrec  26185  dvcnv  26207  dvferm  26218  rollelem  26219  dvlip  26223  dvlip2  26225  c1liplem1  26226  c1lip2  26228  dvgt0lem1  26232  dvivthlem1  26238  lhop1lem  26243  dvcnvrelem1  26247  dvcnvrelem2  26248  dvcvx  26250  dvfsumle  26251  dvfsumabs  26253  dvfsumlem1  26256  dvfsumlem2  26257  dvfsumlem4  26259  dvfsumrlim2  26262  dvfsum2  26264  ftc1cn  26273  ftc2ditglem  26275  itgsubstlem  26278  itgpowd  26280  mdegaddle  26302  mdegmullem  26306  deg1sublt  26338  ply1divmo  26364  fta1g  26398  dgrub  26463  dgrnznn  26476  dgradd2  26497  dvply1  26517  plyrem  26538  rnplynfin  26542  aalioulem4  26574  aalioulem5  26575  aalioulem6  26576  aaliou2  26579  taylf  26600  ulmdv  26642  psercn2  26662  abelth  26680  abelth2  26681  reeff1olem  26685  efopn  26898  logreclem  27002  isosctrlem2  27059  xrlimcnp  27208  basellem4  27323  ppiwordi  27401  musum  27430  chpub  27459  gausslemma2dlem0c  27597  2sqlem6  27662  addsqnreup  27682  2sqreulem1  27685  2sqreunnlem1  27688  dchrisumlema  27727  dchrisumlem2  27729  dchrisumlem3  27730  pntlemp  27849  pntleml  27850  ostth3  27877  ltsres  27901  noextenddif  27907  nolesgn2ores  27911  nogesgn1ores  27913  nosep1o  27920  nosep2o  27921  nosepeq  27924  nolt02o  27934  noresle  27936  nosupno  27942  nosupbday  27944  nosupres  27946  nosupbnd1lem1  27947  nosupbnd1lem4  27950  nosupbnd1  27953  nosupbnd2lem1  27954  nosupbnd2  27955  noinfno  27957  noinfbday  27959  noinfres  27961  noinfbnd1lem5  27966  noinfbnd1  27968  noinfbnd2lem1  27969  ltlesd  28012  madebday  28168  leadds1  28257  precsexlem10  28484  noseqrdg0  28575  noseqrdgsuc  28576  elnnzs  28669  bdaypw2n0bndlem  28731  iscgrglt  28859  colline  29000  axlowdimlem16  29417  axlowdimlem17  29418  axcontlem3  29426  axcontlem10  29433  uhgr2edg  29671  nbupgruvtxres  29870  cusgrres  29911  cusgrfilem2  29919  vdumgr0  29943  frusgrnn0  30034  wlkp1lem8  30141  pthdivtx  30194  upgrwlkdvde  30205  spthonepeq  30220  usgr2pthlem  30231  cyclnumvtx  30270  lfgrn1cycl  30276  wwlknbp1  30315  wwlknllvtx  30317  wlkiswwlks2lem3  30342  umgr2adedgspth  30419  clwlkclwwlklem3  30474  clwwisshclwwslemlem  30486  clwwisshclwws  30488  clwwlkel  30519  wwlksubclwwlk  30531  eleclclwwlknlem1  30533  eleclclwwlknlem2  30534  erclwwlknref  30542  clwwlknonccat  30569  clwwlknonex2lem2  30581  3wlkdlem4  30645  vdn0conngrumgrv2  30679  eucrctshift  30726  frgrnbnb  30776  frgrncvvdeqlem2  30783  frgrncvvdeqlem3  30784  fusgreghash2wspv  30818  numclwwlk2lem1  30859  numclwlk2lem2f  30860  numclwwlk5  30871  numclwwlk7  30874  frgrreggt1  30876  minvecolem4b  31362  minvecolem4  31364  bcsiALT  31663  ococin  31892  spanpr  32064  pjorthi  32153  nmbdoplbi  32508  nmcoplbi  32512  nmbdfnlbi  32533  nmcfnlbi  32536  nmopcoi  32579  branmfn  32589  hstnmoc  32707  mdsl0  32794  atomli  32866  atcvat4i  32881  atabsi  32885  foresf1o  32982  rabfodom  32983  abrexdomjm  32985  elpreq  33006  ifeqeqx  33020  disjiunel  33072  ac6mapd  33099  aciunf1lem  33138  ffsrn  33202  xlt2addrd  33233  supxrnemnf  33242  ssnnssfz  33261  gsummptres2  33496  gsumfs2d  33504  archirngz  33632  isarchiofld  33642  unitprodclb  33825  elrspunidl  33859  drngidlhash  33864  ssmxidl  33880  1arithidom  33950  1arithufdlem4  33960  constrmon  34257  locfinreflem  34353  cmpcref  34363  fmcncfil  34444  xrge0iifiso  34448  elzdif0  34493  qqhval2lem  34494  esumcst  34576  esumrnmpt2  34581  esumpinfval  34586  esumpinfsum  34590  sigaclci  34645  insiga  34651  ldgenpisys  34680  measres  34736  measdivcstALTV  34739  dya2iocnrect  34795  dya2iocnei  34796  omssubadd  34814  carsggect  34832  carsgclctunlem2  34833  sitgclg  34856  eulerpartlemsv2  34872  eulerpartlemv  34878  eulerpartlemf  34884  eulerpartlemgh  34892  eulerpartlemgs2  34894  ballotlemfp1  35006  ballotlemfrcn0  35044  ftc2re  35109  fdvposlt  35110  fdvposle  35112  bnj1379  35342  bnj580  35425  bnj944  35450  bnj999  35470  bnj1204  35524  bnj1398  35546  onvfowev  35716  cusgredgex  35723  pthacycspth  35739  derangenlem  35753  subfacp1lem3  35764  resconn  35828  cvmliftlem3  35869  satfv0fvfmla0  35995  satfv1fvfmla1  36005  mrsub0  36098  cgrextend  36591  segconeq  36593  trisegint  36611  fwddifnp1  36748  onelssd  36784  nmuladdss  36796  ivthALT  36957  fnessref  36979  refssfne  36980  neibastop1  36981  filnetlem4  37003  ontgval  37053  weiunlem  37085  weiunse  37090  dfttc4  37152  mh-inf3f1  37163  unblimceq0lem  37206  unbdqndv2lem2  37210  unbdqndv2  37211  bj-babygodel  37307  bj-alrimd  37329  bj-exlimd  37341  bj-spim  37359  bj-spime  37360  bj-nnf-spime  37511  bj-spcimdv  37641  bj-spcimdvv  37642  bj-finsumval0  38040  bj-fvimacnv0  38041  dfgcd3  38079  relowlssretop  38120  relowlpssretop  38121  onsucuni3  38124  finxpreclem4  38151  poimirlem18  38390  poimirlem21  38393  poimirlem25  38397  ftc1cnnclem  38443  ftc1cnnc  38444  ftc2nc  38454  dvasin  38456  dvacos  38457  abrexdom  38483  indexdom  38487  mettrifi  38510  equivtotbnd  38531  totbndbnd  38542  prdstotbnd  38547  heibor1lem  38562  bfplem1  38575  bfplem2  38576  opidonOLD  38605  rngodm1dm2  38685  zerdivemp1x  38700  equid1  39775  omllaw5N  40123  cmtcomlemN  40124  cmtbr3N  40130  omlfh3N  40135  atlen0  40186  exatleN  40280  hlrelat3  40288  cvrexchlem  40295  atlelt  40314  cvrat4  40319  4atlem11b  40484  4atlem12b  40487  lneq2at  40654  cdlema1N  40667  cdlemblem  40669  paddss12  40695  paddasslem2  40697  paddasslem4  40699  paddasslem6  40701  paddasslem12  40707  paddunN  40803  poml4N  40829  poml5N  40830  osumcllem6N  40837  pexmidlem6N  40851  pl42lem2N  40856  ltrnu  40997  ltrneq2  41024  trlval2  41039  cdlemd6  41079  cdleme25b  41230  cdleme29b  41251  cdlemefr29exN  41278  ltrniotacnvval  41458  cdlemk28-3  41784  dochexmidlem7  42342  muldvds2d  42867  frlmsnic  43425  nna4b4nsq  43509  mzpsubmpt  43591  mzpsubst  43596  eqrabdioph  43625  rabdiophlem2  43646  elpell14qr2  43706  elpell1qr2  43716  pellfundre  43725  pellfundge  43726  pellfundglb  43729  pellfund14gap  43731  congabseq  43818  jm2.22  43839  jm2.23  43840  jm2.26lem3  43845  wepwsolem  43886  aomclem2  43899  aomclem4  43901  pwfi2f1o  43940  onexlimgt  44087  oaltublim  44134  oege1  44150  cantnfub2  44166  cantnfresb  44168  cantnf2  44169  oacl2g  44174  tfsconcatb0  44188  tfsconcatrev  44192  oaun3lem1  44218  oaun3lem2  44219  nadd2rabtr  44228  nadd1suc  44236  naddwordnexlem0  44240  naddwordnexlem3  44243  oawordex3  44244  naddwordnexlem4  44245  oaltom  44248  omltoe  44250  ss2iundf  44502  dssmapf1od  44864  neik0pk1imk0  44890  gneispace  44977  grur1cld  45073  cpcolld  45085  mnuop23d  45093  mnuprdlem1  45099  mnuprdlem2  45100  mnurndlem1  45108  grumnudlem  45112  radcnvrat  45141  sbiota1  45261  ordelordALT  45363  2pm13.193  45378  ee11an  45516  modelaxreplem2  45805  refsumcn  45867  rfcnnnub  45873  disjxp1  45906  xrnmnfpnf  45920  ssinc  45922  nssd  45940  disjf1o  46026  choicefi  46034  axccdom  46055  dmrelrnrel  46059  monoords  46133  fperiodmullem  46139  xadd0ge  46155  xrssre  46181  xrlexaddrp  46185  xrred  46197  infxr  46199  xrnpnfmnf  46305  monoordxrv  46312  monoord2xrv  46314  cvgcaule  46322  fsumiunss  46408  fmul01  46413  fmuldfeqlem1  46415  fmuldfeq  46416  fmul01lt1lem1  46417  fmul01lt1lem2  46418  cncfmptss  46420  climinf  46439  climsuselem1  46440  climsuse  46441  limcperiod  46461  limcrecl  46462  sumnnodd  46463  limcleqr  46475  0ellimcdiv  46480  climleltrp  46507  limsuppnfdlem  46532  limsupresxr  46597  liminfresxr  46598  liminfvalxr  46614  cnrefiisplem  46660  xlimmnfvlem1  46663  xlimpnfvlem1  46667  cncfperiod  46710  icccncfext  46718  cncfiooicclem1  46724  dvbdfbdioolem1  46759  dvnmptdivc  46769  dvdsn1add  46770  dvnmptconst  46772  dvnmul  46774  dvmptfprodlem  46775  dvmptfprod  46776  dvnprodlem2  46778  iblspltprt  46804  itgsubsticclem  46806  itgspltprt  46810  itgsbtaddcnst  46813  stoweidlem3  46834  stoweidlem16  46847  stoweidlem17  46848  stoweidlem19  46850  stoweidlem20  46851  stoweidlem23  46854  stoweidlem25  46856  stoweidlem27  46858  stoweidlem31  46862  stoweidlem34  46865  stoweidlem42  46873  stoweidlem48  46879  stoweidlem51  46882  stoweidlem52  46883  stoweidlem59  46890  wallispilem1  46896  wallispilem3  46898  stirlinglem13  46917  fourierdlem16  46954  fourierdlem20  46958  fourierdlem21  46959  fourierdlem38  46976  fourierdlem42  46980  fourierdlem46  46983  fourierdlem48  46985  fourierdlem49  46986  fourierdlem50  46987  fourierdlem54  46991  fourierdlem68  47005  fourierdlem72  47009  fourierdlem73  47010  fourierdlem76  47013  fourierdlem79  47016  fourierdlem81  47018  fourierdlem86  47023  fourierdlem89  47026  fourierdlem90  47027  fourierdlem91  47028  fourierdlem92  47029  fourierdlem97  47034  fourierdlem101  47038  fourierdlem103  47040  fourierdlem104  47041  fourierdlem111  47048  etransclem24  47089  etransclem25  47090  etransclem28  47093  etransclem41  47106  etransclem44  47109  etransclem48  47113  salexct  47165  dfsalgen2  47172  sge0f1o  47213  sge0rnbnd  47224  sge0split  47240  sge0iunmptlemre  47246  sge0fodjrnlem  47247  sge0iunmpt  47249  nnfoctbdjlem  47286  iundjiunlem  47290  meadjiunlem  47296  ismeannd  47298  meaiuninclem  47311  carageniuncllem1  47352  caratheodorylem1  47357  hoidmvlelem4  47429  hoiqssbllem2  47454  salpreimagelt  47538  salpreimalegt  47540  pimdecfgtioc  47546  smfaddlem2  47595  smflimlem6  47607  nsssmfmbflem  47609  smfpimcclem  47638  quantgodelALT  47706  ormkglobd  47708  or2expropbilem1  47923  funressndmfvrn  47935  f1cof1b  47968  2leaddle2  48189  smonoord  48268  muldvdsfacgt  48277  uniimaprimaeqfv  48285  fundcmpsurbijinjpreimafv  48310  fundcmpsurinjALT  48315  iccpartf  48334  ich2exprop  48374  ichnreuop  48375  ichreuopeq  48376  sprbisymrel  48402  fmtnodvds  48450  proththdlem  48519  gbowgt5  48681  gboge9  48683  gbege6  48684  stgoldbwt  48695  sbgoldbalt  48700  bgoldbnnsum3prm  48723  grimgrtri  48868  grlimgrtri  48922  grlicsym  48932  clnbgr3stgrgrlim  48938  clnbgr3stgrgrlic  48939  gpg5gricstgr3  49009  uspgrbisymrelALT  49074  ssnn0ssfz  49282  ldepspr  49406  seposep  49855  upeu  50100  subthinc  50372  prsthinc  50393  iunord  50605  bnd2d  50610  setrecsss  50630