Theorem biimpd 229

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 215 and biimpi 216. (Contributed by NM, 11-Jan-1993.)

Hypothesis

Ref	Expression
biimpd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 215	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  mpbid  232  sylibd  239  sylbid  240  mpbidi  241  imbitrid  244  biimtrdi  253  con4bid  317  mtbird  325  mtbiri  327  imbi1d  341  bitr3  352  pm5.21im  374  biimpa  476  bi23imp13  1115  alexbii  1833  spvv  1988  spfw  2033  cbvalw  2035  sbequi  2085  chvarfv  2241  cbvalv1  2339  spv  2392  chvar  2394  cbval  2397  sb1  2477  nfsb4t  2498  exmoeu  2575  euim  2611  2eu3  2648  eqrdav  2729  ralbida  3249  rgen2a  3347  ralcom2  3353  ceqsalt  3484  ceqsalgALT  3487  spcimgft  3515  vtoclfOLD  3534  vtoclegft  3557  spcdv  3563  rspcdv  3583  rspcebdv  3585  rexraleqim  3616  sbcn1  3809  sbcbi1  3814  sbeqalb  3819  sbcel21v  3824  disj  4416  elpwunsn  4651  rabsnifsb  4689  ssunsn2  4794  preqr1g  4819  iuneqconst  4970  axprlem3  5383  axprlem3OLD  5386  sbcop1  5451  propeqop  5470  euotd  5476  rexopabb  5491  sotr2  5583  relop  5817  elinxp  5993  elimasni  6065  sotri2  6105  onmindif  6429  iotavalOLD  6488  dffv2  6959  mpteqb  6990  elfvmptrab  7000  chfnrn  7024  elpreima  7033  iinpreima  7044  exfo  7080  ffnfv  7094  f1elima  7241  f1ounsn  7250  f1eqcocnv  7279  fliftfun  7290  soisores  7305  isotr  7314  isomin  7315  ovmpodv2  7550  difsnexi  7740  onint  7769  oneqmin  7779  ordunisuc2  7823  tfindsg  7840  findsg  7876  resf1extb  7913  f1oweALT  7954  el2mpocl  8068  poseq  8140  soseq  8141  ressuppss  8165  funsssuppss  8172  suppofssd  8185  smoiso  8334  seqomlem2  8422  oaordi  8513  oawordri  8517  oaordex  8525  oalimcl  8527  omwordi  8538  oewordi  8558  oelim2  8562  nnmwordi  8602  xpider  8764  iiner  8765  undifixp  8910  mptelixpg  8911  dom2lem  8966  findcard2s  9135  pssnn  9138  nneneq  9176  fineqvlem  9216  dif1ennnALT  9229  unfilem2  9262  xpfiOLD  9277  domunfican  9279  f1dmvrnfibi  9299  fsuppimp  9326  dffi2  9381  infsupprpr  9464  wemaplem2  9507  suc11reg  9579  noinfep  9620  cantnflem1  9649  r1fin  9733  tcrank  9844  cardlim  9932  pr2nelemOLD  9963  fseqenlem1  9984  alephnbtwn  10031  alephord2i  10037  alephf1  10045  cardaleph  10049  alephiso  10058  dfac12lem2  10105  ackbij1lem16  10194  cflm  10210  cfcoflem  10232  sornom  10237  fin23lem27  10288  isf32lem7  10319  fin17  10354  fin1a2lem2  10361  fin1a2lem4  10363  fin1a2lem6  10365  fin1a2lem9  10368  axdc3lem2  10411  zorn2lem7  10462  uniimadom  10504  inar1  10735  grothomex  10789  addcanpi  10859  mulcanpi  10860  enqer  10881  genpcd  10966  genpnmax  10967  ltexprlem4  10999  reclem3pr  11009  reclem4pr  11010  suplem2pr  11013  axpre-ltadd  11127  axpre-sup  11129  ltletr  11273  00id  11356  addn0nid  11605  mul0or  11825  prodgt02  12037  lemul1a  12043  mulgt1OLD  12048  divgt0  12058  divge0  12059  ledivp1i  12115  ltdivp1i  12116  cju  12189  nnsub  12237  nominpos  12426  nn0n0n1ge2  12517  btwnnz  12617  suprfinzcl  12655  ublbneg  12899  zmax  12911  cnref1o  12951  ltsubrp  12996  ltaddrp  12997  xrltletr  13124  qbtwnre  13166  xltnegi  13183  xnn0xadd0  13214  iccsupr  13410  icoshft  13441  difreicc  13452  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  fzen  13509  elfz1b  13561  fzofzim  13677  eluzgtdifelfzo  13695  elfzo1elm1fzo0  13736  injresinjlem  13755  injresinj  13756  flval2  13783  flval3  13784  modmuladdim  13886  modaddmodup  13906  addmodlteq  13918  fseqsupubi  13950  ssnn0fi  13957  mptnn0fsuppr  13971  sq01  14197  hashf1rn  14324  hashgt12el  14394  hashgt12el2  14395  hashfundm  14414  hash2pr  14441  hash2exprb  14443  hashge2el2difr  14453  hashtpg  14457  hash3tr  14463  lswlgt0cl  14541  ccatalpha  14565  pfxfv  14654  pfxsuff1eqwrdeq  14671  ccatopth2  14689  swrdccat  14707  swrdccat3blem  14711  reuccatpfxs1lem  14718  repsdf2  14750  repswsymball  14751  repswrevw  14759  cshweqrep  14793  cshw1  14794  2cshwcshw  14798  scshwfzeqfzo  14799  cshwcsh2id  14801  swrdco  14810  swrd2lsw  14925  2swrd2eqwrdeq  14926  wwlktovfo  14931  cjre  15112  icodiamlt  15411  reusq0  15438  o1lo1  15510  o1of2  15586  o1rlimmul  15592  zsum  15691  modfsummods  15766  zprod  15910  reeff1  16095  dvdsmod0  16235  dvds2lem  16245  muldvds1  16257  dvdscmulr  16261  dvdsmulcr  16262  dvdsdivcl  16293  mod2eq1n2dvds  16324  oddnn02np1  16325  divalglem8  16377  ndvdsadd  16387  zeqzmulgcd  16487  dfgcd2  16523  absproddvds  16594  lcmftp  16613  coprmdvds  16630  2mulprm  16670  isprm5  16684  divgcdodd  16687  isprm6  16691  prmdvdsexpr  16694  prmdvdsbc  16703  cncongrprm  16706  phiprmpw  16753  modprm0  16783  pythagtriplem4  16797  pcz  16859  difsqpwdvds  16865  1arith  16905  prmgaplem5  17033  prmgaplem6  17034  cshwrepswhash1  17080  sbcie2s  17138  divsfval  17517  catsubcat  17808  fthmon  17898  isinitoi  17968  istermoi  17969  iszeroi  17978  setcmon  18056  setcepi  18057  funcestrcsetclem8  18115  fthestrcsetc  18118  funcsetcestrclem8  18130  fthsetcestrc  18133  odupos  18294  pltnle  18304  pltval3  18305  lublecllem  18326  latasym  18409  mrelatglb  18526  mrelatlub  18528  cnvpsb  18545  mgmpropd  18585  isgrpid2  18915  ghmghmrn  19174  ghmf1  19185  kerf1ghm  19186  orbsta  19252  resscntz  19272  gsmsymgrfixlem1  19364  gsmsymgreqlem2  19368  mndodcongi  19480  odf1  19499  lsmss1  19602  lsmss2  19604  efgredeu  19689  cntzcmnss  19778  imasabl  19813  lt6abl  19832  ablfaclem3  20026  ringinvnz1ne0  20216  0ringnnzr  20441  subrngringnsg  20469  srhmsubc  20596  domnmuln0  20625  lspsneq  21039  lspsneu  21040  lsmcv  21058  rnglidlmcl  21133  rngqiprngimf1lem  21211  lidldvgen  21251  domnchr  21449  znf1o  21468  zntoslem  21473  znfld  21477  cygznlem2a  21484  cygznlem3  21486  phlssphl  21575  islindf4  21754  uvcendim  21763  psdmul  22060  ply1scln0  22185  gsummoncoe1  22202  matvscl  22325  scmataddcl  22410  scmatsubcl  22411  scmatfo  22424  scmatghm  22427  maducoeval2  22534  slesolinv  22574  cramerimplem2  22578  cpmatelimp  22606  cpmatelimp2  22608  cpmatacl  22610  cpmatinvcl  22611  pm2mpf1  22693  cayhamlem1  22760  cayleyhamilton1  22786  0ntr  22965  islpi  23043  lmss  23192  cmpcld  23296  cmpfi  23302  1stcelcls  23355  comppfsc  23426  ptcnplem  23515  qtophmeo  23711  fbdmn0  23728  fbasrn  23778  elfm3  23844  fmfnfmlem4  23851  fclscf  23919  cnpfcf  23935  alexsubALTlem3  23943  tsmsres  24038  blval2  24457  tnggrpr  24550  nmoleub  24626  nmhmcn  25027  ncvs1  25064  iscau4  25186  caussi  25204  cmssmscld  25257  cmslssbn  25279  cniccbdd  25369  ovoliunnul  25415  mbfinf  25573  itg2splitlem  25656  dvcn  25830  c1lip1  25909  c1lip3  25911  dvcnvrelem1  25929  dvfsumlem2  25940  ply1divex  26049  quotcan  26224  aannenlem1  26243  taylf  26275  taylthlem2  26289  ulmcaulem  26310  ulmcau  26311  reeff1o  26364  logccv  26579  rtprmirr  26677  logreclem  26679  isosctrlem2  26736  xrlimcnp  26885  rlimcxp  26891  ftalem7  26996  vmappw  27033  fsumdvdsmul  27112  fsumvma  27131  dchreq  27176  dchrptlem1  27182  dchrsum  27187  bposlem7  27208  lgsqrlem2  27265  lgsdchr  27273  gausslemma2dlem1a  27283  lgseisenlem2  27294  lgsquad2  27304  2lgslem1b  27310  2sqlem6  27341  2sqnn0  27356  addsq2reu  27358  2sqreulem2  27370  sltval2  27575  sltres  27581  nodenselem8  27610  nodense  27611  noresle  27616  scutun12  27729  madeval2  27768  elmade  27786  negsf1o  27967  muls0ord  28095  recsex  28128  bdayon  28180  noseqrdgfn  28207  n0subs  28260  eln0zs  28295  tgcgrcomimp  28411  isperp2  28649  xmstrkgc  28820  brbtwn  28833  brcgr  28834  axcgrid  28850  axeuclidlem  28896  axeuclid  28897  elntg2  28919  lpvtx  29002  upgrex  29026  upgrpredgv  29073  upgredgpr  29076  uhgr0v0e  29172  subgrprop  29207  fusgrfisbase  29262  edgnbusgreu  29301  nbusgredgeu0  29302  cusgredg  29358  structtocusgr  29380  cusgrsize2inds  29388  cusgrsize  29389  usgredgsscusgredg  29394  fusgrmaxsize  29399  uspgrloopvtxel  29451  umgr2v2e  29460  vtxdginducedm1fi  29479  finsumvtxdg2sstep  29484  rgrprop  29495  rusgrprop  29497  0uhgrrusgr  29513  rusgrpropedg  29519  ewlkprop  29538  upgrewlkle2  29541  wlkprop  29546  upgrwlkcompim  29578  uspgr2wlkeq  29581  wlklenvclwlk  29590  wlkonprop  29593  wlkres  29605  redwlk  29607  wlkdlem2  29618  wksonproplem  29639  wksonproplemOLD  29640  usgr2trlspth  29698  usgr2pth  29701  pthdlem1  29703  crctcshwlkn0lem4  29750  wwlksnprcl  29776  wlkiswwlks2  29812  wwlksm1edg  29818  wlknewwlksn  29824  wwlksnred  29829  wwlksnextbi  29831  wwlksnextwrd  29834  wwlksnextinj  29836  wwlksnextsurj  29837  umgr2wlk  29886  umgrwwlks2on  29894  elwwlks2  29903  clwwlk1loop  29924  umgrclwwlkge2  29927  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlkfo  29945  clwwisshclwwslemlem  29949  clwwlknwwlksn  29974  clwwlknlbonbgr1  29975  clwwlkn1loopb  29979  clwwlkf  29983  clwwlknon1  30033  clwwlknonwwlknonb  30042  clwwlknonex2lem2  30044  vdn0conngrumgrv2  30132  frgrnbnb  30229  frgrncvvdeqlem2  30236  frgrncvvdeqlem3  30237  frgrncvvdeqlem6  30240  frgrwopreglem4a  30246  fusgr2wsp2nb  30270  frrusgrord0lem  30275  numclwwlk2lem1lem  30278  2clwwlk2clwwlklem  30282  2clwwlk2clwwlk  30286  numclwwlk1lem2foa  30290  numclwwlk1lem2f1  30293  frgrreg  30330  hlipgt0  30850  ocin  31232  ocnel  31234  shmodsi  31325  pjmf1  31652  unopf1o  31852  staddi  32182  stadd3i  32184  mdi  32231  dmdmd  32236  dmdi  32238  dmdbr2  32239  dmdbr3  32241  dmdbr4  32242  dmdi4  32243  mdsl1i  32257  superpos  32290  cvbr4i  32303  atssma  32314  atcv1  32316  atomli  32318  chirredlem1  32326  addltmulALT  32382  bian1dOLD  32393  ifeqeqx  32478  disjxpin  32524  suppss3  32654  fpwrelmap  32663  expgt0b  32748  mndlactfo  32975  mndractfo  32977  ogrpaddlt  33038  qsfld  33476  ply1degltdimlem  33625  ply1degltdim  33626  metider  33891  tpr2rico  33909  xrge0iifiso  33932  qqhcn  33988  qqhucn  33989  esumlub  34057  esumpinfval  34070  esumpinfsum  34074  ballotlemfc0  34491  ballotlemfcc  34492  ftc2re  34596  bnj517  34882  axsepg2  35079  axsepg2ALT  35080  fnrelpredd  35086  axnulg  35089  pfxwlk  35118  subgrwlk  35126  loop1cycl  35131  erdsze2lem2  35198  satfv1  35357  satfdmlem  35362  satf0op  35371  fmlasuc  35380  dfrdg4  35946  altopthsn  35956  btwncomim  36008  btwnexch3  36015  btwnexch2  36018  endofsegid  36080  opnrebl2  36316  nn0prpwlem  36317  onsuct0  36436  ordcmp  36442  nndivsub  36452  dnibndlem13  36485  bj-cbval  36644  bj-cbvex  36645  bj-cbvexw  36671  bj-cbv3tb  36782  bj-spimtv  36789  bj-equsal  36821  bj-sbsb  36832  bj-vtoclf  36910  bj-zfauscl  36919  bj-gabss  36930  bj-gabeqd  36932  currysetlem2  36943  bj-snsetex  36958  bj-ismooredr2  37105  bj-inftyexpiinj  37204  bj-finsumval0  37280  bj-fvimacnv0  37281  bj-bary1lem1  37306  bj-bary1  37307  f1omptsnlem  37331  iooelexlt  37357  relowlpssretop  37359  rdgeqoa  37365  finxpsuclem  37392  fvineqsneq  37407  pibt2  37412  wl-isseteq  37500  wl-equsal1i  37539  wl-ax11-lem10  37589  ltflcei  37609  sin2h  37611  cos2h  37612  tan2h  37613  lindsenlbs  37616  matunitlindf  37619  poimirlem3  37624  poimirlem4  37625  poimirlem18  37639  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  poimir  37654  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  mbfresfi  37667  cnambfre  37669  ftc1anc  37702  dvasin  37705  areacirclem1  37709  areacirclem4  37712  areacirc  37714  brabg2  37718  fzmul  37742  fdc  37746  incsequz2  37750  isbnd2  37784  opidonOLD  37853  opidon2OLD  37855  grpomndo  37876  elghomlem2OLD  37887  rngoueqz  37941  dvrunz  37955  divrngidl  38029  refressn  38441  dral1-o  38904  lsatn0  38999  l1cvpat  39054  leat2  39294  atnle  39317  cvlcvr1  39339  cvrexchlem  39420  cvratlem  39422  cvrat  39423  atcvrj0  39429  atle  39437  snatpsubN  39751  linepsubN  39753  pmapsub  39769  lneq2at  39779  lncvrelatN  39782  2llnma3r  39789  cdlemblem  39794  paddasslem5  39825  poml4N  39954  lhpmcvr4N  40027  trlval2  40164  cdlemd6  40204  cdleme7ga  40249  cdleme25b  40355  cdleme29b  40376  cdleme35fnpq  40450  cdleme50f1  40544  cdlemf1  40562  cdlemg27b  40697  cdlemk28-3  40909  tendospcanN  41024  diaf11N  41050  dia2dimlem1  41065  dibf11N  41162  dihf11  41268  dihmeetlem1N  41291  dochvalr  41358  dochnel2  41393  dvh4dimlem  41444  dochsat0  41458  mapd1o  41649  hdmapf1oN  41866  hgmapval0  41893  hgmapf1oN  41904  hlhilhillem  41961  nnproddivdvdsd  41995  lcmineqlem  42047  aks4d1p1p5  42070  aks4d1p3  42073  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1p9  42083  fldhmf1  42085  isprimroot2  42089  primrootsunit1  42092  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij  42097  primrootlekpowne0  42100  primrootspoweq0  42101  aks6d1c1p1  42102  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1p8  42110  aks6d1c2p2  42114  aks6d1c2lem3  42121  aks6d1c2lem4  42122  hashnexinj  42123  hashnexinjle  42124  aks6d1c2  42125  aks6d1c5lem0  42130  aks6d1c5lem1  42131  aks6d1c5  42134  sticksstones1  42141  sticksstones3  42143  sticksstones8  42148  sticksstones11  42151  sticksstones12  42153  sticksstones20  42161  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6lem5  42172  aks6d1c7  42179  rhmqusspan  42180  unitscyglem2  42191  unitscyglem3  42192  aks5lem8  42196  sn-axprlem3  42212  oexpreposd  42317  sn-remul0ord  42403  frlmsnic  42535  fsuppind  42585  prjspval  42598  rexrabdioph  42789  fphpdo  42812  irrapxlem3  42819  rmxypairf1o  42907  rmxycomplete  42913  zindbi  42942  lermxnn0  42946  ltrmy  42948  rmyeq0  42949  rmyeq  42950  lermy  42951  acongsym  42972  acongneg2  42973  wepwsolem  43038  onsupuni  43225  onsupmaxb  43235  onsucf1o  43268  onov0suclim  43270  oe0suclim  43273  onsucwordi  43284  cantnfresb  43320  omabs2  43328  tfsconcat0b  43342  tfsconcatrev  43344  naddcnffo  43360  oaun3lem1  43370  oaltom  43401  omltoe  43403  sdomne0  43409  sdomne0d  43410  safesnsupfidom1o  43413  intabssd  43515  iscard4  43529  ss2iundf  43655  frege129d  43759  frege133d  43761  axfrege52a  43852  axfrege52c  43883  ntrk0kbimka  44035  gneispace  44130  suprleubrd  44162  suprlubrd  44164  radcnvrat  44310  nzss  44313  expgrowthi  44329  ordpss  44447  bi23impib  44483  rspsbc2  44531  tratrb  44533  sbcim2g  44535  truniALT  44538  3impcombi  44813  tpid3gVD  44838  orbi1rVD  44844  sbc3orgVD  44847  rspsbc2VD  44851  tratrbVD  44857  sbcim2gVD  44871  sbcbiVD  44872  truniALTVD  44874  trintALTVD  44876  trintALT  44877  csbingVD  44880  csbsngVD  44889  csbxpgVD  44890  csbresgVD  44891  csbrngVD  44892  csbima12gALTVD  44893  csbunigVD  44894  csbfv12gALTVD  44895  relopabVD  44897  isosctrlem1ALT  44930  relpfrlem  44950  trfr  44959  fzisoeu  45305  xrralrecnnge  45393  allbutfi  45396  climinf  45611  liminfreuzlem  45807  climliminf  45811  climliminflimsup  45813  xlimpnfxnegmnf  45819  xlimbr  45832  stoweidlem7  46012  stoweidlem62  46067  sge0gerpmpt  46407  meaiuninclem  46485  carageniuncllem2  46527  issmflem  46732  et-sqrtnegnre  46878  ormkglobd  46880  natlocalincr  46881  tworepnotupword  46891  funressnfv  47048  funressnvmo  47050  f1cof1b  47082  2reu3  47115  ralbinrald  47127  afv0fv0  47154  afv0nbfvbi  47156  afvfv0bi  47157  fnbrafvb  47159  afvres  47177  tz6.12-afv  47178  afvco2  47181  ndmaovcl  47208  afv2res  47244  tz6.12-afv2  47245  nelbrim  47280  f1oresf1o2  47296  zm1nn  47307  nltle2tri  47318  subsubelfzo0  47331  2tceilhalfelfzo1  47337  iccpartres  47423  iccpartiltu  47427  fargshiftfv  47444  ichnreuop  47477  ichreuopeq  47478  prsprel  47492  sprsymrelf1lem  47496  sprsymrelfolem2  47498  sprsymrelfo  47502  prpair  47506  paireqne  47516  sbcpr  47526  fmtnof1  47540  goldbachthlem2  47551  fmtnoprmfac1  47570  fmtnoprmfac2  47572  lighneallem2  47611  lighneallem4b  47614  lighneallem4  47615  evennodd  47648  oddneven  47649  oexpnegnz  47683  evenltle  47722  fpprwppr  47744  fpprwpprb  47745  gbowge7  47768  gbege6  47770  sbgoldbwt  47782  sbgoldbst  47783  nnsum3primesle9  47799  bgoldbtbndlem2  47811  grimprop  47887  isuspgrimlem  47899  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  grtriproplem  47942  isgrtri  47946  grimgrtri  47952  stgr1  47964  isubgr3stgr  47978  grlimprop  47987  uspgrlimlem2  47992  uspgrlimlem3  47993  gpg5nbgrvtx13starlem1  48066  clintop  48200  isassintop  48202  lidldomn1  48223  uzlidlring  48227  2zrngnmlid2  48249  rngccatidALTV  48264  ringccatidALTV  48298  srhmsubcALTV  48317  ztprmneprm  48339  pgrpgt2nabl  48358  lindslinindimp2lem4  48454  lincresunit3  48474  fldivexpfllog2  48558  digexp  48600  naryfvalelfv  48625  affinecomb1  48695  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  eenglngeehlnm  48732  itscnhlc0yqe  48752  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  itsclquadeu  48770  inlinecirc02plem  48779  inlinecirc02p  48780  pm4.71da  48782  mofsn  48836  seposep  48918  resipos  48967  idmon  49013  idepi  49014  prsthinc  49457  grptcmon  49586  grptcepi  49587  spd  49671  spcdvw  49672  setrec2fun  49685