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  264  jca  510  syl2anc  582  aevlem0  2049  equvel  2449  elex2OLD  3484  elex22  3485  spcedv  3582  rspcdf  3593  rspcdva  3607  rspc3dv  3624  spsbcd  3787  opth  5478  euotd  5515  wereu2  5675  unielrel  6280  frpomin  6348  tz7.7  6397  funmo  6569  funmoOLD  6570  fvelimad  6965  iinpreima  7077  fompt  7127  fnfvima  7245  resfvresima  7247  fliftfun  7319  fliftval  7323  weniso  7361  riota5f  7404  riotass2  7406  fovcld  7548  ofmpteq  7707  ssorduni  7782  sucexeloniOLD  7814  suceloniOLD  7816  nlimsucg  7847  tfisi  7864  zfrep6  7959  curry1  8109  curry2  8112  fnwelem  8136  funsssuppss  8195  frrlem4  8295  frrlem8  8299  frrlem10  8301  fprlem1  8306  fprlem2  8307  wfrlem4OLD  8333  smogt  8388  tfrlem5  8401  omeulem1  8603  oeworde  8614  oelimcl  8621  oeeulem  8622  oeeui  8623  nnawordex  8658  oaabs2  8670  naddssim  8706  swoso  8758  qliftlem  8817  resixp  8952  domssl  9019  domssr  9020  undomOLD  9085  xpdom3  9095  domunsncan  9097  omxpenlem  9098  domssex  9163  xpf1o  9164  mapdom3  9174  dif1en  9185  findcard  9188  f1dmvrnfibi  9362  fsuppss  9408  fiin  9447  marypha1lem  9458  marypha1  9459  fisupcl  9494  supgtoreq  9495  ordiso2  9540  ordtypelem2  9544  ordtypelem8  9550  wemapso2lem  9577  unxpwdom2  9613  cantnflt  9697  cantnfrescl  9701  oemapvali  9709  cantnflem1d  9713  wemapwe  9722  cnfcom  9725  ttrclss  9745  ttrclselem2  9751  frrlem15  9782  rankr1id  9887  tcrank  9909  cardmin2  10024  infxpenlem  10038  fseqen  10052  ween  10060  ac5num  10061  indcardi  10066  acni2  10071  fodomfi2  10085  infpwfien  10087  inffien  10088  iunfictbso  10139  acacni  10165  dfac12lem2  10169  djuinf  10213  infmap2  10243  ackbij1lem18  10262  ackbij1b  10264  fictb  10270  cfslb2n  10293  cofsmo  10294  cfsmolem  10295  coftr  10298  infpssrlem4  10331  domfin4  10336  fin2i2  10343  isfin2-2  10344  fincssdom  10348  ssfin3ds  10355  fin23lem20  10362  fin23lem30  10367  isf32lem3  10380  fin1a2lem12  10436  fin1a2lem13  10437  hsmexlem2  10452  axdc2lem  10473  imadomg  10559  fnct  10562  iundom2g  10565  iundomg  10566  iundom  10567  unirnfdomd  10592  konigthlem  10593  iunctb  10599  fpwwe2  10668  canthwelem  10675  pwfseqlem3  10685  pwfseqlem5  10688  winalim2  10721  wunelss  10733  r1wunlim  10762  wunex2  10763  tsksdom  10781  tskinf  10794  inttsk  10799  inar1  10800  tskcard  10806  tskurn  10814  gruina  10843  grur1a  10844  grur1  10845  addsrpr  11100  mulsrpr  11101  lemul12a  12105  lemulge11  12109  lediv12a  12140  fiminre2  12195  nngt0  12276  nn0ge2m1nn  12574  peano5uzi  12684  nn0ind-raph  12695  znnn0nn  12706  suprzub  12956  uzsupss  12957  rpge0  13022  fz0fzelfz0  13642  fz0fzdiffz0  13645  ige2m2fzo  13730  elfzodifsumelfzo  13733  elfzom1elp1fzo  13734  fzonfzoufzol  13771  flltdivnn0lt  13834  fldiv  13861  modaddmodup  13935  uzrdgsuci  13961  fzennn  13969  uzindi  13983  fsuppmapnn0fiubex  13993  expcl2lem  14074  leexp1a  14175  modexp  14236  faclbnd  14285  faclbnd6  14294  facavg  14296  hashginv  14329  hashf1rn  14347  hasheqf1od  14348  seqcoll  14461  hashge2el2dif  14477  wrdsymb0  14535  wrdlenge2n0  14538  ccatsymb  14568  swrdnd2  14641  swrdnd0  14643  pfxnd  14673  pfxccat1  14688  swrdpfx  14693  pfxpfx  14694  wrd2ind  14709  pfxccatin12  14719  pfxccat3  14720  swrdccat  14721  pfxccatpfx1  14722  pfxccatpfx2  14723  swrdccatin1d  14729  pfxccatin12d  14731  repswswrd  14770  cshwidxmod  14789  s2f1o  14903  f1oun2prg  14904  wwlktovfo  14945  relexpfld  15032  rtrclreclem3  15043  resqrex  15233  cau3lem  15337  reusq0  15445  rlimcld2  15558  climcn2  15573  isercoll  15650  climsup  15652  caurcvgr  15656  sumeq2ii  15675  summolem3  15696  zsum  15700  fsumadd  15722  fsumsplit1  15727  fsum2dlem  15752  fsum0diag2  15765  fsummulc2  15766  fsumabs  15783  fsumrelem  15789  fsumrlim  15793  fsumo1  15794  o1fsum  15795  fsumiun  15803  qshash  15809  prodeq2ii  15893  prodmolem3  15913  fprodmul  15940  fproddiv  15941  fprod2dlem  15960  fprodsplit1f  15970  sin02gt0  16172  efieq1re  16179  p1modz1  16241  dvdsleabs2  16292  4dvdseven  16353  sumeven  16367  sumodd  16368  divalglem9  16381  smupvallem  16461  algfx  16554  eucalgcvga  16560  lcmfunsnlem1  16611  lcmfunsnlem2lem1  16612  lcmflefac  16622  qredeq  16631  dvdszzq  16696  fermltl  16756  modprm0  16777  pythagtriplem4  16791  pythagtriplem6  16793  pythagtriplem7  16794  pythagtriplem12  16798  pythagtriplem13  16799  pythagtriplem14  16800  pythagtriplem16  16802  difsqpwdvds  16859  pcmpt  16864  prmreclem2  16889  4sqlem11  16927  vdwlem9  16961  vdwlem11  16963  vdwlem12  16964  0ram  16992  0ram2  16993  0ramcl  16995  ramcl  17001  prmolelcmf  17020  cshwsidrepsw  17066  cshwshashlem2  17069  prmlem1  17080  prmlem2  17092  strfvd  17173  strfv2d  17174  strssd  17178  firest  17417  prdsdsval3  17470  imasbas  17497  imasds  17498  imasaddfnlem  17513  imasaddvallem  17514  imasvscafn  17522  qusaddvallem  17536  qusaddflem  17537  qusaddval  17538  qusaddf  17539  qusmulval  17540  qusmulf  17541  catideu  17658  idinv  17775  brcici  17786  invfuc  17969  2initoinv  18002  initoeu1w  18004  initoeu2lem0  18005  2termoinv  18009  termoeu1w  18011  mod2ile  18489  lubss  18508  acsmapd  18549  lidrididd  18633  gsumval2a  18648  mndind  18788  submefmnd  18855  mgm2nsgrplem4  18881  qusgrp2  19022  mulgnegnn  19047  pgrpsubgsymg  19376  fvcosymgeq  19396  gsmsymgreqlem1  19397  psgnunilem4  19464  pgpssslw  19581  sylow2alem2  19585  fislw  19592  efgsres  19705  rinvmod  19773  gsumval3lem2  19873  gsumzaddlem  19888  gsum2d  19939  nn0gsumfz  19951  telgsums  19960  dprddomcld  19970  ablfac2  20058  qusrng  20132  srgdilem  20144  o2timesd  20162  rglcom4d  20163  ringdilem  20201  qusring2  20282  lssintcl  20860  lbsextlem3  21060  lbsextlem4  21061  zringlpirlem3  21407  psgnodpm  21537  psgndiflemB  21549  frlmup4  21752  lindff1  21771  lindfrn  21772  lmisfree  21793  evlseu  22051  mhpmulcl  22096  mptcoe1fsupp  22158  cply1coe0bi  22246  mpfpf1  22295  pf1mpf  22296  mat0dimscm  22415  mdetdiagid  22546  mdet1  22547  mdetunilem9  22566  slesolinv  22626  cramerimp  22632  cpmatmcllem  22664  mptcoe1matfsupp  22748  mp2pm2mp  22757  chpdmat  22787  cctop  22953  subbascn  23202  cnss2  23225  cmpcovf  23339  2ndcctbss  23403  2ndcomap  23406  2ndcsep  23407  comppfsc  23480  ptclsg  23563  dfac14  23566  txcnp  23568  ptcnplem  23569  uptx  23573  txtube  23588  tx2ndc  23599  xkococnlem  23607  elqtop  23645  qtoprest  23665  indishmph  23746  ptcmpfi  23761  kqhmph  23767  csdfil  23842  filssufilg  23859  ufilen  23878  rnelfm  23901  fmfnfmlem4  23905  alexsubALTlem4  23998  ptcmplem4  24003  cnextfvval  24013  cnextcn  24015  cnextfres  24017  tmdgsum2  24044  imasf1oxmet  24325  metss  24461  met2ndci  24475  prdsxmslem2  24482  metust  24511  cfilucfil  24512  metustbl  24519  psmetutop  24520  opnreen  24791  rectbntr0  24792  fsumcn  24832  rescncf  24861  xrhmeo  24915  cnllycmp  24926  lebnumlem1  24931  lebnumlem3  24933  cfilss  25242  iscmet3lem1  25263  iscmet3lem2  25264  ivthicc  25431  ovolsslem  25457  ovoliunlem2  25476  ovoliunnul  25480  ovolicc2lem4  25493  voliunlem3  25525  volsup  25529  uniiccdif  25551  uniioombllem2  25556  volivth  25580  mbfimaopnlem  25628  mbflimsup  25639  i1fd  25654  itg1addlem4  25672  itg1addlem4OLD  25673  itg2addlem  25732  itg2gt0  25734  limciun  25867  dvadd  25915  dvmul  25916  dvco  25923  dvrec  25931  dvcnv  25953  dvferm  25964  rollelem  25965  dvlip  25970  dvlip2  25972  c1liplem1  25973  c1lip2  25975  dvgt0lem1  25979  dvivthlem1  25985  lhop1lem  25990  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcvx  25997  dvfsumle  25998  dvfsumleOLD  25999  dvfsumabs  26001  dvfsumlem1  26004  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem4  26008  dvfsumrlim2  26011  dvfsum2  26013  ftc1cn  26022  ftc2ditglem  26024  itgsubstlem  26027  itgpowd  26029  tdeglem4OLD  26040  mdegaddle  26054  mdegmullem  26058  deg1sublt  26090  ply1divmo  26116  fta1g  26149  dgrub  26213  dgrnznn  26226  dgradd2  26248  dvply1  26263  plyrem  26285  aalioulem4  26315  aalioulem5  26316  aalioulem6  26317  aaliou2  26320  taylf  26340  ulmdv  26384  psercn2  26404  psercn2OLD  26405  abelth  26423  abelth2  26424  reeff1olem  26428  efopn  26637  logreclem  26739  isosctrlem2  26796  xrlimcnp  26945  basellem4  27061  ppiwordi  27139  musum  27168  chpub  27198  gausslemma2dlem0c  27336  2sqlem6  27401  addsqnreup  27421  2sqreulem1  27424  2sqreunnlem1  27427  dchrisumlema  27466  dchrisumlem2  27468  dchrisumlem3  27469  pntlemp  27588  pntleml  27589  ostth3  27616  sltres  27641  noextenddif  27647  nolesgn2ores  27651  nogesgn1ores  27653  nosep1o  27660  nosep2o  27661  nosepeq  27664  nolt02o  27674  noresle  27676  nosupno  27682  nosupbday  27684  nosupres  27686  nosupbnd1lem1  27687  nosupbnd1lem4  27690  nosupbnd1  27693  nosupbnd2lem1  27694  nosupbnd2  27695  noinfno  27697  noinfbday  27699  noinfres  27701  noinfbnd1lem5  27706  noinfbnd1  27708  noinfbnd2lem1  27709  sltled  27748  madebday  27872  sleadd1  27952  precsexlem10  28164  noseqrdg0  28230  noseqrdgsuc  28231  iscgrglt  28390  colline  28525  axlowdimlem16  28840  axlowdimlem17  28841  axcontlem3  28849  axcontlem10  28856  uhgr2edg  29093  nbupgruvtxres  29292  cusgrres  29334  cusgrfilem2  29342  vdumgr0  29366  frusgrnn0  29457  wlkp1lem8  29566  pthdivtx  29615  upgrwlkdvde  29623  spthonepeq  29638  usgr2pthlem  29649  lfgrn1cycl  29688  wwlknbp1  29727  wwlknllvtx  29729  wlkiswwlks2lem3  29754  umgr2adedgspth  29831  clwlkclwwlklem3  29883  clwwisshclwwslemlem  29895  clwwisshclwws  29897  clwwlkel  29928  wwlksubclwwlk  29940  eleclclwwlknlem1  29942  eleclclwwlknlem2  29943  erclwwlknref  29951  clwwlknonccat  29978  clwwlknonex2lem2  29990  3wlkdlem4  30044  vdn0conngrumgrv2  30078  eucrctshift  30125  frgrnbnb  30175  frgrncvvdeqlem2  30182  frgrncvvdeqlem3  30183  fusgreghash2wspv  30217  numclwwlk2lem1  30258  numclwlk2lem2f  30259  numclwwlk5  30270  numclwwlk7  30273  frgrreggt1  30275  minvecolem4b  30760  minvecolem4  30762  bcsiALT  31061  ococin  31290  spanpr  31462  pjorthi  31551  nmbdoplbi  31906  nmcoplbi  31910  nmbdfnlbi  31931  nmcfnlbi  31934  nmopcoi  31977  branmfn  31987  hstnmoc  32105  mdsl0  32192  atomli  32264  atcvat4i  32279  atabsi  32283  foresf1o  32378  rabfodom  32379  abrexdomjm  32380  elpreq  32405  ifeqeqx  32412  disjiunel  32465  aciunf1lem  32529  ffsrn  32593  xlt2addrd  32610  supxrnemnf  32620  ssnnssfz  32637  resspos  32782  resstos  32783  gsummptres2  32857  archirngz  32989  orngsqr  33118  isarchiofld  33131  unitprodclb  33201  elrspunidl  33240  drngidlhash  33246  prmidl2  33253  qsidomlem2  33265  ssmxidl  33286  1arithidom  33349  1arithufdlem4  33362  locfinreflem  33572  cmpcref  33582  fmcncfil  33663  xrge0iifiso  33667  elzdif0  33712  qqhval2lem  33713  esumcst  33813  esumrnmpt2  33818  esumpinfval  33823  esumpinfsum  33827  sigaclci  33882  insiga  33887  ldgenpisys  33916  measres  33972  measdivcstALTV  33975  dya2iocnrect  34032  dya2iocnei  34033  omssubadd  34051  carsggect  34069  carsgclctunlem2  34070  sitgclg  34093  eulerpartlemsv2  34109  eulerpartlemv  34115  eulerpartlemf  34121  eulerpartlemgh  34129  eulerpartlemgs2  34131  ballotlemfp1  34242  ballotlemfrcn0  34280  ftc2re  34361  fdvposlt  34362  fdvposle  34364  bnj1379  34592  bnj580  34675  bnj944  34700  bnj999  34720  bnj1204  34774  bnj1398  34796  cusgredgex  34862  pthacycspth  34898  derangenlem  34912  subfacp1lem3  34923  resconn  34987  cvmliftlem3  35028  satfv0fvfmla0  35154  satfv1fvfmla1  35164  mrsub0  35257  cgrextend  35735  segconeq  35737  trisegint  35755  fwddifnp1  35892  ivthALT  35950  fnessref  35972  refssfne  35973  neibastop1  35974  filnetlem4  35996  ontgval  36046  unblimceq0lem  36112  unbdqndv2lem2  36116  unbdqndv2  36117  bj-babygodel  36211  bj-alrimd  36227  bj-exlimd  36232  bj-spcimdv  36504  bj-spcimdvv  36505  bj-finsumval0  36895  bj-fvimacnv0  36896  dfgcd3  36934  relowlssretop  36973  relowlpssretop  36974  onsucuni3  36977  finxpreclem4  37004  poimirlem18  37242  poimirlem21  37245  poimirlem25  37249  ftc1cnnclem  37295  ftc1cnnc  37296  ftc2nc  37306  dvasin  37308  dvacos  37309  abrexdom  37334  indexdom  37338  mettrifi  37361  equivtotbnd  37382  totbndbnd  37393  prdstotbnd  37398  heibor1lem  37413  bfplem1  37426  bfplem2  37427  opidonOLD  37456  rngodm1dm2  37536  zerdivemp1x  37551  equid1  38501  omllaw5N  38849  cmtcomlemN  38850  cmtbr3N  38856  omlfh3N  38861  atlen0  38912  exatleN  39007  hlrelat3  39015  cvrexchlem  39022  atlelt  39041  cvrat4  39046  4atlem11b  39211  4atlem12b  39214  lneq2at  39381  cdlema1N  39394  cdlemblem  39396  paddss12  39422  paddasslem2  39424  paddasslem4  39426  paddasslem6  39428  paddasslem12  39434  paddunN  39530  poml4N  39556  poml5N  39557  osumcllem6N  39564  pexmidlem6N  39578  pl42lem2N  39583  ltrnu  39724  ltrneq2  39751  trlval2  39766  cdlemd6  39806  cdleme25b  39957  cdleme29b  39978  cdlemefr29exN  40005  ltrniotacnvval  40185  cdlemk28-3  40511  dochexmidlem7  41069  muldvds2d  41601  frlmsnic  41908  nna4b4nsq  42219  mzpsubmpt  42305  mzpsubst  42310  eqrabdioph  42339  rabdiophlem2  42364  elpell14qr2  42424  elpell1qr2  42434  pellfundre  42443  pellfundge  42444  pellfundglb  42447  pellfund14gap  42449  congabseq  42537  jm2.22  42558  jm2.23  42559  jm2.26lem3  42564  wepwsolem  42608  dnwech  42614  aomclem2  42621  aomclem4  42623  pwfi2f1o  42662  onexlimgt  42813  oaltublim  42861  oege1  42877  cantnfub2  42893  cantnfresb  42895  cantnf2  42896  oacl2g  42901  tfsconcatb0  42915  tfsconcatrev  42919  oaun3lem1  42945  oaun3lem2  42946  nadd2rabtr  42955  nadd1suc  42963  naddsuc2  42964  naddwordnexlem0  42968  naddwordnexlem3  42971  oawordex3  42972  naddwordnexlem4  42973  oaltom  42977  omltoe  42979  ss2iundf  43231  dssmapf1od  43593  neik0pk1imk0  43619  gneispace  43706  grur1cld  43811  cpcolld  43837  mnuop23d  43845  mnuprdlem1  43851  mnuprdlem2  43852  mnurndlem1  43860  grumnudlem  43864  radcnvrat  43893  sbiota1  44013  ordelordALT  44118  2pm13.193  44133  ee11an  44271  refsumcn  44534  rfcnnnub  44540  disjxp1  44575  xrnmnfpnf  44589  ssinc  44593  nssd  44611  disjf1o  44703  disjinfi  44704  choicefi  44712  axccdom  44734  dmrelrnrel  44738  monoords  44817  fperiodmullem  44823  xadd0ge  44840  xrssre  44868  xrlexaddrp  44872  xrred  44885  infxr  44887  xrnpnfmnf  44995  monoordxrv  45002  monoord2xrv  45004  cvgcaule  45012  fsumiunss  45101  fmul01  45106  fmuldfeqlem1  45108  fmuldfeq  45109  fmul01lt1lem1  45110  fmul01lt1lem2  45111  cncfmptss  45113  climinf  45132  climsuselem1  45133  climsuse  45134  limcperiod  45154  limcrecl  45155  sumnnodd  45156  limcleqr  45170  0ellimcdiv  45175  climleltrp  45202  limsuppnfdlem  45227  limsupresxr  45292  liminfresxr  45293  liminfvalxr  45309  cnrefiisplem  45355  xlimmnfvlem1  45358  xlimpnfvlem1  45362  cncfperiod  45405  icccncfext  45413  cncfiooicclem1  45419  dvbdfbdioolem1  45454  dvnmptdivc  45464  dvdsn1add  45465  dvnmptconst  45467  dvnmul  45469  dvmptfprodlem  45470  dvmptfprod  45471  dvnprodlem2  45473  iblspltprt  45499  itgsubsticclem  45501  itgspltprt  45505  itgsbtaddcnst  45508  stoweidlem3  45529  stoweidlem16  45542  stoweidlem17  45543  stoweidlem19  45545  stoweidlem20  45546  stoweidlem23  45549  stoweidlem25  45551  stoweidlem27  45553  stoweidlem31  45557  stoweidlem34  45560  stoweidlem42  45568  stoweidlem48  45574  stoweidlem51  45577  stoweidlem52  45578  stoweidlem59  45585  wallispilem1  45591  wallispilem3  45593  stirlinglem13  45612  fourierdlem16  45649  fourierdlem20  45653  fourierdlem21  45654  fourierdlem38  45671  fourierdlem42  45675  fourierdlem46  45678  fourierdlem48  45680  fourierdlem49  45681  fourierdlem50  45682  fourierdlem54  45686  fourierdlem68  45700  fourierdlem72  45704  fourierdlem73  45705  fourierdlem76  45708  fourierdlem79  45711  fourierdlem81  45713  fourierdlem86  45718  fourierdlem89  45721  fourierdlem90  45722  fourierdlem91  45723  fourierdlem92  45724  fourierdlem97  45729  fourierdlem101  45733  fourierdlem103  45735  fourierdlem104  45736  fourierdlem111  45743  etransclem24  45784  etransclem25  45785  etransclem28  45788  etransclem41  45801  etransclem44  45804  etransclem48  45808  salexct  45860  dfsalgen2  45867  sge0f1o  45908  sge0rnbnd  45919  sge0split  45935  sge0iunmptlemre  45941  sge0fodjrnlem  45942  sge0iunmpt  45944  nnfoctbdjlem  45981  iundjiunlem  45985  meadjiunlem  45991  ismeannd  45993  meaiuninclem  46006  omeiunle  46043  carageniuncllem1  46047  caratheodorylem1  46052  hoidmvlelem4  46124  hoiqssbllem2  46149  salpreimagelt  46233  salpreimalegt  46235  pimdecfgtioc  46241  smfaddlem2  46290  smflimlem6  46302  nsssmfmbflem  46304  smfpimcclem  46333  or2expropbilem1  46552  funressndmfvrn  46564  f1cof1b  46595  2leaddle2  46816  smonoord  46848  uniimaprimaeqfv  46859  fundcmpsurbijinjpreimafv  46884  fundcmpsurinjALT  46889  iccpartf  46908  ich2exprop  46948  ichnreuop  46949  ichreuopeq  46950  sprbisymrel  46976  fmtnodvds  47021  proththdlem  47090  gbowgt5  47239  gboge9  47241  gbege6  47242  stgoldbwt  47253  sbgoldbalt  47258  bgoldbnnsum3prm  47281  uspgrbisymrelALT  47403  ssnn0ssfz  47599  ldepspr  47727  seposep  48130  subthinc  48232  prsthinc  48246  iunord  48293  bnd2d  48298  setrecsss  48318