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  1996  spfw  2032  cbvalw  2034  sbequi  2084  chvarfv  2240  cbvalv1  2342  spv  2397  chvar  2399  cbval  2402  sb1  2482  nfsb4t  2503  exmoeu  2580  euim  2616  2eu3  2653  eqrdav  2734  ralbida  3253  rgen2a  3350  ralcom2  3356  ceqsalt  3494  ceqsalgALT  3497  spcimgft  3525  vtoclfOLD  3544  vtoclegft  3567  spcdv  3573  rspcdv  3593  rspcebdv  3595  rexraleqim  3626  sbcn1  3818  sbcbi1  3823  sbeqalb  3828  sbcel21v  3833  disj  4425  elpwunsn  4660  rabsnifsb  4698  ssunsn2  4803  preqr1g  4828  iuneqconst  4979  axprlem3  5395  axprlem3OLD  5398  sbcop1  5463  propeqop  5482  euotd  5488  rexopabb  5503  sotr2  5595  relop  5830  elinxp  6006  elimasni  6078  sotri2  6118  onmindif  6445  iotavalOLD  6504  dffv2  6973  mpteqb  7004  elfvmptrab  7014  chfnrn  7038  elpreima  7047  iinpreima  7058  exfo  7094  ffnfv  7108  f1elima  7255  f1ounsn  7264  f1eqcocnv  7293  fliftfun  7304  soisores  7319  isotr  7328  isomin  7329  ovmpodv2  7563  difsnexi  7753  onint  7782  oneqmin  7792  ordunisuc2  7837  tfindsg  7854  findsg  7891  resf1extb  7928  f1oweALT  7969  el2mpocl  8083  poseq  8155  soseq  8156  ressuppss  8180  funsssuppss  8187  suppofssd  8200  smoiso  8374  seqomlem2  8463  oaordi  8556  oawordri  8560  oaordex  8568  oalimcl  8570  omwordi  8581  oewordi  8601  oelim2  8605  nnmwordi  8645  xpider  8800  iiner  8801  undifixp  8946  mptelixpg  8947  dom2lem  9004  findcard2s  9177  pssnn  9180  nneneq  9218  fineqvlem  9268  dif1ennnALT  9281  unfilem2  9314  xpfiOLD  9329  domunfican  9331  f1dmvrnfibi  9351  fsuppimp  9378  dffi2  9433  infsupprpr  9516  wemaplem2  9559  suc11reg  9631  noinfep  9672  cantnflem1  9701  r1fin  9785  tcrank  9896  cardlim  9984  pr2nelemOLD  10015  fseqenlem1  10036  alephnbtwn  10083  alephord2i  10089  alephf1  10097  cardaleph  10101  alephiso  10110  dfac12lem2  10157  ackbij1lem16  10246  cflm  10262  cfcoflem  10284  sornom  10289  fin23lem27  10340  isf32lem7  10371  fin17  10406  fin1a2lem2  10413  fin1a2lem4  10415  fin1a2lem6  10417  fin1a2lem9  10420  axdc3lem2  10463  zorn2lem7  10514  uniimadom  10556  inar1  10787  grothomex  10841  addcanpi  10911  mulcanpi  10912  enqer  10933  genpcd  11018  genpnmax  11019  ltexprlem4  11051  reclem3pr  11061  reclem4pr  11062  suplem2pr  11065  axpre-ltadd  11179  axpre-sup  11181  ltletr  11325  00id  11408  addn0nid  11655  mul0or  11875  prodgt02  12087  lemul1a  12093  mulgt1OLD  12098  divgt0  12108  divge0  12109  ledivp1i  12165  ltdivp1i  12166  cju  12234  nnsub  12282  nominpos  12476  nn0n0n1ge2  12567  btwnnz  12667  suprfinzcl  12705  ublbneg  12947  zmax  12959  cnref1o  12999  ltsubrp  13043  ltaddrp  13044  xrltletr  13171  qbtwnre  13213  xltnegi  13230  xnn0xadd0  13261  iccsupr  13457  icoshft  13488  difreicc  13499  iccshftri  13502  iccshftli  13504  iccdili  13506  icccntri  13508  fzen  13556  elfz1b  13608  fzofzim  13724  eluzgtdifelfzo  13741  elfzo1elm1fzo0  13782  injresinjlem  13801  injresinj  13802  flval2  13829  flval3  13830  modmuladdim  13930  modaddmodup  13950  addmodlteq  13962  fseqsupubi  13994  ssnn0fi  14001  mptnn0fsuppr  14015  sq01  14241  hashf1rn  14368  hashgt12el  14438  hashgt12el2  14439  hashfundm  14458  hash2pr  14485  hash2exprb  14487  hashge2el2difr  14497  hashtpg  14501  hash3tr  14507  lswlgt0cl  14585  ccatalpha  14609  pfxfv  14698  pfxsuff1eqwrdeq  14715  ccatopth2  14733  swrdccat  14751  swrdccat3blem  14755  reuccatpfxs1lem  14762  repsdf2  14794  repswsymball  14795  repswrevw  14803  cshweqrep  14837  cshw1  14838  2cshwcshw  14842  scshwfzeqfzo  14843  cshwcsh2id  14845  swrdco  14854  swrd2lsw  14969  2swrd2eqwrdeq  14970  wwlktovfo  14975  cjre  15156  icodiamlt  15452  reusq0  15479  o1lo1  15551  o1of2  15627  o1rlimmul  15633  zsum  15732  modfsummods  15807  zprod  15951  reeff1  16136  dvdsmod0  16276  dvds2lem  16286  muldvds1  16298  dvdscmulr  16302  dvdsmulcr  16303  dvdsdivcl  16333  mod2eq1n2dvds  16364  oddnn02np1  16365  divalglem8  16417  ndvdsadd  16427  zeqzmulgcd  16527  dfgcd2  16563  absproddvds  16634  lcmftp  16653  coprmdvds  16670  2mulprm  16710  isprm5  16724  divgcdodd  16727  isprm6  16731  prmdvdsexpr  16734  prmdvdsbc  16743  cncongrprm  16746  phiprmpw  16793  modprm0  16823  pythagtriplem4  16837  pcz  16899  difsqpwdvds  16905  1arith  16945  prmgaplem5  17073  prmgaplem6  17074  cshwrepswhash1  17120  sbcie2s  17178  divsfval  17559  catsubcat  17850  fthmon  17940  isinitoi  18010  istermoi  18011  iszeroi  18020  setcmon  18098  setcepi  18099  funcestrcsetclem8  18157  fthestrcsetc  18160  funcsetcestrclem8  18172  fthsetcestrc  18175  odupos  18336  pltnle  18346  pltval3  18347  lublecllem  18368  latasym  18451  mrelatglb  18568  mrelatlub  18570  cnvpsb  18587  mgmpropd  18627  isgrpid2  18957  ghmghmrn  19216  ghmf1  19227  kerf1ghm  19228  orbsta  19294  resscntz  19314  gsmsymgrfixlem1  19406  gsmsymgreqlem2  19410  mndodcongi  19522  odf1  19541  lsmss1  19644  lsmss2  19646  efgredeu  19731  cntzcmnss  19820  imasabl  19855  lt6abl  19874  ablfaclem3  20068  ringinvnz1ne0  20258  0ringnnzr  20483  subrngringnsg  20511  srhmsubc  20638  domnmuln0  20667  lspsneq  21081  lspsneu  21082  lsmcv  21100  rnglidlmcl  21175  rngqiprngimf1lem  21253  lidldvgen  21293  domnchr  21491  znf1o  21510  zntoslem  21515  znfld  21519  cygznlem2a  21526  cygznlem3  21528  phlssphl  21617  islindf4  21796  uvcendim  21805  psdmul  22102  ply1scln0  22227  gsummoncoe1  22244  matvscl  22367  scmataddcl  22452  scmatsubcl  22453  scmatfo  22466  scmatghm  22469  maducoeval2  22576  slesolinv  22616  cramerimplem2  22620  cpmatelimp  22648  cpmatelimp2  22650  cpmatacl  22652  cpmatinvcl  22653  pm2mpf1  22735  cayhamlem1  22802  cayleyhamilton1  22828  0ntr  23007  islpi  23085  lmss  23234  cmpcld  23338  cmpfi  23344  1stcelcls  23397  comppfsc  23468  ptcnplem  23557  qtophmeo  23753  fbdmn0  23770  fbasrn  23820  elfm3  23886  fmfnfmlem4  23893  fclscf  23961  cnpfcf  23977  alexsubALTlem3  23985  tsmsres  24080  blval2  24499  tnggrpr  24592  nmoleub  24668  nmhmcn  25069  ncvs1  25107  iscau4  25229  caussi  25247  cmssmscld  25300  cmslssbn  25322  cniccbdd  25412  ovoliunnul  25458  mbfinf  25616  itg2splitlem  25699  dvcn  25873  c1lip1  25952  c1lip3  25954  dvcnvrelem1  25972  dvfsumlem2  25983  ply1divex  26092  quotcan  26267  aannenlem1  26286  taylf  26318  taylthlem2  26332  ulmcaulem  26353  ulmcau  26354  reeff1o  26407  logccv  26622  rtprmirr  26720  logreclem  26722  isosctrlem2  26779  xrlimcnp  26928  rlimcxp  26934  ftalem7  27039  vmappw  27076  fsumdvdsmul  27155  fsumvma  27174  dchreq  27219  dchrptlem1  27225  dchrsum  27230  bposlem7  27251  lgsqrlem2  27308  lgsdchr  27316  gausslemma2dlem1a  27326  lgseisenlem2  27337  lgsquad2  27347  2lgslem1b  27353  2sqlem6  27384  2sqnn0  27399  addsq2reu  27401  2sqreulem2  27413  sltval2  27618  sltres  27624  nodenselem8  27653  nodense  27654  noresle  27659  scutun12  27772  madeval2  27809  elmade  27823  negsf1o  28003  muls0ord  28128  recsex  28160  noseqrdgfn  28229  n0subs  28277  eln0zs  28303  tgcgrcomimp  28402  isperp2  28640  xmstrkgc  28811  brbtwn  28824  brcgr  28825  axcgrid  28841  axeuclidlem  28887  axeuclid  28888  elntg2  28910  lpvtx  28993  upgrex  29017  upgrpredgv  29064  upgredgpr  29067  uhgr0v0e  29163  subgrprop  29198  fusgrfisbase  29253  edgnbusgreu  29292  nbusgredgeu0  29293  cusgredg  29349  structtocusgr  29371  cusgrsize2inds  29379  cusgrsize  29380  usgredgsscusgredg  29385  fusgrmaxsize  29390  uspgrloopvtxel  29442  umgr2v2e  29451  vtxdginducedm1fi  29470  finsumvtxdg2sstep  29475  rgrprop  29486  rusgrprop  29488  0uhgrrusgr  29504  rusgrpropedg  29510  ewlkprop  29529  upgrewlkle2  29532  wlkprop  29537  upgrwlkcompim  29569  uspgr2wlkeq  29572  wlklenvclwlk  29581  wlkonprop  29584  wlkres  29596  redwlk  29598  wlkdlem2  29609  wksonproplem  29630  wksonproplemOLD  29631  usgr2trlspth  29689  usgr2pth  29692  pthdlem1  29694  crctcshwlkn0lem4  29741  wwlksnprcl  29767  wlkiswwlks2  29803  wwlksm1edg  29809  wlknewwlksn  29815  wwlksnred  29820  wwlksnextbi  29822  wwlksnextwrd  29825  wwlksnextinj  29827  wwlksnextsurj  29828  umgr2wlk  29877  umgrwwlks2on  29885  elwwlks2  29894  clwwlk1loop  29915  umgrclwwlkge2  29918  clwlkclwwlklem2a1  29919  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlkfo  29936  clwwisshclwwslemlem  29940  clwwlknwwlksn  29965  clwwlknlbonbgr1  29966  clwwlkn1loopb  29970  clwwlkf  29974  clwwlknon1  30024  clwwlknonwwlknonb  30033  clwwlknonex2lem2  30035  vdn0conngrumgrv2  30123  frgrnbnb  30220  frgrncvvdeqlem2  30227  frgrncvvdeqlem3  30228  frgrncvvdeqlem6  30231  frgrwopreglem4a  30237  fusgr2wsp2nb  30261  frrusgrord0lem  30266  numclwwlk2lem1lem  30269  2clwwlk2clwwlklem  30273  2clwwlk2clwwlk  30277  numclwwlk1lem2foa  30281  numclwwlk1lem2f1  30284  frgrreg  30321  hlipgt0  30841  ocin  31223  ocnel  31225  shmodsi  31316  pjmf1  31643  unopf1o  31843  staddi  32173  stadd3i  32175  mdi  32222  dmdmd  32227  dmdi  32229  dmdbr2  32230  dmdbr3  32232  dmdbr4  32233  dmdi4  32234  mdsl1i  32248  superpos  32281  cvbr4i  32294  atssma  32305  atcv1  32307  atomli  32309  chirredlem1  32317  addltmulALT  32373  bian1dOLD  32384  ifeqeqx  32469  disjxpin  32515  suppss3  32647  fpwrelmap  32656  expgt0b  32741  mndlactfo  32968  mndractfo  32970  ogrpaddlt  33031  qsfld  33459  ply1degltdimlem  33608  ply1degltdim  33609  metider  33871  tpr2rico  33889  xrge0iifiso  33912  qqhcn  33968  qqhucn  33969  esumlub  34037  esumpinfval  34050  esumpinfsum  34054  ballotlemfc0  34471  ballotlemfcc  34472  ftc2re  34576  bnj517  34862  axsepg2  35059  axsepg2ALT  35060  fnrelpredd  35066  axnulg  35069  pfxwlk  35092  subgrwlk  35100  loop1cycl  35105  erdsze2lem2  35172  satfv1  35331  satfdmlem  35336  satf0op  35345  fmlasuc  35354  dfrdg4  35915  altopthsn  35925  btwncomim  35977  btwnexch3  35984  btwnexch2  35987  endofsegid  36049  opnrebl2  36285  nn0prpwlem  36286  onsuct0  36405  ordcmp  36411  nndivsub  36421  dnibndlem13  36454  bj-cbval  36613  bj-cbvex  36614  bj-cbvexw  36640  bj-cbv3tb  36751  bj-spimtv  36758  bj-equsal  36790  bj-sbsb  36801  bj-vtoclf  36879  bj-zfauscl  36888  bj-gabss  36899  bj-gabeqd  36901  currysetlem2  36912  bj-snsetex  36927  bj-ismooredr2  37074  bj-inftyexpiinj  37173  bj-finsumval0  37249  bj-fvimacnv0  37250  bj-bary1lem1  37275  bj-bary1  37276  f1omptsnlem  37300  iooelexlt  37326  relowlpssretop  37328  rdgeqoa  37334  finxpsuclem  37361  fvineqsneq  37376  pibt2  37381  wl-isseteq  37469  wl-equsal1i  37508  wl-ax11-lem10  37558  ltflcei  37578  sin2h  37580  cos2h  37581  tan2h  37582  lindsenlbs  37585  matunitlindf  37588  poimirlem3  37593  poimirlem4  37594  poimirlem18  37608  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem31  37621  poimir  37623  heicant  37625  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  mbfresfi  37636  cnambfre  37638  ftc1anc  37671  dvasin  37674  areacirclem1  37678  areacirclem4  37681  areacirc  37683  brabg2  37687  fzmul  37711  fdc  37715  incsequz2  37719  isbnd2  37753  opidonOLD  37822  opidon2OLD  37824  grpomndo  37845  elghomlem2OLD  37856  rngoueqz  37910  dvrunz  37924  divrngidl  37998  refressn  38407  dral1-o  38868  lsatn0  38963  l1cvpat  39018  leat2  39258  atnle  39281  cvlcvr1  39303  cvrexchlem  39384  cvratlem  39386  cvrat  39387  atcvrj0  39393  atle  39401  snatpsubN  39715  linepsubN  39717  pmapsub  39733  lneq2at  39743  lncvrelatN  39746  2llnma3r  39753  cdlemblem  39758  paddasslem5  39789  poml4N  39918  lhpmcvr4N  39991  trlval2  40128  cdlemd6  40168  cdleme7ga  40213  cdleme25b  40319  cdleme29b  40340  cdleme35fnpq  40414  cdleme50f1  40508  cdlemf1  40526  cdlemg27b  40661  cdlemk28-3  40873  tendospcanN  40988  diaf11N  41014  dia2dimlem1  41029  dibf11N  41126  dihf11  41232  dihmeetlem1N  41255  dochvalr  41322  dochnel2  41357  dvh4dimlem  41408  dochsat0  41422  mapd1o  41613  hdmapf1oN  41830  hgmapval0  41857  hgmapf1oN  41868  hlhilhillem  41925  nnproddivdvdsd  41959  lcmineqlem  42011  aks4d1p1p5  42034  aks4d1p3  42037  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1p9  42047  fldhmf1  42049  isprimroot2  42053  primrootsunit1  42056  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootlekpowne0  42064  primrootspoweq0  42065  aks6d1c1p1  42066  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c2p2  42078  aks6d1c2lem3  42085  aks6d1c2lem4  42086  hashnexinj  42087  hashnexinjle  42088  aks6d1c2  42089  aks6d1c5lem0  42094  aks6d1c5lem1  42095  aks6d1c5  42098  sticksstones1  42105  sticksstones3  42107  sticksstones8  42112  sticksstones11  42115  sticksstones12  42117  sticksstones20  42125  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  aks6d1c7  42143  rhmqusspan  42144  unitscyglem2  42155  unitscyglem3  42156  aks5lem8  42160  metakunt7  42170  sn-axprlem3  42214  oexpreposd  42318  frlmsnic  42510  fsuppind  42560  prjspval  42573  rexrabdioph  42764  fphpdo  42787  irrapxlem3  42794  rmxypairf1o  42882  rmxycomplete  42888  zindbi  42917  lermxnn0  42921  ltrmy  42923  rmyeq0  42924  rmyeq  42925  lermy  42926  acongsym  42947  acongneg2  42948  wepwsolem  43013  onsupuni  43200  onsupmaxb  43210  onsucf1o  43243  onov0suclim  43245  oe0suclim  43248  onsucwordi  43259  cantnfresb  43295  omabs2  43303  tfsconcat0b  43317  tfsconcatrev  43319  naddcnffo  43335  oaun3lem1  43345  oaltom  43376  omltoe  43378  sdomne0  43384  sdomne0d  43385  safesnsupfidom1o  43388  intabssd  43490  iscard4  43504  ss2iundf  43630  frege129d  43734  frege133d  43736  axfrege52a  43827  axfrege52c  43858  ntrk0kbimka  44010  gneispace  44105  suprleubrd  44137  suprlubrd  44139  radcnvrat  44286  nzss  44289  expgrowthi  44305  ordpss  44423  bi23impib  44459  rspsbc2  44507  tratrb  44509  sbcim2g  44511  truniALT  44514  3impcombi  44789  tpid3gVD  44814  orbi1rVD  44820  sbc3orgVD  44823  rspsbc2VD  44827  tratrbVD  44833  sbcim2gVD  44847  sbcbiVD  44848  truniALTVD  44850  trintALTVD  44852  trintALT  44853  csbingVD  44856  csbsngVD  44865  csbxpgVD  44866  csbresgVD  44867  csbrngVD  44868  csbima12gALTVD  44869  csbunigVD  44870  csbfv12gALTVD  44871  relopabVD  44873  isosctrlem1ALT  44906  relpfrlem  44926  trfr  44935  fzisoeu  45277  xrralrecnnge  45365  allbutfi  45368  climinf  45583  liminfreuzlem  45779  climliminf  45783  climliminflimsup  45785  xlimpnfxnegmnf  45791  xlimbr  45804  stoweidlem7  45984  stoweidlem62  46039  sge0gerpmpt  46379  meaiuninclem  46457  carageniuncllem2  46499  issmflem  46704  et-sqrtnegnre  46850  ormkglobd  46852  natlocalincr  46853  tworepnotupword  46863  funressnfv  47020  funressnvmo  47022  f1cof1b  47054  2reu3  47087  ralbinrald  47099  afv0fv0  47126  afv0nbfvbi  47128  afvfv0bi  47129  fnbrafvb  47131  afvres  47149  tz6.12-afv  47150  afvco2  47153  ndmaovcl  47180  afv2res  47216  tz6.12-afv2  47217  nelbrim  47252  f1oresf1o2  47268  zm1nn  47279  nltle2tri  47290  subsubelfzo0  47303  2tceilhalfelfzo1  47309  iccpartres  47380  iccpartiltu  47384  fargshiftfv  47401  ichnreuop  47434  ichreuopeq  47435  prsprel  47449  sprsymrelf1lem  47453  sprsymrelfolem2  47455  sprsymrelfo  47459  prpair  47463  paireqne  47473  sbcpr  47483  fmtnof1  47497  goldbachthlem2  47508  fmtnoprmfac1  47527  fmtnoprmfac2  47529  lighneallem2  47568  lighneallem4b  47571  lighneallem4  47572  evennodd  47605  oddneven  47606  oexpnegnz  47640  evenltle  47679  fpprwppr  47701  fpprwpprb  47702  gbowge7  47725  gbege6  47727  sbgoldbwt  47739  sbgoldbst  47740  nnsum3primesle9  47756  bgoldbtbndlem2  47768  grimprop  47844  isuspgrimlem  47856  uhgrimisgrgriclem  47891  clnbgrgrimlem  47894  grtriproplem  47899  isgrtri  47903  grimgrtri  47909  stgr1  47921  isubgr3stgr  47935  grlimprop  47944  uspgrlimlem2  47949  uspgrlimlem3  47950  gpg5nbgrvtx13starlem1  48021  clintop  48131  isassintop  48133  lidldomn1  48154  uzlidlring  48158  2zrngnmlid2  48180  rngccatidALTV  48195  ringccatidALTV  48229  srhmsubcALTV  48248  ztprmneprm  48270  pgrpgt2nabl  48289  lindslinindimp2lem4  48385  lincresunit3  48405  fldivexpfllog2  48493  digexp  48535  naryfvalelfv  48560  affinecomb1  48630  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  eenglngeehlnm  48667  itscnhlc0yqe  48687  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itschlc0xyqsol  48695  itsclquadeu  48705  inlinecirc02plem  48714  inlinecirc02p  48715  pm4.71da  48717  mofsn  48770  seposep  48848  resipos  48897  idmon  48943  idepi  48944  prsthinc  49298  grptcmon  49418  grptcepi  49419  spd  49490  spcdvw  49491  setrec2fun  49504