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  3240  rgen2a  3336  ralcom2  3342  ceqsalt  3472  ceqsalgALT  3475  spcimgft  3503  vtoclfOLD  3522  vtoclegft  3545  spcdv  3551  rspcdv  3571  rspcebdv  3573  rexraleqim  3604  sbcn1  3797  sbcbi1  3802  sbeqalb  3807  sbcel21v  3812  disj  4403  elpwunsn  4638  rabsnifsb  4676  ssunsn2  4781  preqr1g  4806  iuneqconst  4956  axprlem3  5367  axprlem3OLD  5370  sbcop1  5435  propeqop  5454  euotd  5460  rexopabb  5475  sotr2  5565  relop  5797  elinxp  5974  elimasni  6046  sotri2  6082  onmindif  6405  dffv2  6922  mpteqb  6953  elfvmptrab  6963  chfnrn  6987  elpreima  6996  iinpreima  7007  exfo  7043  ffnfv  7057  f1elima  7204  f1ounsn  7213  f1eqcocnv  7242  fliftfun  7253  soisores  7268  isotr  7277  isomin  7278  ovmpodv2  7511  difsnexi  7701  onint  7730  oneqmin  7740  ordunisuc2  7784  tfindsg  7801  findsg  7837  resf1extb  7874  f1oweALT  7914  el2mpocl  8026  poseq  8098  soseq  8099  ressuppss  8123  funsssuppss  8130  suppofssd  8143  smoiso  8292  seqomlem2  8380  oaordi  8471  oawordri  8475  oaordex  8483  oalimcl  8485  omwordi  8496  oewordi  8516  oelim2  8520  nnmwordi  8560  xpider  8722  iiner  8723  undifixp  8868  mptelixpg  8869  dom2lem  8924  findcard2s  9089  pssnn  9092  nneneq  9130  fineqvlem  9167  dif1ennnALT  9180  unfilem2  9213  xpfiOLD  9228  domunfican  9230  f1dmvrnfibi  9250  fsuppimp  9277  dffi2  9332  infsupprpr  9415  wemaplem2  9458  suc11reg  9534  noinfep  9575  cantnflem1  9604  r1fin  9688  tcrank  9799  cardlim  9887  fseqenlem1  9937  alephnbtwn  9984  alephord2i  9990  alephf1  9998  cardaleph  10002  alephiso  10011  dfac12lem2  10058  ackbij1lem16  10147  cflm  10163  cfcoflem  10185  sornom  10190  fin23lem27  10241  isf32lem7  10272  fin17  10307  fin1a2lem2  10314  fin1a2lem4  10316  fin1a2lem6  10318  fin1a2lem9  10321  axdc3lem2  10364  zorn2lem7  10415  uniimadom  10457  inar1  10688  grothomex  10742  addcanpi  10812  mulcanpi  10813  enqer  10834  genpcd  10919  genpnmax  10920  ltexprlem4  10952  reclem3pr  10962  reclem4pr  10963  suplem2pr  10966  axpre-ltadd  11080  axpre-sup  11082  ltletr  11227  00id  11310  addn0nid  11559  mul0or  11779  prodgt02  11991  lemul1a  11997  mulgt1OLD  12002  divgt0  12012  divge0  12013  ledivp1i  12069  ltdivp1i  12070  cju  12143  nnsub  12191  nominpos  12380  nn0n0n1ge2  12471  btwnnz  12571  suprfinzcl  12609  ublbneg  12853  zmax  12865  cnref1o  12905  ltsubrp  12950  ltaddrp  12951  xrltletr  13078  qbtwnre  13120  xltnegi  13137  xnn0xadd0  13168  iccsupr  13364  icoshft  13395  difreicc  13406  iccshftri  13409  iccshftli  13411  iccdili  13413  icccntri  13415  fzen  13463  elfz1b  13515  fzofzim  13631  eluzgtdifelfzo  13649  elfzo1elm1fzo0  13690  injresinjlem  13709  injresinj  13710  flval2  13737  flval3  13738  modmuladdim  13840  modaddmodup  13860  addmodlteq  13872  fseqsupubi  13904  ssnn0fi  13911  mptnn0fsuppr  13925  sq01  14151  hashf1rn  14278  hashgt12el  14348  hashgt12el2  14349  hashfundm  14368  hash2pr  14395  hash2exprb  14397  hashge2el2difr  14407  hashtpg  14411  hash3tr  14417  lswlgt0cl  14495  ccatalpha  14519  pfxfv  14608  pfxsuff1eqwrdeq  14624  ccatopth2  14642  swrdccat  14660  swrdccat3blem  14664  reuccatpfxs1lem  14671  repsdf2  14703  repswsymball  14704  repswrevw  14712  cshweqrep  14746  cshw1  14747  2cshwcshw  14751  scshwfzeqfzo  14752  cshwcsh2id  14754  swrdco  14763  swrd2lsw  14878  2swrd2eqwrdeq  14879  wwlktovfo  14884  cjre  15065  icodiamlt  15364  reusq0  15391  o1lo1  15463  o1of2  15539  o1rlimmul  15545  zsum  15644  modfsummods  15719  zprod  15863  reeff1  16048  dvdsmod0  16188  dvds2lem  16198  muldvds1  16210  dvdscmulr  16214  dvdsmulcr  16215  dvdsdivcl  16246  mod2eq1n2dvds  16277  oddnn02np1  16278  divalglem8  16330  ndvdsadd  16340  zeqzmulgcd  16440  dfgcd2  16476  absproddvds  16547  lcmftp  16566  coprmdvds  16583  2mulprm  16623  isprm5  16637  divgcdodd  16640  isprm6  16644  prmdvdsexpr  16647  prmdvdsbc  16656  cncongrprm  16659  phiprmpw  16706  modprm0  16736  pythagtriplem4  16750  pcz  16812  difsqpwdvds  16818  1arith  16858  prmgaplem5  16986  prmgaplem6  16987  cshwrepswhash1  17033  sbcie2s  17091  divsfval  17470  catsubcat  17765  fthmon  17855  isinitoi  17925  istermoi  17926  iszeroi  17935  setcmon  18013  setcepi  18014  funcestrcsetclem8  18072  fthestrcsetc  18075  funcsetcestrclem8  18087  fthsetcestrc  18090  odupos  18251  pltnle  18261  pltval3  18262  lublecllem  18283  latasym  18368  mrelatglb  18485  mrelatlub  18487  cnvpsb  18504  mgmpropd  18544  isgrpid2  18874  ghmghmrn  19133  ghmf1  19144  kerf1ghm  19145  orbsta  19211  resscntz  19231  gsmsymgrfixlem1  19325  gsmsymgreqlem2  19329  mndodcongi  19441  odf1  19460  lsmss1  19563  lsmss2  19565  efgredeu  19650  cntzcmnss  19739  imasabl  19774  lt6abl  19793  ablfaclem3  19987  ogrpaddlt  20036  ringinvnz1ne0  20204  0ringnnzr  20429  subrngringnsg  20457  srhmsubc  20584  domnmuln0  20613  lspsneq  21048  lspsneu  21049  lsmcv  21067  rnglidlmcl  21142  rngqiprngimf1lem  21220  lidldvgen  21260  domnchr  21458  znf1o  21477  zntoslem  21482  znfld  21486  cygznlem2a  21493  cygznlem3  21495  phlssphl  21585  islindf4  21764  uvcendim  21773  psdmul  22070  ply1scln0  22195  gsummoncoe1  22212  matvscl  22335  scmataddcl  22420  scmatsubcl  22421  scmatfo  22434  scmatghm  22437  maducoeval2  22544  slesolinv  22584  cramerimplem2  22588  cpmatelimp  22616  cpmatelimp2  22618  cpmatacl  22620  cpmatinvcl  22621  pm2mpf1  22703  cayhamlem1  22770  cayleyhamilton1  22796  0ntr  22975  islpi  23053  lmss  23202  cmpcld  23306  cmpfi  23312  1stcelcls  23365  comppfsc  23436  ptcnplem  23525  qtophmeo  23721  fbdmn0  23738  fbasrn  23788  elfm3  23854  fmfnfmlem4  23861  fclscf  23929  cnpfcf  23945  alexsubALTlem3  23953  tsmsres  24048  blval2  24467  tnggrpr  24560  nmoleub  24636  nmhmcn  25037  ncvs1  25074  iscau4  25196  caussi  25214  cmssmscld  25267  cmslssbn  25289  cniccbdd  25379  ovoliunnul  25425  mbfinf  25583  itg2splitlem  25666  dvcn  25840  c1lip1  25919  c1lip3  25921  dvcnvrelem1  25939  dvfsumlem2  25950  ply1divex  26059  quotcan  26234  aannenlem1  26253  taylf  26285  taylthlem2  26299  ulmcaulem  26320  ulmcau  26321  reeff1o  26374  logccv  26589  rtprmirr  26687  logreclem  26689  isosctrlem2  26746  xrlimcnp  26895  rlimcxp  26901  ftalem7  27006  vmappw  27043  fsumdvdsmul  27122  fsumvma  27141  dchreq  27186  dchrptlem1  27192  dchrsum  27197  bposlem7  27218  lgsqrlem2  27275  lgsdchr  27283  gausslemma2dlem1a  27293  lgseisenlem2  27304  lgsquad2  27314  2lgslem1b  27320  2sqlem6  27351  2sqnn0  27366  addsq2reu  27368  2sqreulem2  27380  sltval2  27585  sltres  27591  nodenselem8  27620  nodense  27621  noresle  27626  scutun12  27740  madeval2  27782  elmade  27800  negsf1o  27984  muls0ord  28112  recsex  28145  bdayon  28197  noseqrdgfn  28224  n0subs  28277  eln0zs  28312  zsoring  28320  tgcgrcomimp  28441  isperp2  28679  xmstrkgc  28850  brbtwn  28863  brcgr  28864  axcgrid  28880  axeuclidlem  28926  axeuclid  28927  elntg2  28949  lpvtx  29032  upgrex  29056  upgrpredgv  29103  upgredgpr  29106  uhgr0v0e  29202  subgrprop  29237  fusgrfisbase  29292  edgnbusgreu  29331  nbusgredgeu0  29332  cusgredg  29388  structtocusgr  29410  cusgrsize2inds  29418  cusgrsize  29419  usgredgsscusgredg  29424  fusgrmaxsize  29429  uspgrloopvtxel  29481  umgr2v2e  29490  vtxdginducedm1fi  29509  finsumvtxdg2sstep  29514  rgrprop  29525  rusgrprop  29527  0uhgrrusgr  29543  rusgrpropedg  29549  ewlkprop  29568  upgrewlkle2  29571  wlkprop  29576  upgrwlkcompim  29607  uspgr2wlkeq  29610  wlklenvclwlk  29618  wlkonprop  29621  wlkres  29633  redwlk  29635  wlkdlem2  29646  wksonproplem  29667  usgr2trlspth  29725  usgr2pth  29728  pthdlem1  29730  crctcshwlkn0lem4  29777  wwlksnprcl  29803  wlkiswwlks2  29839  wwlksm1edg  29845  wlknewwlksn  29851  wwlksnred  29856  wwlksnextbi  29858  wwlksnextwrd  29861  wwlksnextinj  29863  wwlksnextsurj  29864  umgr2wlk  29913  umgrwwlks2on  29921  elwwlks2  29930  clwwlk1loop  29951  umgrclwwlkge2  29954  clwlkclwwlklem2a1  29955  clwlkclwwlklem2a4  29960  clwlkclwwlklem2a  29961  clwlkclwwlklem2  29963  clwlkclwwlkfo  29972  clwwisshclwwslemlem  29976  clwwlknwwlksn  30001  clwwlknlbonbgr1  30002  clwwlkn1loopb  30006  clwwlkf  30010  clwwlknon1  30060  clwwlknonwwlknonb  30069  clwwlknonex2lem2  30071  vdn0conngrumgrv2  30159  frgrnbnb  30256  frgrncvvdeqlem2  30263  frgrncvvdeqlem3  30264  frgrncvvdeqlem6  30267  frgrwopreglem4a  30273  fusgr2wsp2nb  30297  frrusgrord0lem  30302  numclwwlk2lem1lem  30305  2clwwlk2clwwlklem  30309  2clwwlk2clwwlk  30313  numclwwlk1lem2foa  30317  numclwwlk1lem2f1  30320  frgrreg  30357  hlipgt0  30877  ocin  31259  ocnel  31261  shmodsi  31352  pjmf1  31679  unopf1o  31879  staddi  32209  stadd3i  32211  mdi  32258  dmdmd  32263  dmdi  32265  dmdbr2  32266  dmdbr3  32268  dmdbr4  32269  dmdi4  32270  mdsl1i  32284  superpos  32317  cvbr4i  32330  atssma  32341  atcv1  32343  atomli  32345  chirredlem1  32353  addltmulALT  32409  bian1dOLD  32420  ifeqeqx  32505  disjxpin  32551  suppss3  32686  fpwrelmap  32695  expgt0b  32780  mndlactfo  33000  mndractfo  33002  qsfld  33454  ply1degltdimlem  33608  ply1degltdim  33609  metider  33880  tpr2rico  33898  xrge0iifiso  33921  qqhcn  33977  qqhucn  33978  esumlub  34046  esumpinfval  34059  esumpinfsum  34063  ballotlemfc0  34480  ballotlemfcc  34481  ftc2re  34585  bnj517  34871  axsepg2  35068  axsepg2ALT  35069  fnrelpredd  35075  axnulg  35078  pfxwlk  35116  subgrwlk  35124  loop1cycl  35129  erdsze2lem2  35196  satfv1  35355  satfdmlem  35360  satf0op  35369  fmlasuc  35378  dfrdg4  35944  altopthsn  35954  btwncomim  36006  btwnexch3  36013  btwnexch2  36016  endofsegid  36078  opnrebl2  36314  nn0prpwlem  36315  onsuct0  36434  ordcmp  36440  nndivsub  36450  dnibndlem13  36483  bj-cbval  36642  bj-cbvex  36643  bj-cbvexw  36669  bj-cbv3tb  36780  bj-spimtv  36787  bj-equsal  36819  bj-sbsb  36830  bj-vtoclf  36908  bj-zfauscl  36917  bj-gabss  36928  bj-gabeqd  36930  currysetlem2  36941  bj-snsetex  36956  bj-ismooredr2  37103  bj-inftyexpiinj  37202  bj-finsumval0  37278  bj-fvimacnv0  37279  bj-bary1lem1  37304  bj-bary1  37305  f1omptsnlem  37329  iooelexlt  37355  relowlpssretop  37357  rdgeqoa  37363  finxpsuclem  37390  fvineqsneq  37405  pibt2  37410  wl-isseteq  37498  wl-equsal1i  37537  wl-ax11-lem10  37587  ltflcei  37607  sin2h  37609  cos2h  37610  tan2h  37611  lindsenlbs  37614  matunitlindf  37617  poimirlem3  37622  poimirlem4  37623  poimirlem18  37637  poimirlem20  37639  poimirlem21  37640  poimirlem22  37641  poimirlem24  37643  poimirlem25  37644  poimirlem26  37645  poimirlem27  37646  poimirlem28  37647  poimirlem31  37650  poimir  37652  heicant  37654  mblfinlem1  37656  mblfinlem2  37657  mblfinlem3  37658  mblfinlem4  37659  mbfresfi  37665  cnambfre  37667  ftc1anc  37700  dvasin  37703  areacirclem1  37707  areacirclem4  37710  areacirc  37712  brabg2  37716  fzmul  37740  fdc  37744  incsequz2  37748  isbnd2  37782  opidonOLD  37851  opidon2OLD  37853  grpomndo  37874  elghomlem2OLD  37885  rngoueqz  37939  dvrunz  37953  divrngidl  38027  refressn  38439  dral1-o  38902  lsatn0  38997  l1cvpat  39052  leat2  39292  atnle  39315  cvlcvr1  39337  cvrexchlem  39418  cvratlem  39420  cvrat  39421  atcvrj0  39427  atle  39435  snatpsubN  39749  linepsubN  39751  pmapsub  39767  lneq2at  39777  lncvrelatN  39780  2llnma3r  39787  cdlemblem  39792  paddasslem5  39823  poml4N  39952  lhpmcvr4N  40025  trlval2  40162  cdlemd6  40202  cdleme7ga  40247  cdleme25b  40353  cdleme29b  40374  cdleme35fnpq  40448  cdleme50f1  40542  cdlemf1  40560  cdlemg27b  40695  cdlemk28-3  40907  tendospcanN  41022  diaf11N  41048  dia2dimlem1  41063  dibf11N  41160  dihf11  41266  dihmeetlem1N  41289  dochvalr  41356  dochnel2  41391  dvh4dimlem  41442  dochsat0  41456  mapd1o  41647  hdmapf1oN  41864  hgmapval0  41891  hgmapf1oN  41902  hlhilhillem  41959  nnproddivdvdsd  41993  lcmineqlem  42045  aks4d1p1p5  42068  aks4d1p3  42071  aks4d1p8d2  42078  aks4d1p8  42080  aks4d1p9  42081  fldhmf1  42083  isprimroot2  42087  primrootsunit1  42090  primrootscoprmpow  42092  posbezout  42093  primrootscoprbij  42095  primrootlekpowne0  42098  primrootspoweq0  42099  aks6d1c1p1  42100  aks6d1c1p2  42102  aks6d1c1p3  42103  aks6d1c1p4  42104  aks6d1c1p5  42105  aks6d1c1p7  42106  aks6d1c1p6  42107  aks6d1c1p8  42108  aks6d1c2p2  42112  aks6d1c2lem3  42119  aks6d1c2lem4  42120  hashnexinj  42121  hashnexinjle  42122  aks6d1c2  42123  aks6d1c5lem0  42128  aks6d1c5lem1  42129  aks6d1c5  42132  sticksstones1  42139  sticksstones3  42141  sticksstones8  42146  sticksstones11  42149  sticksstones12  42151  sticksstones20  42159  sticksstones22  42161  aks6d1c6lem3  42165  aks6d1c6lem4  42166  aks6d1c6isolem1  42167  aks6d1c6isolem2  42168  aks6d1c6lem5  42170  aks6d1c7  42177  rhmqusspan  42178  unitscyglem2  42189  unitscyglem3  42190  aks5lem8  42194  sn-axprlem3  42210  oexpreposd  42315  sn-remul0ord  42401  frlmsnic  42533  fsuppind  42583  prjspval  42596  rexrabdioph  42787  fphpdo  42810  irrapxlem3  42817  rmxypairf1o  42904  rmxycomplete  42910  zindbi  42939  lermxnn0  42943  ltrmy  42945  rmyeq0  42946  rmyeq  42947  lermy  42948  acongsym  42969  acongneg2  42970  wepwsolem  43035  onsupuni  43222  onsupmaxb  43232  onsucf1o  43265  onov0suclim  43267  oe0suclim  43270  onsucwordi  43281  cantnfresb  43317  omabs2  43325  tfsconcat0b  43339  tfsconcatrev  43341  naddcnffo  43357  oaun3lem1  43367  oaltom  43398  omltoe  43400  sdomne0  43406  sdomne0d  43407  safesnsupfidom1o  43410  intabssd  43512  iscard4  43526  ss2iundf  43652  frege129d  43756  frege133d  43758  axfrege52a  43849  axfrege52c  43880  ntrk0kbimka  44032  gneispace  44127  suprleubrd  44159  suprlubrd  44161  radcnvrat  44307  nzss  44310  expgrowthi  44326  ordpss  44444  bi23impib  44480  rspsbc2  44528  tratrb  44530  sbcim2g  44532  truniALT  44535  3impcombi  44810  tpid3gVD  44835  orbi1rVD  44841  sbc3orgVD  44844  rspsbc2VD  44848  tratrbVD  44854  sbcim2gVD  44868  sbcbiVD  44869  truniALTVD  44871  trintALTVD  44873  trintALT  44874  csbingVD  44877  csbsngVD  44886  csbxpgVD  44887  csbresgVD  44888  csbrngVD  44889  csbima12gALTVD  44890  csbunigVD  44891  csbfv12gALTVD  44892  relopabVD  44894  isosctrlem1ALT  44927  relpfrlem  44947  trfr  44956  fzisoeu  45302  xrralrecnnge  45389  allbutfi  45392  climinf  45607  liminfreuzlem  45803  climliminf  45807  climliminflimsup  45809  xlimpnfxnegmnf  45815  xlimbr  45828  stoweidlem7  46008  stoweidlem62  46063  sge0gerpmpt  46403  meaiuninclem  46481  carageniuncllem2  46523  issmflem  46728  et-sqrtnegnre  46874  ormkglobd  46876  natlocalincr  46877  tworepnotupword  46887  funressnfv  47047  funressnvmo  47049  f1cof1b  47081  2reu3  47114  ralbinrald  47126  afv0fv0  47153  afv0nbfvbi  47155  afvfv0bi  47156  fnbrafvb  47158  afvres  47176  tz6.12-afv  47177  afvco2  47180  ndmaovcl  47207  afv2res  47243  tz6.12-afv2  47244  nelbrim  47279  f1oresf1o2  47295  zm1nn  47306  nltle2tri  47317  subsubelfzo0  47330  2tceilhalfelfzo1  47336  iccpartres  47422  iccpartiltu  47426  fargshiftfv  47443  ichnreuop  47476  ichreuopeq  47477  prsprel  47491  sprsymrelf1lem  47495  sprsymrelfolem2  47497  sprsymrelfo  47501  prpair  47505  paireqne  47515  sbcpr  47525  fmtnof1  47539  goldbachthlem2  47550  fmtnoprmfac1  47569  fmtnoprmfac2  47571  lighneallem2  47610  lighneallem4b  47613  lighneallem4  47614  evennodd  47647  oddneven  47648  oexpnegnz  47682  evenltle  47721  fpprwppr  47743  fpprwpprb  47744  gbowge7  47767  gbege6  47769  sbgoldbwt  47781  sbgoldbst  47782  nnsum3primesle9  47798  bgoldbtbndlem2  47810  grimprop  47887  isuspgrimlem  47899  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  grtriproplem  47943  isgrtri  47947  grimgrtri  47953  stgr1  47965  isubgr3stgr  47979  grlimprop  47988  uspgrlimlem2  47993  uspgrlimlem3  47994  grlimprclnbgr  48000  gpg5nbgrvtx13starlem1  48075  clintop  48212  isassintop  48214  lidldomn1  48235  uzlidlring  48239  2zrngnmlid2  48261  rngccatidALTV  48276  ringccatidALTV  48310  srhmsubcALTV  48329  ztprmneprm  48351  pgrpgt2nabl  48370  lindslinindimp2lem4  48466  lincresunit3  48486  fldivexpfllog2  48570  digexp  48612  naryfvalelfv  48637  affinecomb1  48707  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  eenglngeehlnm  48744  itscnhlc0yqe  48764  itsclc0yqsol  48769  itscnhlc0xyqsol  48770  itschlc0xyqsol1  48771  itschlc0xyqsol  48772  itsclquadeu  48782  inlinecirc02plem  48791  inlinecirc02p  48792  pm4.71da  48794  mofsn  48848  seposep  48930  resipos  48979  idmon  49025  idepi  49026  prsthinc  49469  grptcmon  49598  grptcepi  49599  spd  49683  spcdvw  49684  setrec2fun  49697