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  2391  chvar  2393  cbval  2396  sb1  2476  nfsb4t  2497  exmoeu  2574  euim  2610  2eu3  2647  eqrdav  2728  ralbida  3248  rgen2a  3345  ralcom2  3351  ceqsalt  3481  ceqsalgALT  3484  spcimgft  3512  vtoclfOLD  3531  vtoclegft  3554  spcdv  3560  rspcdv  3580  rspcebdv  3582  rexraleqim  3613  sbcn1  3806  sbcbi1  3811  sbeqalb  3816  sbcel21v  3821  disj  4413  elpwunsn  4648  rabsnifsb  4686  ssunsn2  4791  preqr1g  4816  iuneqconst  4967  axprlem3  5380  axprlem3OLD  5383  sbcop1  5448  propeqop  5467  euotd  5473  rexopabb  5488  sotr2  5580  relop  5814  elinxp  5990  elimasni  6062  sotri2  6102  onmindif  6426  iotavalOLD  6485  dffv2  6956  mpteqb  6987  elfvmptrab  6997  chfnrn  7021  elpreima  7030  iinpreima  7041  exfo  7077  ffnfv  7091  f1elima  7238  f1ounsn  7247  f1eqcocnv  7276  fliftfun  7287  soisores  7302  isotr  7311  isomin  7312  ovmpodv2  7547  difsnexi  7737  onint  7766  oneqmin  7776  ordunisuc2  7820  tfindsg  7837  findsg  7873  resf1extb  7910  f1oweALT  7951  el2mpocl  8065  poseq  8137  soseq  8138  ressuppss  8162  funsssuppss  8169  suppofssd  8182  smoiso  8331  seqomlem2  8419  oaordi  8510  oawordri  8514  oaordex  8522  oalimcl  8524  omwordi  8535  oewordi  8555  oelim2  8559  nnmwordi  8599  xpider  8761  iiner  8762  undifixp  8907  mptelixpg  8908  dom2lem  8963  findcard2s  9129  pssnn  9132  nneneq  9170  fineqvlem  9209  dif1ennnALT  9222  unfilem2  9255  xpfiOLD  9270  domunfican  9272  f1dmvrnfibi  9292  fsuppimp  9319  dffi2  9374  infsupprpr  9457  wemaplem2  9500  suc11reg  9572  noinfep  9613  cantnflem1  9642  r1fin  9726  tcrank  9837  cardlim  9925  pr2nelemOLD  9956  fseqenlem1  9977  alephnbtwn  10024  alephord2i  10030  alephf1  10038  cardaleph  10042  alephiso  10051  dfac12lem2  10098  ackbij1lem16  10187  cflm  10203  cfcoflem  10225  sornom  10230  fin23lem27  10281  isf32lem7  10312  fin17  10347  fin1a2lem2  10354  fin1a2lem4  10356  fin1a2lem6  10358  fin1a2lem9  10361  axdc3lem2  10404  zorn2lem7  10455  uniimadom  10497  inar1  10728  grothomex  10782  addcanpi  10852  mulcanpi  10853  enqer  10874  genpcd  10959  genpnmax  10960  ltexprlem4  10992  reclem3pr  11002  reclem4pr  11003  suplem2pr  11006  axpre-ltadd  11120  axpre-sup  11122  ltletr  11266  00id  11349  addn0nid  11598  mul0or  11818  prodgt02  12030  lemul1a  12036  mulgt1OLD  12041  divgt0  12051  divge0  12052  ledivp1i  12108  ltdivp1i  12109  cju  12182  nnsub  12230  nominpos  12419  nn0n0n1ge2  12510  btwnnz  12610  suprfinzcl  12648  ublbneg  12892  zmax  12904  cnref1o  12944  ltsubrp  12989  ltaddrp  12990  xrltletr  13117  qbtwnre  13159  xltnegi  13176  xnn0xadd0  13207  iccsupr  13403  icoshft  13434  difreicc  13445  iccshftri  13448  iccshftli  13450  iccdili  13452  icccntri  13454  fzen  13502  elfz1b  13554  fzofzim  13670  eluzgtdifelfzo  13688  elfzo1elm1fzo0  13729  injresinjlem  13748  injresinj  13749  flval2  13776  flval3  13777  modmuladdim  13879  modaddmodup  13899  addmodlteq  13911  fseqsupubi  13943  ssnn0fi  13950  mptnn0fsuppr  13964  sq01  14190  hashf1rn  14317  hashgt12el  14387  hashgt12el2  14388  hashfundm  14407  hash2pr  14434  hash2exprb  14436  hashge2el2difr  14446  hashtpg  14450  hash3tr  14456  lswlgt0cl  14534  ccatalpha  14558  pfxfv  14647  pfxsuff1eqwrdeq  14664  ccatopth2  14682  swrdccat  14700  swrdccat3blem  14704  reuccatpfxs1lem  14711  repsdf2  14743  repswsymball  14744  repswrevw  14752  cshweqrep  14786  cshw1  14787  2cshwcshw  14791  scshwfzeqfzo  14792  cshwcsh2id  14794  swrdco  14803  swrd2lsw  14918  2swrd2eqwrdeq  14919  wwlktovfo  14924  cjre  15105  icodiamlt  15404  reusq0  15431  o1lo1  15503  o1of2  15579  o1rlimmul  15585  zsum  15684  modfsummods  15759  zprod  15903  reeff1  16088  dvdsmod0  16228  dvds2lem  16238  muldvds1  16250  dvdscmulr  16254  dvdsmulcr  16255  dvdsdivcl  16286  mod2eq1n2dvds  16317  oddnn02np1  16318  divalglem8  16370  ndvdsadd  16380  zeqzmulgcd  16480  dfgcd2  16516  absproddvds  16587  lcmftp  16606  coprmdvds  16623  2mulprm  16663  isprm5  16677  divgcdodd  16680  isprm6  16684  prmdvdsexpr  16687  prmdvdsbc  16696  cncongrprm  16699  phiprmpw  16746  modprm0  16776  pythagtriplem4  16790  pcz  16852  difsqpwdvds  16858  1arith  16898  prmgaplem5  17026  prmgaplem6  17027  cshwrepswhash1  17073  sbcie2s  17131  divsfval  17510  catsubcat  17801  fthmon  17891  isinitoi  17961  istermoi  17962  iszeroi  17971  setcmon  18049  setcepi  18050  funcestrcsetclem8  18108  fthestrcsetc  18111  funcsetcestrclem8  18123  fthsetcestrc  18126  odupos  18287  pltnle  18297  pltval3  18298  lublecllem  18319  latasym  18402  mrelatglb  18519  mrelatlub  18521  cnvpsb  18538  mgmpropd  18578  isgrpid2  18908  ghmghmrn  19167  ghmf1  19178  kerf1ghm  19179  orbsta  19245  resscntz  19265  gsmsymgrfixlem1  19357  gsmsymgreqlem2  19361  mndodcongi  19473  odf1  19492  lsmss1  19595  lsmss2  19597  efgredeu  19682  cntzcmnss  19771  imasabl  19806  lt6abl  19825  ablfaclem3  20019  ringinvnz1ne0  20209  0ringnnzr  20434  subrngringnsg  20462  srhmsubc  20589  domnmuln0  20618  lspsneq  21032  lspsneu  21033  lsmcv  21051  rnglidlmcl  21126  rngqiprngimf1lem  21204  lidldvgen  21244  domnchr  21442  znf1o  21461  zntoslem  21466  znfld  21470  cygznlem2a  21477  cygznlem3  21479  phlssphl  21568  islindf4  21747  uvcendim  21756  psdmul  22053  ply1scln0  22178  gsummoncoe1  22195  matvscl  22318  scmataddcl  22403  scmatsubcl  22404  scmatfo  22417  scmatghm  22420  maducoeval2  22527  slesolinv  22567  cramerimplem2  22571  cpmatelimp  22599  cpmatelimp2  22601  cpmatacl  22603  cpmatinvcl  22604  pm2mpf1  22686  cayhamlem1  22753  cayleyhamilton1  22779  0ntr  22958  islpi  23036  lmss  23185  cmpcld  23289  cmpfi  23295  1stcelcls  23348  comppfsc  23419  ptcnplem  23508  qtophmeo  23704  fbdmn0  23721  fbasrn  23771  elfm3  23837  fmfnfmlem4  23844  fclscf  23912  cnpfcf  23928  alexsubALTlem3  23936  tsmsres  24031  blval2  24450  tnggrpr  24543  nmoleub  24619  nmhmcn  25020  ncvs1  25057  iscau4  25179  caussi  25197  cmssmscld  25250  cmslssbn  25272  cniccbdd  25362  ovoliunnul  25408  mbfinf  25566  itg2splitlem  25649  dvcn  25823  c1lip1  25902  c1lip3  25904  dvcnvrelem1  25922  dvfsumlem2  25933  ply1divex  26042  quotcan  26217  aannenlem1  26236  taylf  26268  taylthlem2  26282  ulmcaulem  26303  ulmcau  26304  reeff1o  26357  logccv  26572  rtprmirr  26670  logreclem  26672  isosctrlem2  26729  xrlimcnp  26878  rlimcxp  26884  ftalem7  26989  vmappw  27026  fsumdvdsmul  27105  fsumvma  27124  dchreq  27169  dchrptlem1  27175  dchrsum  27180  bposlem7  27201  lgsqrlem2  27258  lgsdchr  27266  gausslemma2dlem1a  27276  lgseisenlem2  27287  lgsquad2  27297  2lgslem1b  27303  2sqlem6  27334  2sqnn0  27349  addsq2reu  27351  2sqreulem2  27363  sltval2  27568  sltres  27574  nodenselem8  27603  nodense  27604  noresle  27609  scutun12  27722  madeval2  27761  elmade  27779  negsf1o  27960  muls0ord  28088  recsex  28121  bdayon  28173  noseqrdgfn  28200  n0subs  28253  eln0zs  28288  tgcgrcomimp  28404  isperp2  28642  xmstrkgc  28813  brbtwn  28826  brcgr  28827  axcgrid  28843  axeuclidlem  28889  axeuclid  28890  elntg2  28912  lpvtx  28995  upgrex  29019  upgrpredgv  29066  upgredgpr  29069  uhgr0v0e  29165  subgrprop  29200  fusgrfisbase  29255  edgnbusgreu  29294  nbusgredgeu0  29295  cusgredg  29351  structtocusgr  29373  cusgrsize2inds  29381  cusgrsize  29382  usgredgsscusgredg  29387  fusgrmaxsize  29392  uspgrloopvtxel  29444  umgr2v2e  29453  vtxdginducedm1fi  29472  finsumvtxdg2sstep  29477  rgrprop  29488  rusgrprop  29490  0uhgrrusgr  29506  rusgrpropedg  29512  ewlkprop  29531  upgrewlkle2  29534  wlkprop  29539  upgrwlkcompim  29571  uspgr2wlkeq  29574  wlklenvclwlk  29583  wlkonprop  29586  wlkres  29598  redwlk  29600  wlkdlem2  29611  wksonproplem  29632  wksonproplemOLD  29633  usgr2trlspth  29691  usgr2pth  29694  pthdlem1  29696  crctcshwlkn0lem4  29743  wwlksnprcl  29769  wlkiswwlks2  29805  wwlksm1edg  29811  wlknewwlksn  29817  wwlksnred  29822  wwlksnextbi  29824  wwlksnextwrd  29827  wwlksnextinj  29829  wwlksnextsurj  29830  umgr2wlk  29879  umgrwwlks2on  29887  elwwlks2  29896  clwwlk1loop  29917  umgrclwwlkge2  29920  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlkfo  29938  clwwisshclwwslemlem  29942  clwwlknwwlksn  29967  clwwlknlbonbgr1  29968  clwwlkn1loopb  29972  clwwlkf  29976  clwwlknon1  30026  clwwlknonwwlknonb  30035  clwwlknonex2lem2  30037  vdn0conngrumgrv2  30125  frgrnbnb  30222  frgrncvvdeqlem2  30229  frgrncvvdeqlem3  30230  frgrncvvdeqlem6  30233  frgrwopreglem4a  30239  fusgr2wsp2nb  30263  frrusgrord0lem  30268  numclwwlk2lem1lem  30271  2clwwlk2clwwlklem  30275  2clwwlk2clwwlk  30279  numclwwlk1lem2foa  30283  numclwwlk1lem2f1  30286  frgrreg  30323  hlipgt0  30843  ocin  31225  ocnel  31227  shmodsi  31318  pjmf1  31645  unopf1o  31845  staddi  32175  stadd3i  32177  mdi  32224  dmdmd  32229  dmdi  32231  dmdbr2  32232  dmdbr3  32234  dmdbr4  32235  dmdi4  32236  mdsl1i  32250  superpos  32283  cvbr4i  32296  atssma  32307  atcv1  32309  atomli  32311  chirredlem1  32319  addltmulALT  32375  bian1dOLD  32386  ifeqeqx  32471  disjxpin  32517  suppss3  32647  fpwrelmap  32656  expgt0b  32741  mndlactfo  32968  mndractfo  32970  ogrpaddlt  33031  qsfld  33469  ply1degltdimlem  33618  ply1degltdim  33619  metider  33884  tpr2rico  33902  xrge0iifiso  33925  qqhcn  33981  qqhucn  33982  esumlub  34050  esumpinfval  34063  esumpinfsum  34067  ballotlemfc0  34484  ballotlemfcc  34485  ftc2re  34589  bnj517  34875  axsepg2  35072  axsepg2ALT  35073  fnrelpredd  35079  axnulg  35082  pfxwlk  35111  subgrwlk  35119  loop1cycl  35124  erdsze2lem2  35191  satfv1  35350  satfdmlem  35355  satf0op  35364  fmlasuc  35373  dfrdg4  35939  altopthsn  35949  btwncomim  36001  btwnexch3  36008  btwnexch2  36011  endofsegid  36073  opnrebl2  36309  nn0prpwlem  36310  onsuct0  36429  ordcmp  36435  nndivsub  36445  dnibndlem13  36478  bj-cbval  36637  bj-cbvex  36638  bj-cbvexw  36664  bj-cbv3tb  36775  bj-spimtv  36782  bj-equsal  36814  bj-sbsb  36825  bj-vtoclf  36903  bj-zfauscl  36912  bj-gabss  36923  bj-gabeqd  36925  currysetlem2  36936  bj-snsetex  36951  bj-ismooredr2  37098  bj-inftyexpiinj  37197  bj-finsumval0  37273  bj-fvimacnv0  37274  bj-bary1lem1  37299  bj-bary1  37300  f1omptsnlem  37324  iooelexlt  37350  relowlpssretop  37352  rdgeqoa  37358  finxpsuclem  37385  fvineqsneq  37400  pibt2  37405  wl-isseteq  37493  wl-equsal1i  37532  wl-ax11-lem10  37582  ltflcei  37602  sin2h  37604  cos2h  37605  tan2h  37606  lindsenlbs  37609  matunitlindf  37612  poimirlem3  37617  poimirlem4  37618  poimirlem18  37632  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  poimir  37647  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  mbfresfi  37660  cnambfre  37662  ftc1anc  37695  dvasin  37698  areacirclem1  37702  areacirclem4  37705  areacirc  37707  brabg2  37711  fzmul  37735  fdc  37739  incsequz2  37743  isbnd2  37777  opidonOLD  37846  opidon2OLD  37848  grpomndo  37869  elghomlem2OLD  37880  rngoueqz  37934  dvrunz  37948  divrngidl  38022  refressn  38434  dral1-o  38897  lsatn0  38992  l1cvpat  39047  leat2  39287  atnle  39310  cvlcvr1  39332  cvrexchlem  39413  cvratlem  39415  cvrat  39416  atcvrj0  39422  atle  39430  snatpsubN  39744  linepsubN  39746  pmapsub  39762  lneq2at  39772  lncvrelatN  39775  2llnma3r  39782  cdlemblem  39787  paddasslem5  39818  poml4N  39947  lhpmcvr4N  40020  trlval2  40157  cdlemd6  40197  cdleme7ga  40242  cdleme25b  40348  cdleme29b  40369  cdleme35fnpq  40443  cdleme50f1  40537  cdlemf1  40555  cdlemg27b  40690  cdlemk28-3  40902  tendospcanN  41017  diaf11N  41043  dia2dimlem1  41058  dibf11N  41155  dihf11  41261  dihmeetlem1N  41284  dochvalr  41351  dochnel2  41386  dvh4dimlem  41437  dochsat0  41451  mapd1o  41642  hdmapf1oN  41859  hgmapval0  41886  hgmapf1oN  41897  hlhilhillem  41954  nnproddivdvdsd  41988  lcmineqlem  42040  aks4d1p1p5  42063  aks4d1p3  42066  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  fldhmf1  42078  isprimroot2  42082  primrootsunit1  42085  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootlekpowne0  42093  primrootspoweq0  42094  aks6d1c1p1  42095  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c2p2  42107  aks6d1c2lem3  42114  aks6d1c2lem4  42115  hashnexinj  42116  hashnexinjle  42117  aks6d1c2  42118  aks6d1c5lem0  42123  aks6d1c5lem1  42124  aks6d1c5  42127  sticksstones1  42134  sticksstones3  42136  sticksstones8  42141  sticksstones11  42144  sticksstones12  42146  sticksstones20  42154  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  aks6d1c7  42172  rhmqusspan  42173  unitscyglem2  42184  unitscyglem3  42185  aks5lem8  42189  sn-axprlem3  42205  oexpreposd  42310  sn-remul0ord  42396  frlmsnic  42528  fsuppind  42578  prjspval  42591  rexrabdioph  42782  fphpdo  42805  irrapxlem3  42812  rmxypairf1o  42900  rmxycomplete  42906  zindbi  42935  lermxnn0  42939  ltrmy  42941  rmyeq0  42942  rmyeq  42943  lermy  42944  acongsym  42965  acongneg2  42966  wepwsolem  43031  onsupuni  43218  onsupmaxb  43228  onsucf1o  43261  onov0suclim  43263  oe0suclim  43266  onsucwordi  43277  cantnfresb  43313  omabs2  43321  tfsconcat0b  43335  tfsconcatrev  43337  naddcnffo  43353  oaun3lem1  43363  oaltom  43394  omltoe  43396  sdomne0  43402  sdomne0d  43403  safesnsupfidom1o  43406  intabssd  43508  iscard4  43522  ss2iundf  43648  frege129d  43752  frege133d  43754  axfrege52a  43845  axfrege52c  43876  ntrk0kbimka  44028  gneispace  44123  suprleubrd  44155  suprlubrd  44157  radcnvrat  44303  nzss  44306  expgrowthi  44322  ordpss  44440  bi23impib  44476  rspsbc2  44524  tratrb  44526  sbcim2g  44528  truniALT  44531  3impcombi  44806  tpid3gVD  44831  orbi1rVD  44837  sbc3orgVD  44840  rspsbc2VD  44844  tratrbVD  44850  sbcim2gVD  44864  sbcbiVD  44865  truniALTVD  44867  trintALTVD  44869  trintALT  44870  csbingVD  44873  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  relopabVD  44890  isosctrlem1ALT  44923  relpfrlem  44943  trfr  44952  fzisoeu  45298  xrralrecnnge  45386  allbutfi  45389  climinf  45604  liminfreuzlem  45800  climliminf  45804  climliminflimsup  45806  xlimpnfxnegmnf  45812  xlimbr  45825  stoweidlem7  46005  stoweidlem62  46060  sge0gerpmpt  46400  meaiuninclem  46478  carageniuncllem2  46520  issmflem  46725  et-sqrtnegnre  46871  ormkglobd  46873  natlocalincr  46874  tworepnotupword  46884  funressnfv  47044  funressnvmo  47046  f1cof1b  47078  2reu3  47111  ralbinrald  47123  afv0fv0  47150  afv0nbfvbi  47152  afvfv0bi  47153  fnbrafvb  47155  afvres  47173  tz6.12-afv  47174  afvco2  47177  ndmaovcl  47204  afv2res  47240  tz6.12-afv2  47241  nelbrim  47276  f1oresf1o2  47292  zm1nn  47303  nltle2tri  47314  subsubelfzo0  47327  2tceilhalfelfzo1  47333  iccpartres  47419  iccpartiltu  47423  fargshiftfv  47440  ichnreuop  47473  ichreuopeq  47474  prsprel  47488  sprsymrelf1lem  47492  sprsymrelfolem2  47494  sprsymrelfo  47498  prpair  47502  paireqne  47512  sbcpr  47522  fmtnof1  47536  goldbachthlem2  47547  fmtnoprmfac1  47566  fmtnoprmfac2  47568  lighneallem2  47607  lighneallem4b  47610  lighneallem4  47611  evennodd  47644  oddneven  47645  oexpnegnz  47679  evenltle  47718  fpprwppr  47740  fpprwpprb  47741  gbowge7  47764  gbege6  47766  sbgoldbwt  47778  sbgoldbst  47779  nnsum3primesle9  47795  bgoldbtbndlem2  47807  grimprop  47883  isuspgrimlem  47895  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  grtriproplem  47938  isgrtri  47942  grimgrtri  47948  stgr1  47960  isubgr3stgr  47974  grlimprop  47983  uspgrlimlem2  47988  uspgrlimlem3  47989  gpg5nbgrvtx13starlem1  48062  clintop  48196  isassintop  48198  lidldomn1  48219  uzlidlring  48223  2zrngnmlid2  48245  rngccatidALTV  48260  ringccatidALTV  48294  srhmsubcALTV  48313  ztprmneprm  48335  pgrpgt2nabl  48354  lindslinindimp2lem4  48450  lincresunit3  48470  fldivexpfllog2  48554  digexp  48596  naryfvalelfv  48621  affinecomb1  48691  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  eenglngeehlnm  48728  itscnhlc0yqe  48748  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  itsclquadeu  48766  inlinecirc02plem  48775  inlinecirc02p  48776  pm4.71da  48778  mofsn  48832  seposep  48914  resipos  48963  idmon  49009  idepi  49010  prsthinc  49453  grptcmon  49582  grptcepi  49583  spd  49667  spcdvw  49668  setrec2fun  49681