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  alexbii  1829  spvv  1993  spfw  2029  cbvalw  2031  sbequi  2081  chvarfv  2237  cbvalv1  2341  spv  2395  chvar  2397  cbval  2400  sb1  2480  nfsb4t  2501  exmoeu  2578  euim  2614  2eu3  2651  eqrdav  2733  ralbida  3267  rgen2a  3368  ralcom2  3374  ceqsalt  3512  ceqsalgALT  3515  spcimgft  3545  vtoclfOLD  3564  vtoclegft  3587  spcdv  3593  rspcdv  3613  rspcebdv  3615  rexraleqim  3646  elabgtOLDOLD  3673  sbcn1  3846  sbcim1OLD  3848  sbcbi1  3852  sbeqalb  3858  sbcel21v  3863  disj  4455  elpwunsn  4688  rabsnifsb  4726  ssunsn2  4831  preqr1g  4856  iuneqconst  5007  axprlem3  5430  axprlem3OLD  5433  sbcop1  5498  propeqop  5516  euotd  5522  rexopabb  5537  sotr2  5629  relop  5863  elinxp  6038  elimasni  6111  sotri2  6151  onmindif  6477  iotavalOLD  6536  dffv2  7003  mpteqb  7034  elfvmptrab  7044  chfnrn  7068  elpreima  7077  iinpreima  7088  exfo  7124  ffnfv  7138  f1elima  7282  f1ounsn  7291  f1eqcocnv  7320  fliftfun  7331  soisores  7346  isotr  7355  isomin  7356  ovmpodv2  7590  difsnexi  7779  onint  7809  oneqmin  7819  ordunisuc2  7864  tfindsg  7881  findsg  7919  f1oweALT  7995  el2mpocl  8109  poseq  8181  soseq  8182  ressuppss  8206  funsssuppss  8213  suppofssd  8226  smoiso  8400  seqomlem2  8489  oaordi  8582  oawordri  8586  oaordex  8594  oalimcl  8596  omwordi  8607  oewordi  8627  oelim2  8631  nnmwordi  8671  xpider  8826  iiner  8827  undifixp  8972  mptelixpg  8973  dom2lem  9030  findcard2s  9203  pssnn  9206  nneneq  9243  nneneqOLD  9255  fineqvlem  9295  dif1ennnALT  9308  unfilem2  9341  xpfiOLD  9356  domunfican  9358  f1dmvrnfibi  9378  fsuppimp  9405  dffi2  9460  infsupprpr  9541  wemaplem2  9584  suc11reg  9656  noinfep  9697  cantnflem1  9726  r1fin  9810  tcrank  9921  cardlim  10009  pr2nelemOLD  10040  fseqenlem1  10061  alephnbtwn  10108  alephord2i  10114  alephf1  10122  cardaleph  10126  alephiso  10135  dfac12lem2  10182  ackbij1lem16  10271  cflm  10287  cfcoflem  10309  sornom  10314  fin23lem27  10365  isf32lem7  10396  fin17  10431  fin1a2lem2  10438  fin1a2lem4  10440  fin1a2lem6  10442  fin1a2lem9  10445  axdc3lem2  10488  zorn2lem7  10539  uniimadom  10581  inar1  10812  grothomex  10866  addcanpi  10936  mulcanpi  10937  enqer  10958  genpcd  11043  genpnmax  11044  ltexprlem4  11076  reclem3pr  11086  reclem4pr  11087  suplem2pr  11090  axpre-ltadd  11204  axpre-sup  11206  ltletr  11350  00id  11433  addn0nid  11680  mul0or  11900  prodgt02  12112  lemul1a  12118  mulgt1OLD  12123  divgt0  12133  divge0  12134  ledivp1i  12190  ltdivp1i  12191  cju  12259  nnsub  12307  nominpos  12500  nn0n0n1ge2  12591  btwnnz  12691  suprfinzcl  12729  ublbneg  12972  zmax  12984  cnref1o  13024  ltsubrp  13068  ltaddrp  13069  xrltletr  13195  qbtwnre  13237  xltnegi  13254  xnn0xadd0  13285  iccsupr  13478  icoshft  13509  difreicc  13520  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  fzen  13577  elfz1b  13629  fzofzim  13745  eluzgtdifelfzo  13762  elfzo1elm1fzo0  13803  injresinjlem  13822  injresinj  13823  flval2  13850  flval3  13851  modmuladdim  13951  modaddmodup  13971  addmodlteq  13983  fseqsupubi  14015  ssnn0fi  14022  mptnn0fsuppr  14036  sq01  14260  hashf1rn  14387  hashgt12el  14457  hashgt12el2  14458  hashfundm  14477  hash2pr  14504  hash2exprb  14506  hashge2el2difr  14516  hashtpg  14520  hash3tr  14526  lswlgt0cl  14603  ccatalpha  14627  pfxfv  14716  pfxsuff1eqwrdeq  14733  ccatopth2  14751  swrdccat  14769  swrdccat3blem  14773  reuccatpfxs1lem  14780  repsdf2  14812  repswsymball  14813  repswrevw  14821  cshweqrep  14855  cshw1  14856  2cshwcshw  14860  scshwfzeqfzo  14861  cshwcsh2id  14863  swrdco  14872  swrd2lsw  14987  2swrd2eqwrdeq  14988  wwlktovfo  14993  cjre  15174  icodiamlt  15470  reusq0  15497  o1lo1  15569  o1of2  15645  o1rlimmul  15651  zsum  15750  modfsummods  15825  zprod  15969  reeff1  16152  dvdsmod0  16292  dvds2lem  16302  muldvds1  16314  dvdscmulr  16318  dvdsmulcr  16319  dvdsdivcl  16349  mod2eq1n2dvds  16380  oddnn02np1  16381  divalglem8  16433  ndvdsadd  16443  zeqzmulgcd  16543  dfgcd2  16579  absproddvds  16650  lcmftp  16669  coprmdvds  16686  2mulprm  16726  isprm5  16740  divgcdodd  16743  isprm6  16747  prmdvdsexpr  16750  prmdvdsbc  16759  cncongrprm  16762  phiprmpw  16809  modprm0  16838  pythagtriplem4  16852  pcz  16914  difsqpwdvds  16920  1arith  16960  prmgaplem5  17088  prmgaplem6  17089  cshwrepswhash1  17136  sbcie2s  17194  divsfval  17593  catsubcat  17889  fthmon  17980  isinitoi  18052  istermoi  18053  iszeroi  18062  setcmon  18140  setcepi  18141  funcestrcsetclem8  18202  fthestrcsetc  18205  funcsetcestrclem8  18217  fthsetcestrc  18220  odupos  18385  pltnle  18395  pltval3  18396  lublecllem  18417  latasym  18500  mrelatglb  18617  mrelatlub  18619  cnvpsb  18636  mgmpropd  18676  isgrpid2  19006  ghmghmrn  19265  ghmf1  19276  kerf1ghm  19277  orbsta  19343  resscntz  19363  gsmsymgrfixlem1  19459  gsmsymgreqlem2  19463  mndodcongi  19575  odf1  19594  lsmss1  19697  lsmss2  19699  efgredeu  19784  cntzcmnss  19873  imasabl  19908  lt6abl  19927  ablfaclem3  20121  ringinvnz1ne0  20313  0ringnnzr  20541  subrngringnsg  20569  srhmsubc  20696  domnmuln0  20725  lspsneq  21141  lspsneu  21142  lsmcv  21160  rnglidlmcl  21243  rngqiprngimf1lem  21321  lidldvgen  21361  domnchr  21564  znf1o  21587  zntoslem  21592  znfld  21596  cygznlem2a  21603  cygznlem3  21605  phlssphl  21694  islindf4  21875  uvcendim  21884  psdmul  22187  ply1scln0  22310  gsummoncoe1  22327  matvscl  22452  scmataddcl  22537  scmatsubcl  22538  scmatfo  22551  scmatghm  22554  maducoeval2  22661  slesolinv  22701  cramerimplem2  22705  cpmatelimp  22733  cpmatelimp2  22735  cpmatacl  22737  cpmatinvcl  22738  pm2mpf1  22820  cayhamlem1  22887  cayleyhamilton1  22913  0ntr  23094  islpi  23172  lmss  23321  cmpcld  23425  cmpfi  23431  1stcelcls  23484  comppfsc  23555  ptcnplem  23644  qtophmeo  23840  fbdmn0  23857  fbasrn  23907  elfm3  23973  fmfnfmlem4  23980  fclscf  24048  cnpfcf  24064  alexsubALTlem3  24072  tsmsres  24167  blval2  24590  tnggrpr  24691  nmoleub  24767  nmhmcn  25166  ncvs1  25204  iscau4  25326  caussi  25344  cmssmscld  25397  cmslssbn  25419  cniccbdd  25509  ovoliunnul  25555  mbfinf  25713  itg2splitlem  25797  dvcn  25971  c1lip1  26050  c1lip3  26052  dvcnvrelem1  26070  dvfsumlem2  26081  ply1divex  26190  quotcan  26365  aannenlem1  26384  taylf  26416  taylthlem2  26430  ulmcaulem  26451  ulmcau  26452  reeff1o  26505  logccv  26719  rtprmirr  26817  logreclem  26819  isosctrlem2  26876  xrlimcnp  27025  rlimcxp  27031  ftalem7  27136  vmappw  27173  fsumdvdsmul  27252  fsumvma  27271  dchreq  27316  dchrptlem1  27322  dchrsum  27327  bposlem7  27348  lgsqrlem2  27405  lgsdchr  27413  gausslemma2dlem1a  27423  lgseisenlem2  27434  lgsquad2  27444  2lgslem1b  27450  2sqlem6  27481  2sqnn0  27496  addsq2reu  27498  2sqreulem2  27510  sltval2  27715  sltres  27721  nodenselem8  27750  nodense  27751  noresle  27756  scutun12  27869  madeval2  27906  elmade  27920  negsf1o  28100  muls0ord  28225  recsex  28257  noseqrdgfn  28326  n0subs  28374  eln0zs  28400  tgcgrcomimp  28499  isperp2  28737  xmstrkgc  28914  brbtwn  28928  brcgr  28929  axcgrid  28945  axeuclidlem  28991  axeuclid  28992  elntg2  29014  lpvtx  29099  upgrex  29123  upgrpredgv  29170  upgredgpr  29173  uhgr0v0e  29269  subgrprop  29304  fusgrfisbase  29359  edgnbusgreu  29398  nbusgredgeu0  29399  cusgredg  29455  structtocusgr  29477  cusgrsize2inds  29485  cusgrsize  29486  usgredgsscusgredg  29491  fusgrmaxsize  29496  uspgrloopvtxel  29548  umgr2v2e  29557  vtxdginducedm1fi  29576  finsumvtxdg2sstep  29581  rgrprop  29592  rusgrprop  29594  0uhgrrusgr  29610  rusgrpropedg  29616  ewlkprop  29635  upgrewlkle2  29638  wlkprop  29643  upgrwlkcompim  29675  uspgr2wlkeq  29678  wlklenvclwlk  29687  wlkonprop  29690  wlkres  29702  redwlk  29704  wlkdlem2  29715  wksonproplem  29736  wksonproplemOLD  29737  usgr2trlspth  29793  usgr2pth  29796  pthdlem1  29798  crctcshwlkn0lem4  29842  wwlksnprcl  29868  wlkiswwlks2  29904  wwlksm1edg  29910  wlknewwlksn  29916  wwlksnred  29921  wwlksnextbi  29923  wwlksnextwrd  29926  wwlksnextinj  29928  wwlksnextsurj  29929  umgr2wlk  29978  umgrwwlks2on  29986  elwwlks2  29995  clwwlk1loop  30016  umgrclwwlkge2  30019  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlkfo  30037  clwwisshclwwslemlem  30041  clwwlknwwlksn  30066  clwwlknlbonbgr1  30067  clwwlkn1loopb  30071  clwwlkf  30075  clwwlknon1  30125  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  vdn0conngrumgrv2  30224  frgrnbnb  30321  frgrncvvdeqlem2  30328  frgrncvvdeqlem3  30329  frgrncvvdeqlem6  30332  frgrwopreglem4a  30338  fusgr2wsp2nb  30362  frrusgrord0lem  30367  numclwwlk2lem1lem  30370  2clwwlk2clwwlklem  30374  2clwwlk2clwwlk  30378  numclwwlk1lem2foa  30382  numclwwlk1lem2f1  30385  frgrreg  30422  hlipgt0  30942  ocin  31324  ocnel  31326  shmodsi  31417  pjmf1  31744  unopf1o  31944  staddi  32274  stadd3i  32276  mdi  32323  dmdmd  32328  dmdi  32330  dmdbr2  32331  dmdbr3  32333  dmdbr4  32334  dmdi4  32335  mdsl1i  32349  superpos  32382  cvbr4i  32395  atssma  32406  atcv1  32408  atomli  32410  chirredlem1  32418  addltmulALT  32474  bian1dOLD  32484  ifeqeqx  32562  disjxpin  32607  suppss3  32741  fpwrelmap  32750  expgt0b  32822  mndlactfo  33014  mndractfo  33016  ogrpaddlt  33076  qsfld  33505  ply1degltdimlem  33649  ply1degltdim  33650  metider  33854  tpr2rico  33872  xrge0iifiso  33895  qqhcn  33953  qqhucn  33954  esumlub  34040  esumpinfval  34053  esumpinfsum  34057  ballotlemfc0  34473  ballotlemfcc  34474  ftc2re  34591  bnj517  34877  axsepg2  35074  axsepg2ALT  35075  fnrelpredd  35081  axnulg  35084  pfxwlk  35107  subgrwlk  35116  loop1cycl  35121  erdsze2lem2  35188  satfv1  35347  satfdmlem  35352  satf0op  35361  fmlasuc  35370  dfrdg4  35932  altopthsn  35942  btwncomim  35994  btwnexch3  36001  btwnexch2  36004  endofsegid  36066  opnrebl2  36303  nn0prpwlem  36304  onsuct0  36423  ordcmp  36429  nndivsub  36439  dnibndlem13  36472  bj-cbval  36631  bj-cbvex  36632  bj-cbvexw  36658  bj-cbv3tb  36769  bj-spimtv  36776  bj-equsal  36808  bj-sbsb  36819  bj-vtoclf  36897  bj-zfauscl  36906  bj-gabss  36917  bj-gabeqd  36919  currysetlem2  36930  bj-snsetex  36945  bj-ismooredr2  37092  bj-inftyexpiinj  37191  bj-finsumval0  37267  bj-fvimacnv0  37268  bj-bary1lem1  37293  bj-bary1  37294  f1omptsnlem  37318  iooelexlt  37344  relowlpssretop  37346  rdgeqoa  37352  finxpsuclem  37379  fvineqsneq  37394  pibt2  37399  wl-isseteq  37485  wl-equsal1i  37524  wl-ax11-lem10  37574  ltflcei  37594  sin2h  37596  cos2h  37597  tan2h  37598  lindsenlbs  37601  matunitlindf  37604  poimirlem3  37609  poimirlem4  37610  poimirlem18  37624  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  poimir  37639  heicant  37641  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  mbfresfi  37652  cnambfre  37654  ftc1anc  37687  dvasin  37690  areacirclem1  37694  areacirclem4  37697  areacirc  37699  brabg2  37703  fzmul  37727  fdc  37731  incsequz2  37735  isbnd2  37769  opidonOLD  37838  opidon2OLD  37840  grpomndo  37861  elghomlem2OLD  37872  rngoueqz  37926  dvrunz  37940  divrngidl  38014  refressn  38424  dral1-o  38885  lsatn0  38980  l1cvpat  39035  leat2  39275  atnle  39298  cvlcvr1  39320  cvrexchlem  39401  cvratlem  39403  cvrat  39404  atcvrj0  39410  atle  39418  snatpsubN  39732  linepsubN  39734  pmapsub  39750  lneq2at  39760  lncvrelatN  39763  2llnma3r  39770  cdlemblem  39775  paddasslem5  39806  poml4N  39935  lhpmcvr4N  40008  trlval2  40145  cdlemd6  40185  cdleme7ga  40230  cdleme25b  40336  cdleme29b  40357  cdleme35fnpq  40431  cdleme50f1  40525  cdlemf1  40543  cdlemg27b  40678  cdlemk28-3  40890  tendospcanN  41005  diaf11N  41031  dia2dimlem1  41046  dibf11N  41143  dihf11  41249  dihmeetlem1N  41272  dochvalr  41339  dochnel2  41374  dvh4dimlem  41425  dochsat0  41439  mapd1o  41630  hdmapf1oN  41847  hgmapval0  41874  hgmapf1oN  41885  hlhilhillem  41946  nnproddivdvdsd  41981  lcmineqlem  42033  aks4d1p1p5  42056  aks4d1p3  42059  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  fldhmf1  42071  isprimroot2  42075  primrootsunit1  42078  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootlekpowne0  42086  primrootspoweq0  42087  aks6d1c1p1  42088  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c2p2  42100  aks6d1c2lem3  42107  aks6d1c2lem4  42108  hashnexinj  42109  hashnexinjle  42110  aks6d1c2  42111  aks6d1c5lem0  42116  aks6d1c5lem1  42117  aks6d1c5  42120  sticksstones1  42127  sticksstones3  42129  sticksstones8  42134  sticksstones11  42137  sticksstones12  42139  sticksstones20  42147  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  aks6d1c7  42165  rhmqusspan  42166  unitscyglem2  42177  unitscyglem3  42178  aks5lem8  42182  metakunt7  42192  sn-axprlem3  42234  oexpreposd  42335  frlmsnic  42526  fsuppind  42576  prjspval  42589  rexrabdioph  42781  fphpdo  42804  irrapxlem3  42811  rmxypairf1o  42899  rmxycomplete  42905  zindbi  42934  lermxnn0  42938  ltrmy  42940  rmyeq0  42941  rmyeq  42942  lermy  42943  acongsym  42964  acongneg2  42965  wepwsolem  43030  onsupuni  43217  onsupmaxb  43227  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  44309  nzss  44312  expgrowthi  44328  ordpss  44446  bi23impib  44482  bi23imp13  44488  rspsbc2  44531  tratrb  44533  sbcim2g  44535  truniALT  44538  3impcombi  44814  tpid3gVD  44839  orbi1rVD  44845  sbc3orgVD  44848  rspsbc2VD  44852  tratrbVD  44858  sbcim2gVD  44872  sbcbiVD  44873  truniALTVD  44875  trintALTVD  44877  trintALT  44878  csbingVD  44881  csbsngVD  44890  csbxpgVD  44891  csbresgVD  44892  csbrngVD  44893  csbima12gALTVD  44894  csbunigVD  44895  csbfv12gALTVD  44896  relopabVD  44898  isosctrlem1ALT  44931  fzisoeu  45250  xrralrecnnge  45339  allbutfi  45342  climinf  45561  liminfreuzlem  45757  climliminf  45761  climliminflimsup  45763  xlimpnfxnegmnf  45769  xlimbr  45782  stoweidlem7  45962  stoweidlem62  46017  sge0gerpmpt  46357  meaiuninclem  46435  carageniuncllem2  46477  issmflem  46682  et-sqrtnegnre  46828  natlocalincr  46829  tworepnotupword  46839  funressnfv  46992  funressnvmo  46994  f1cof1b  47026  2reu3  47059  ralbinrald  47071  afv0fv0  47098  afv0nbfvbi  47100  afvfv0bi  47101  fnbrafvb  47103  afvres  47121  tz6.12-afv  47122  afvco2  47125  ndmaovcl  47152  afv2res  47188  tz6.12-afv2  47189  nelbrim  47224  f1oresf1o2  47240  zm1nn  47251  nltle2tri  47262  subsubelfzo0  47275  iccpartres  47342  iccpartiltu  47346  fargshiftfv  47363  ichnreuop  47396  ichreuopeq  47397  prsprel  47411  sprsymrelf1lem  47415  sprsymrelfolem2  47417  sprsymrelfo  47421  prpair  47425  paireqne  47435  sbcpr  47445  fmtnof1  47459  goldbachthlem2  47470  fmtnoprmfac1  47489  fmtnoprmfac2  47491  lighneallem2  47530  lighneallem4b  47533  lighneallem4  47534  evennodd  47567  oddneven  47568  oexpnegnz  47602  evenltle  47641  fpprwppr  47663  fpprwpprb  47664  gbowge7  47687  gbege6  47689  sbgoldbwt  47701  sbgoldbst  47702  nnsum3primesle9  47718  bgoldbtbndlem2  47730  grimprop  47806  isuspgrimlem  47811  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  grtriproplem  47843  isgrtri  47847  grimgrtri  47851  stgr1  47863  isubgr3stgr  47877  grlimprop  47886  uspgrlimlem2  47891  uspgrlimlem3  47892  2tceilhalfelfzo1  47952  gpg5nbgrvtx13starlem1  47961  clintop  48051  isassintop  48053  lidldomn1  48074  uzlidlring  48078  2zrngnmlid2  48100  rngccatidALTV  48115  ringccatidALTV  48149  srhmsubcALTV  48168  ztprmneprm  48191  pgrpgt2nabl  48210  lindslinindimp2lem4  48306  lincresunit3  48326  fldivexpfllog2  48414  digexp  48456  naryfvalelfv  48481  affinecomb1  48551  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  eenglngeehlnm  48588  itscnhlc0yqe  48608  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itschlc0xyqsol  48616  itsclquadeu  48626  inlinecirc02plem  48635  inlinecirc02p  48636  pm4.71da  48638  mofsn  48673  seposep  48721  idmon  48804  idepi  48805  prsthinc  48854  grptcmon  48901  grptcepi  48902  spd  48908  spcdvw  48909  setrec2fun  48922