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  3246  rgen2a  3342  ralcom2  3348  ceqsalt  3478  ceqsalgALT  3481  spcimgft  3509  vtoclfOLD  3528  vtoclegft  3551  spcdv  3557  rspcdv  3577  rspcebdv  3579  rexraleqim  3610  sbcn1  3803  sbcbi1  3808  sbeqalb  3813  sbcel21v  3818  disj  4409  elpwunsn  4644  rabsnifsb  4682  ssunsn2  4787  preqr1g  4812  iuneqconst  4963  axprlem3  5375  axprlem3OLD  5378  sbcop1  5443  propeqop  5462  euotd  5468  rexopabb  5483  sotr2  5573  relop  5804  elinxp  5979  elimasni  6051  sotri2  6090  onmindif  6414  iotavalOLD  6473  dffv2  6938  mpteqb  6969  elfvmptrab  6979  chfnrn  7003  elpreima  7012  iinpreima  7023  exfo  7059  ffnfv  7073  f1elima  7220  f1ounsn  7229  f1eqcocnv  7258  fliftfun  7269  soisores  7284  isotr  7293  isomin  7294  ovmpodv2  7527  difsnexi  7717  onint  7746  oneqmin  7756  ordunisuc2  7800  tfindsg  7817  findsg  7853  resf1extb  7890  f1oweALT  7930  el2mpocl  8042  poseq  8114  soseq  8115  ressuppss  8139  funsssuppss  8146  suppofssd  8159  smoiso  8308  seqomlem2  8396  oaordi  8487  oawordri  8491  oaordex  8499  oalimcl  8501  omwordi  8512  oewordi  8532  oelim2  8536  nnmwordi  8576  xpider  8738  iiner  8739  undifixp  8884  mptelixpg  8885  dom2lem  8940  findcard2s  9106  pssnn  9109  nneneq  9147  fineqvlem  9185  dif1ennnALT  9198  unfilem2  9231  xpfiOLD  9246  domunfican  9248  f1dmvrnfibi  9268  fsuppimp  9295  dffi2  9350  infsupprpr  9433  wemaplem2  9476  suc11reg  9548  noinfep  9589  cantnflem1  9618  r1fin  9702  tcrank  9813  cardlim  9901  pr2nelemOLD  9932  fseqenlem1  9953  alephnbtwn  10000  alephord2i  10006  alephf1  10014  cardaleph  10018  alephiso  10027  dfac12lem2  10074  ackbij1lem16  10163  cflm  10179  cfcoflem  10201  sornom  10206  fin23lem27  10257  isf32lem7  10288  fin17  10323  fin1a2lem2  10330  fin1a2lem4  10332  fin1a2lem6  10334  fin1a2lem9  10337  axdc3lem2  10380  zorn2lem7  10431  uniimadom  10473  inar1  10704  grothomex  10758  addcanpi  10828  mulcanpi  10829  enqer  10850  genpcd  10935  genpnmax  10936  ltexprlem4  10968  reclem3pr  10978  reclem4pr  10979  suplem2pr  10982  axpre-ltadd  11096  axpre-sup  11098  ltletr  11242  00id  11325  addn0nid  11574  mul0or  11794  prodgt02  12006  lemul1a  12012  mulgt1OLD  12017  divgt0  12027  divge0  12028  ledivp1i  12084  ltdivp1i  12085  cju  12158  nnsub  12206  nominpos  12395  nn0n0n1ge2  12486  btwnnz  12586  suprfinzcl  12624  ublbneg  12868  zmax  12880  cnref1o  12920  ltsubrp  12965  ltaddrp  12966  xrltletr  13093  qbtwnre  13135  xltnegi  13152  xnn0xadd0  13183  iccsupr  13379  icoshft  13410  difreicc  13421  iccshftri  13424  iccshftli  13426  iccdili  13428  icccntri  13430  fzen  13478  elfz1b  13530  fzofzim  13646  eluzgtdifelfzo  13664  elfzo1elm1fzo0  13705  injresinjlem  13724  injresinj  13725  flval2  13752  flval3  13753  modmuladdim  13855  modaddmodup  13875  addmodlteq  13887  fseqsupubi  13919  ssnn0fi  13926  mptnn0fsuppr  13940  sq01  14166  hashf1rn  14293  hashgt12el  14363  hashgt12el2  14364  hashfundm  14383  hash2pr  14410  hash2exprb  14412  hashge2el2difr  14422  hashtpg  14426  hash3tr  14432  lswlgt0cl  14510  ccatalpha  14534  pfxfv  14623  pfxsuff1eqwrdeq  14640  ccatopth2  14658  swrdccat  14676  swrdccat3blem  14680  reuccatpfxs1lem  14687  repsdf2  14719  repswsymball  14720  repswrevw  14728  cshweqrep  14762  cshw1  14763  2cshwcshw  14767  scshwfzeqfzo  14768  cshwcsh2id  14770  swrdco  14779  swrd2lsw  14894  2swrd2eqwrdeq  14895  wwlktovfo  14900  cjre  15081  icodiamlt  15380  reusq0  15407  o1lo1  15479  o1of2  15555  o1rlimmul  15561  zsum  15660  modfsummods  15735  zprod  15879  reeff1  16064  dvdsmod0  16204  dvds2lem  16214  muldvds1  16226  dvdscmulr  16230  dvdsmulcr  16231  dvdsdivcl  16262  mod2eq1n2dvds  16293  oddnn02np1  16294  divalglem8  16346  ndvdsadd  16356  zeqzmulgcd  16456  dfgcd2  16492  absproddvds  16563  lcmftp  16582  coprmdvds  16599  2mulprm  16639  isprm5  16653  divgcdodd  16656  isprm6  16660  prmdvdsexpr  16663  prmdvdsbc  16672  cncongrprm  16675  phiprmpw  16722  modprm0  16752  pythagtriplem4  16766  pcz  16828  difsqpwdvds  16834  1arith  16874  prmgaplem5  17002  prmgaplem6  17003  cshwrepswhash1  17049  sbcie2s  17107  divsfval  17486  catsubcat  17777  fthmon  17867  isinitoi  17937  istermoi  17938  iszeroi  17947  setcmon  18025  setcepi  18026  funcestrcsetclem8  18084  fthestrcsetc  18087  funcsetcestrclem8  18099  fthsetcestrc  18102  odupos  18263  pltnle  18273  pltval3  18274  lublecllem  18295  latasym  18378  mrelatglb  18495  mrelatlub  18497  cnvpsb  18514  mgmpropd  18554  isgrpid2  18884  ghmghmrn  19143  ghmf1  19154  kerf1ghm  19155  orbsta  19221  resscntz  19241  gsmsymgrfixlem1  19333  gsmsymgreqlem2  19337  mndodcongi  19449  odf1  19468  lsmss1  19571  lsmss2  19573  efgredeu  19658  cntzcmnss  19747  imasabl  19782  lt6abl  19801  ablfaclem3  19995  ringinvnz1ne0  20185  0ringnnzr  20410  subrngringnsg  20438  srhmsubc  20565  domnmuln0  20594  lspsneq  21008  lspsneu  21009  lsmcv  21027  rnglidlmcl  21102  rngqiprngimf1lem  21180  lidldvgen  21220  domnchr  21418  znf1o  21437  zntoslem  21442  znfld  21446  cygznlem2a  21453  cygznlem3  21455  phlssphl  21544  islindf4  21723  uvcendim  21732  psdmul  22029  ply1scln0  22154  gsummoncoe1  22171  matvscl  22294  scmataddcl  22379  scmatsubcl  22380  scmatfo  22393  scmatghm  22396  maducoeval2  22503  slesolinv  22543  cramerimplem2  22547  cpmatelimp  22575  cpmatelimp2  22577  cpmatacl  22579  cpmatinvcl  22580  pm2mpf1  22662  cayhamlem1  22729  cayleyhamilton1  22755  0ntr  22934  islpi  23012  lmss  23161  cmpcld  23265  cmpfi  23271  1stcelcls  23324  comppfsc  23395  ptcnplem  23484  qtophmeo  23680  fbdmn0  23697  fbasrn  23747  elfm3  23813  fmfnfmlem4  23820  fclscf  23888  cnpfcf  23904  alexsubALTlem3  23912  tsmsres  24007  blval2  24426  tnggrpr  24519  nmoleub  24595  nmhmcn  24996  ncvs1  25033  iscau4  25155  caussi  25173  cmssmscld  25226  cmslssbn  25248  cniccbdd  25338  ovoliunnul  25384  mbfinf  25542  itg2splitlem  25625  dvcn  25799  c1lip1  25878  c1lip3  25880  dvcnvrelem1  25898  dvfsumlem2  25909  ply1divex  26018  quotcan  26193  aannenlem1  26212  taylf  26244  taylthlem2  26258  ulmcaulem  26279  ulmcau  26280  reeff1o  26333  logccv  26548  rtprmirr  26646  logreclem  26648  isosctrlem2  26705  xrlimcnp  26854  rlimcxp  26860  ftalem7  26965  vmappw  27002  fsumdvdsmul  27081  fsumvma  27100  dchreq  27145  dchrptlem1  27151  dchrsum  27156  bposlem7  27177  lgsqrlem2  27234  lgsdchr  27242  gausslemma2dlem1a  27252  lgseisenlem2  27263  lgsquad2  27273  2lgslem1b  27279  2sqlem6  27310  2sqnn0  27325  addsq2reu  27327  2sqreulem2  27339  sltval2  27544  sltres  27550  nodenselem8  27579  nodense  27580  noresle  27585  scutun12  27698  madeval2  27737  elmade  27755  negsf1o  27936  muls0ord  28064  recsex  28097  bdayon  28149  noseqrdgfn  28176  n0subs  28229  eln0zs  28264  tgcgrcomimp  28380  isperp2  28618  xmstrkgc  28789  brbtwn  28802  brcgr  28803  axcgrid  28819  axeuclidlem  28865  axeuclid  28866  elntg2  28888  lpvtx  28971  upgrex  28995  upgrpredgv  29042  upgredgpr  29045  uhgr0v0e  29141  subgrprop  29176  fusgrfisbase  29231  edgnbusgreu  29270  nbusgredgeu0  29271  cusgredg  29327  structtocusgr  29349  cusgrsize2inds  29357  cusgrsize  29358  usgredgsscusgredg  29363  fusgrmaxsize  29368  uspgrloopvtxel  29420  umgr2v2e  29429  vtxdginducedm1fi  29448  finsumvtxdg2sstep  29453  rgrprop  29464  rusgrprop  29466  0uhgrrusgr  29482  rusgrpropedg  29488  ewlkprop  29507  upgrewlkle2  29510  wlkprop  29515  upgrwlkcompim  29546  uspgr2wlkeq  29549  wlklenvclwlk  29557  wlkonprop  29560  wlkres  29572  redwlk  29574  wlkdlem2  29585  wksonproplem  29606  usgr2trlspth  29664  usgr2pth  29667  pthdlem1  29669  crctcshwlkn0lem4  29716  wwlksnprcl  29742  wlkiswwlks2  29778  wwlksm1edg  29784  wlknewwlksn  29790  wwlksnred  29795  wwlksnextbi  29797  wwlksnextwrd  29800  wwlksnextinj  29802  wwlksnextsurj  29803  umgr2wlk  29852  umgrwwlks2on  29860  elwwlks2  29869  clwwlk1loop  29890  umgrclwwlkge2  29893  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlkfo  29911  clwwisshclwwslemlem  29915  clwwlknwwlksn  29940  clwwlknlbonbgr1  29941  clwwlkn1loopb  29945  clwwlkf  29949  clwwlknon1  29999  clwwlknonwwlknonb  30008  clwwlknonex2lem2  30010  vdn0conngrumgrv2  30098  frgrnbnb  30195  frgrncvvdeqlem2  30202  frgrncvvdeqlem3  30203  frgrncvvdeqlem6  30206  frgrwopreglem4a  30212  fusgr2wsp2nb  30236  frrusgrord0lem  30241  numclwwlk2lem1lem  30244  2clwwlk2clwwlklem  30248  2clwwlk2clwwlk  30252  numclwwlk1lem2foa  30256  numclwwlk1lem2f1  30259  frgrreg  30296  hlipgt0  30816  ocin  31198  ocnel  31200  shmodsi  31291  pjmf1  31618  unopf1o  31818  staddi  32148  stadd3i  32150  mdi  32197  dmdmd  32202  dmdi  32204  dmdbr2  32205  dmdbr3  32207  dmdbr4  32208  dmdi4  32209  mdsl1i  32223  superpos  32256  cvbr4i  32269  atssma  32280  atcv1  32282  atomli  32284  chirredlem1  32292  addltmulALT  32348  bian1dOLD  32359  ifeqeqx  32444  disjxpin  32490  suppss3  32620  fpwrelmap  32629  expgt0b  32714  mndlactfo  32941  mndractfo  32943  ogrpaddlt  33004  qsfld  33442  ply1degltdimlem  33591  ply1degltdim  33592  metider  33857  tpr2rico  33875  xrge0iifiso  33898  qqhcn  33954  qqhucn  33955  esumlub  34023  esumpinfval  34036  esumpinfsum  34040  ballotlemfc0  34457  ballotlemfcc  34458  ftc2re  34562  bnj517  34848  axsepg2  35045  axsepg2ALT  35046  fnrelpredd  35052  axnulg  35055  pfxwlk  35084  subgrwlk  35092  loop1cycl  35097  erdsze2lem2  35164  satfv1  35323  satfdmlem  35328  satf0op  35337  fmlasuc  35346  dfrdg4  35912  altopthsn  35922  btwncomim  35974  btwnexch3  35981  btwnexch2  35984  endofsegid  36046  opnrebl2  36282  nn0prpwlem  36283  onsuct0  36402  ordcmp  36408  nndivsub  36418  dnibndlem13  36451  bj-cbval  36610  bj-cbvex  36611  bj-cbvexw  36637  bj-cbv3tb  36748  bj-spimtv  36755  bj-equsal  36787  bj-sbsb  36798  bj-vtoclf  36876  bj-zfauscl  36885  bj-gabss  36896  bj-gabeqd  36898  currysetlem2  36909  bj-snsetex  36924  bj-ismooredr2  37071  bj-inftyexpiinj  37170  bj-finsumval0  37246  bj-fvimacnv0  37247  bj-bary1lem1  37272  bj-bary1  37273  f1omptsnlem  37297  iooelexlt  37323  relowlpssretop  37325  rdgeqoa  37331  finxpsuclem  37358  fvineqsneq  37373  pibt2  37378  wl-isseteq  37466  wl-equsal1i  37505  wl-ax11-lem10  37555  ltflcei  37575  sin2h  37577  cos2h  37578  tan2h  37579  lindsenlbs  37582  matunitlindf  37585  poimirlem3  37590  poimirlem4  37591  poimirlem18  37605  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  poimirlem31  37618  poimir  37620  heicant  37622  mblfinlem1  37624  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  mbfresfi  37633  cnambfre  37635  ftc1anc  37668  dvasin  37671  areacirclem1  37675  areacirclem4  37678  areacirc  37680  brabg2  37684  fzmul  37708  fdc  37712  incsequz2  37716  isbnd2  37750  opidonOLD  37819  opidon2OLD  37821  grpomndo  37842  elghomlem2OLD  37853  rngoueqz  37907  dvrunz  37921  divrngidl  37995  refressn  38407  dral1-o  38870  lsatn0  38965  l1cvpat  39020  leat2  39260  atnle  39283  cvlcvr1  39305  cvrexchlem  39386  cvratlem  39388  cvrat  39389  atcvrj0  39395  atle  39403  snatpsubN  39717  linepsubN  39719  pmapsub  39735  lneq2at  39745  lncvrelatN  39748  2llnma3r  39755  cdlemblem  39760  paddasslem5  39791  poml4N  39920  lhpmcvr4N  39993  trlval2  40130  cdlemd6  40170  cdleme7ga  40215  cdleme25b  40321  cdleme29b  40342  cdleme35fnpq  40416  cdleme50f1  40510  cdlemf1  40528  cdlemg27b  40663  cdlemk28-3  40875  tendospcanN  40990  diaf11N  41016  dia2dimlem1  41031  dibf11N  41128  dihf11  41234  dihmeetlem1N  41257  dochvalr  41324  dochnel2  41359  dvh4dimlem  41410  dochsat0  41424  mapd1o  41615  hdmapf1oN  41832  hgmapval0  41859  hgmapf1oN  41870  hlhilhillem  41927  nnproddivdvdsd  41961  lcmineqlem  42013  aks4d1p1p5  42036  aks4d1p3  42039  aks4d1p8d2  42046  aks4d1p8  42048  aks4d1p9  42049  fldhmf1  42051  isprimroot2  42055  primrootsunit1  42058  primrootscoprmpow  42060  posbezout  42061  primrootscoprbij  42063  primrootlekpowne0  42066  primrootspoweq0  42067  aks6d1c1p1  42068  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1p8  42076  aks6d1c2p2  42080  aks6d1c2lem3  42087  aks6d1c2lem4  42088  hashnexinj  42089  hashnexinjle  42090  aks6d1c2  42091  aks6d1c5lem0  42096  aks6d1c5lem1  42097  aks6d1c5  42100  sticksstones1  42107  sticksstones3  42109  sticksstones8  42114  sticksstones11  42117  sticksstones12  42119  sticksstones20  42127  sticksstones22  42129  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6isolem1  42135  aks6d1c6isolem2  42136  aks6d1c6lem5  42138  aks6d1c7  42145  rhmqusspan  42146  unitscyglem2  42157  unitscyglem3  42158  aks5lem8  42162  sn-axprlem3  42178  oexpreposd  42283  sn-remul0ord  42369  frlmsnic  42501  fsuppind  42551  prjspval  42564  rexrabdioph  42755  fphpdo  42778  irrapxlem3  42785  rmxypairf1o  42873  rmxycomplete  42879  zindbi  42908  lermxnn0  42912  ltrmy  42914  rmyeq0  42915  rmyeq  42916  lermy  42917  acongsym  42938  acongneg2  42939  wepwsolem  43004  onsupuni  43191  onsupmaxb  43201  onsucf1o  43234  onov0suclim  43236  oe0suclim  43239  onsucwordi  43250  cantnfresb  43286  omabs2  43294  tfsconcat0b  43308  tfsconcatrev  43310  naddcnffo  43326  oaun3lem1  43336  oaltom  43367  omltoe  43369  sdomne0  43375  sdomne0d  43376  safesnsupfidom1o  43379  intabssd  43481  iscard4  43495  ss2iundf  43621  frege129d  43725  frege133d  43727  axfrege52a  43818  axfrege52c  43849  ntrk0kbimka  44001  gneispace  44096  suprleubrd  44128  suprlubrd  44130  radcnvrat  44276  nzss  44279  expgrowthi  44295  ordpss  44413  bi23impib  44449  rspsbc2  44497  tratrb  44499  sbcim2g  44501  truniALT  44504  3impcombi  44779  tpid3gVD  44804  orbi1rVD  44810  sbc3orgVD  44813  rspsbc2VD  44817  tratrbVD  44823  sbcim2gVD  44837  sbcbiVD  44838  truniALTVD  44840  trintALTVD  44842  trintALT  44843  csbingVD  44846  csbsngVD  44855  csbxpgVD  44856  csbresgVD  44857  csbrngVD  44858  csbima12gALTVD  44859  csbunigVD  44860  csbfv12gALTVD  44861  relopabVD  44863  isosctrlem1ALT  44896  relpfrlem  44916  trfr  44925  fzisoeu  45271  xrralrecnnge  45359  allbutfi  45362  climinf  45577  liminfreuzlem  45773  climliminf  45777  climliminflimsup  45779  xlimpnfxnegmnf  45785  xlimbr  45798  stoweidlem7  45978  stoweidlem62  46033  sge0gerpmpt  46373  meaiuninclem  46451  carageniuncllem2  46493  issmflem  46698  et-sqrtnegnre  46844  ormkglobd  46846  natlocalincr  46847  tworepnotupword  46857  funressnfv  47017  funressnvmo  47019  f1cof1b  47051  2reu3  47084  ralbinrald  47096  afv0fv0  47123  afv0nbfvbi  47125  afvfv0bi  47126  fnbrafvb  47128  afvres  47146  tz6.12-afv  47147  afvco2  47150  ndmaovcl  47177  afv2res  47213  tz6.12-afv2  47214  nelbrim  47249  f1oresf1o2  47265  zm1nn  47276  nltle2tri  47287  subsubelfzo0  47300  2tceilhalfelfzo1  47306  iccpartres  47392  iccpartiltu  47396  fargshiftfv  47413  ichnreuop  47446  ichreuopeq  47447  prsprel  47461  sprsymrelf1lem  47465  sprsymrelfolem2  47467  sprsymrelfo  47471  prpair  47475  paireqne  47485  sbcpr  47495  fmtnof1  47509  goldbachthlem2  47520  fmtnoprmfac1  47539  fmtnoprmfac2  47541  lighneallem2  47580  lighneallem4b  47583  lighneallem4  47584  evennodd  47617  oddneven  47618  oexpnegnz  47652  evenltle  47691  fpprwppr  47713  fpprwpprb  47714  gbowge7  47737  gbege6  47739  sbgoldbwt  47751  sbgoldbst  47752  nnsum3primesle9  47768  bgoldbtbndlem2  47780  grimprop  47856  isuspgrimlem  47868  uhgrimisgrgriclem  47903  clnbgrgrimlem  47906  grtriproplem  47911  isgrtri  47915  grimgrtri  47921  stgr1  47933  isubgr3stgr  47947  grlimprop  47956  uspgrlimlem2  47961  uspgrlimlem3  47962  gpg5nbgrvtx13starlem1  48035  clintop  48169  isassintop  48171  lidldomn1  48192  uzlidlring  48196  2zrngnmlid2  48218  rngccatidALTV  48233  ringccatidALTV  48267  srhmsubcALTV  48286  ztprmneprm  48308  pgrpgt2nabl  48327  lindslinindimp2lem4  48423  lincresunit3  48443  fldivexpfllog2  48527  digexp  48569  naryfvalelfv  48594  affinecomb1  48664  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  eenglngeehlnm  48701  itscnhlc0yqe  48721  itsclc0yqsol  48726  itscnhlc0xyqsol  48727  itschlc0xyqsol1  48728  itschlc0xyqsol  48729  itsclquadeu  48739  inlinecirc02plem  48748  inlinecirc02p  48749  pm4.71da  48751  mofsn  48805  seposep  48887  resipos  48936  idmon  48982  idepi  48983  prsthinc  49426  grptcmon  49555  grptcepi  49556  spd  49640  spcdvw  49641  setrec2fun  49654