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  1116  alexbii  1833  spvv  1996  spfw  2032  cbvalw  2034  sbequi  2084  chvarfv  2240  cbvalv1  2343  spv  2398  chvar  2400  cbval  2403  sb1  2483  nfsb4t  2504  exmoeu  2581  euim  2617  2eu3  2654  eqrdav  2736  ralbida  3270  rgen2a  3371  ralcom2  3377  ceqsalt  3515  ceqsalgALT  3518  spcimgft  3546  vtoclfOLD  3565  vtoclegft  3588  spcdv  3594  rspcdv  3614  rspcebdv  3616  rexraleqim  3647  sbcn1  3841  sbcim1OLD  3843  sbcbi1  3847  sbeqalb  3853  sbcel21v  3858  disj  4450  elpwunsn  4684  rabsnifsb  4722  ssunsn2  4827  preqr1g  4852  iuneqconst  5003  axprlem3  5425  axprlem3OLD  5428  sbcop1  5493  propeqop  5512  euotd  5518  rexopabb  5533  sotr2  5626  relop  5861  elinxp  6037  elimasni  6109  sotri2  6149  onmindif  6476  iotavalOLD  6535  dffv2  7004  mpteqb  7035  elfvmptrab  7045  chfnrn  7069  elpreima  7078  iinpreima  7089  exfo  7125  ffnfv  7139  f1elima  7283  f1ounsn  7292  f1eqcocnv  7321  fliftfun  7332  soisores  7347  isotr  7356  isomin  7357  ovmpodv2  7591  difsnexi  7781  onint  7810  oneqmin  7820  ordunisuc2  7865  tfindsg  7882  findsg  7919  resf1extb  7956  f1oweALT  7997  el2mpocl  8111  poseq  8183  soseq  8184  ressuppss  8208  funsssuppss  8215  suppofssd  8228  smoiso  8402  seqomlem2  8491  oaordi  8584  oawordri  8588  oaordex  8596  oalimcl  8598  omwordi  8609  oewordi  8629  oelim2  8633  nnmwordi  8673  xpider  8828  iiner  8829  undifixp  8974  mptelixpg  8975  dom2lem  9032  findcard2s  9205  pssnn  9208  nneneq  9246  nneneqOLD  9258  fineqvlem  9298  dif1ennnALT  9311  unfilem2  9344  xpfiOLD  9359  domunfican  9361  f1dmvrnfibi  9381  fsuppimp  9408  dffi2  9463  infsupprpr  9544  wemaplem2  9587  suc11reg  9659  noinfep  9700  cantnflem1  9729  r1fin  9813  tcrank  9924  cardlim  10012  pr2nelemOLD  10043  fseqenlem1  10064  alephnbtwn  10111  alephord2i  10117  alephf1  10125  cardaleph  10129  alephiso  10138  dfac12lem2  10185  ackbij1lem16  10274  cflm  10290  cfcoflem  10312  sornom  10317  fin23lem27  10368  isf32lem7  10399  fin17  10434  fin1a2lem2  10441  fin1a2lem4  10443  fin1a2lem6  10445  fin1a2lem9  10448  axdc3lem2  10491  zorn2lem7  10542  uniimadom  10584  inar1  10815  grothomex  10869  addcanpi  10939  mulcanpi  10940  enqer  10961  genpcd  11046  genpnmax  11047  ltexprlem4  11079  reclem3pr  11089  reclem4pr  11090  suplem2pr  11093  axpre-ltadd  11207  axpre-sup  11209  ltletr  11353  00id  11436  addn0nid  11683  mul0or  11903  prodgt02  12115  lemul1a  12121  mulgt1OLD  12126  divgt0  12136  divge0  12137  ledivp1i  12193  ltdivp1i  12194  cju  12262  nnsub  12310  nominpos  12503  nn0n0n1ge2  12594  btwnnz  12694  suprfinzcl  12732  ublbneg  12975  zmax  12987  cnref1o  13027  ltsubrp  13071  ltaddrp  13072  xrltletr  13199  qbtwnre  13241  xltnegi  13258  xnn0xadd0  13289  iccsupr  13482  icoshft  13513  difreicc  13524  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  fzen  13581  elfz1b  13633  fzofzim  13749  eluzgtdifelfzo  13766  elfzo1elm1fzo0  13807  injresinjlem  13826  injresinj  13827  flval2  13854  flval3  13855  modmuladdim  13955  modaddmodup  13975  addmodlteq  13987  fseqsupubi  14019  ssnn0fi  14026  mptnn0fsuppr  14040  sq01  14264  hashf1rn  14391  hashgt12el  14461  hashgt12el2  14462  hashfundm  14481  hash2pr  14508  hash2exprb  14510  hashge2el2difr  14520  hashtpg  14524  hash3tr  14530  lswlgt0cl  14607  ccatalpha  14631  pfxfv  14720  pfxsuff1eqwrdeq  14737  ccatopth2  14755  swrdccat  14773  swrdccat3blem  14777  reuccatpfxs1lem  14784  repsdf2  14816  repswsymball  14817  repswrevw  14825  cshweqrep  14859  cshw1  14860  2cshwcshw  14864  scshwfzeqfzo  14865  cshwcsh2id  14867  swrdco  14876  swrd2lsw  14991  2swrd2eqwrdeq  14992  wwlktovfo  14997  cjre  15178  icodiamlt  15474  reusq0  15501  o1lo1  15573  o1of2  15649  o1rlimmul  15655  zsum  15754  modfsummods  15829  zprod  15973  reeff1  16156  dvdsmod0  16296  dvds2lem  16306  muldvds1  16318  dvdscmulr  16322  dvdsmulcr  16323  dvdsdivcl  16353  mod2eq1n2dvds  16384  oddnn02np1  16385  divalglem8  16437  ndvdsadd  16447  zeqzmulgcd  16547  dfgcd2  16583  absproddvds  16654  lcmftp  16673  coprmdvds  16690  2mulprm  16730  isprm5  16744  divgcdodd  16747  isprm6  16751  prmdvdsexpr  16754  prmdvdsbc  16763  cncongrprm  16766  phiprmpw  16813  modprm0  16843  pythagtriplem4  16857  pcz  16919  difsqpwdvds  16925  1arith  16965  prmgaplem5  17093  prmgaplem6  17094  cshwrepswhash1  17140  sbcie2s  17198  divsfval  17592  catsubcat  17884  fthmon  17974  isinitoi  18044  istermoi  18045  iszeroi  18054  setcmon  18132  setcepi  18133  funcestrcsetclem8  18192  fthestrcsetc  18195  funcsetcestrclem8  18207  fthsetcestrc  18210  odupos  18373  pltnle  18383  pltval3  18384  lublecllem  18405  latasym  18488  mrelatglb  18605  mrelatlub  18607  cnvpsb  18624  mgmpropd  18664  isgrpid2  18994  ghmghmrn  19253  ghmf1  19264  kerf1ghm  19265  orbsta  19331  resscntz  19351  gsmsymgrfixlem1  19445  gsmsymgreqlem2  19449  mndodcongi  19561  odf1  19580  lsmss1  19683  lsmss2  19685  efgredeu  19770  cntzcmnss  19859  imasabl  19894  lt6abl  19913  ablfaclem3  20107  ringinvnz1ne0  20297  0ringnnzr  20525  subrngringnsg  20553  srhmsubc  20680  domnmuln0  20709  lspsneq  21124  lspsneu  21125  lsmcv  21143  rnglidlmcl  21226  rngqiprngimf1lem  21304  lidldvgen  21344  domnchr  21547  znf1o  21570  zntoslem  21575  znfld  21579  cygznlem2a  21586  cygznlem3  21588  phlssphl  21677  islindf4  21858  uvcendim  21867  psdmul  22170  ply1scln0  22295  gsummoncoe1  22312  matvscl  22437  scmataddcl  22522  scmatsubcl  22523  scmatfo  22536  scmatghm  22539  maducoeval2  22646  slesolinv  22686  cramerimplem2  22690  cpmatelimp  22718  cpmatelimp2  22720  cpmatacl  22722  cpmatinvcl  22723  pm2mpf1  22805  cayhamlem1  22872  cayleyhamilton1  22898  0ntr  23079  islpi  23157  lmss  23306  cmpcld  23410  cmpfi  23416  1stcelcls  23469  comppfsc  23540  ptcnplem  23629  qtophmeo  23825  fbdmn0  23842  fbasrn  23892  elfm3  23958  fmfnfmlem4  23965  fclscf  24033  cnpfcf  24049  alexsubALTlem3  24057  tsmsres  24152  blval2  24575  tnggrpr  24676  nmoleub  24752  nmhmcn  25153  ncvs1  25191  iscau4  25313  caussi  25331  cmssmscld  25384  cmslssbn  25406  cniccbdd  25496  ovoliunnul  25542  mbfinf  25700  itg2splitlem  25783  dvcn  25957  c1lip1  26036  c1lip3  26038  dvcnvrelem1  26056  dvfsumlem2  26067  ply1divex  26176  quotcan  26351  aannenlem1  26370  taylf  26402  taylthlem2  26416  ulmcaulem  26437  ulmcau  26438  reeff1o  26491  logccv  26705  rtprmirr  26803  logreclem  26805  isosctrlem2  26862  xrlimcnp  27011  rlimcxp  27017  ftalem7  27122  vmappw  27159  fsumdvdsmul  27238  fsumvma  27257  dchreq  27302  dchrptlem1  27308  dchrsum  27313  bposlem7  27334  lgsqrlem2  27391  lgsdchr  27399  gausslemma2dlem1a  27409  lgseisenlem2  27420  lgsquad2  27430  2lgslem1b  27436  2sqlem6  27467  2sqnn0  27482  addsq2reu  27484  2sqreulem2  27496  sltval2  27701  sltres  27707  nodenselem8  27736  nodense  27737  noresle  27742  scutun12  27855  madeval2  27892  elmade  27906  negsf1o  28086  muls0ord  28211  recsex  28243  noseqrdgfn  28312  n0subs  28360  eln0zs  28386  tgcgrcomimp  28485  isperp2  28723  xmstrkgc  28900  brbtwn  28914  brcgr  28915  axcgrid  28931  axeuclidlem  28977  axeuclid  28978  elntg2  29000  lpvtx  29085  upgrex  29109  upgrpredgv  29156  upgredgpr  29159  uhgr0v0e  29255  subgrprop  29290  fusgrfisbase  29345  edgnbusgreu  29384  nbusgredgeu0  29385  cusgredg  29441  structtocusgr  29463  cusgrsize2inds  29471  cusgrsize  29472  usgredgsscusgredg  29477  fusgrmaxsize  29482  uspgrloopvtxel  29534  umgr2v2e  29543  vtxdginducedm1fi  29562  finsumvtxdg2sstep  29567  rgrprop  29578  rusgrprop  29580  0uhgrrusgr  29596  rusgrpropedg  29602  ewlkprop  29621  upgrewlkle2  29624  wlkprop  29629  upgrwlkcompim  29661  uspgr2wlkeq  29664  wlklenvclwlk  29673  wlkonprop  29676  wlkres  29688  redwlk  29690  wlkdlem2  29701  wksonproplem  29722  wksonproplemOLD  29723  usgr2trlspth  29781  usgr2pth  29784  pthdlem1  29786  crctcshwlkn0lem4  29833  wwlksnprcl  29859  wlkiswwlks2  29895  wwlksm1edg  29901  wlknewwlksn  29907  wwlksnred  29912  wwlksnextbi  29914  wwlksnextwrd  29917  wwlksnextinj  29919  wwlksnextsurj  29920  umgr2wlk  29969  umgrwwlks2on  29977  elwwlks2  29986  clwwlk1loop  30007  umgrclwwlkge2  30010  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlkfo  30028  clwwisshclwwslemlem  30032  clwwlknwwlksn  30057  clwwlknlbonbgr1  30058  clwwlkn1loopb  30062  clwwlkf  30066  clwwlknon1  30116  clwwlknonwwlknonb  30125  clwwlknonex2lem2  30127  vdn0conngrumgrv2  30215  frgrnbnb  30312  frgrncvvdeqlem2  30319  frgrncvvdeqlem3  30320  frgrncvvdeqlem6  30323  frgrwopreglem4a  30329  fusgr2wsp2nb  30353  frrusgrord0lem  30358  numclwwlk2lem1lem  30361  2clwwlk2clwwlklem  30365  2clwwlk2clwwlk  30369  numclwwlk1lem2foa  30373  numclwwlk1lem2f1  30376  frgrreg  30413  hlipgt0  30933  ocin  31315  ocnel  31317  shmodsi  31408  pjmf1  31735  unopf1o  31935  staddi  32265  stadd3i  32267  mdi  32314  dmdmd  32319  dmdi  32321  dmdbr2  32322  dmdbr3  32324  dmdbr4  32325  dmdi4  32326  mdsl1i  32340  superpos  32373  cvbr4i  32386  atssma  32397  atcv1  32399  atomli  32401  chirredlem1  32409  addltmulALT  32465  bian1dOLD  32476  ifeqeqx  32555  disjxpin  32601  suppss3  32735  fpwrelmap  32744  expgt0b  32818  mndlactfo  33032  mndractfo  33034  ogrpaddlt  33094  qsfld  33526  ply1degltdimlem  33673  ply1degltdim  33674  metider  33893  tpr2rico  33911  xrge0iifiso  33934  qqhcn  33992  qqhucn  33993  esumlub  34061  esumpinfval  34074  esumpinfsum  34078  ballotlemfc0  34495  ballotlemfcc  34496  ftc2re  34613  bnj517  34899  axsepg2  35096  axsepg2ALT  35097  fnrelpredd  35103  axnulg  35106  pfxwlk  35129  subgrwlk  35137  loop1cycl  35142  erdsze2lem2  35209  satfv1  35368  satfdmlem  35373  satf0op  35382  fmlasuc  35391  dfrdg4  35952  altopthsn  35962  btwncomim  36014  btwnexch3  36021  btwnexch2  36024  endofsegid  36086  opnrebl2  36322  nn0prpwlem  36323  onsuct0  36442  ordcmp  36448  nndivsub  36458  dnibndlem13  36491  bj-cbval  36650  bj-cbvex  36651  bj-cbvexw  36677  bj-cbv3tb  36788  bj-spimtv  36795  bj-equsal  36827  bj-sbsb  36838  bj-vtoclf  36916  bj-zfauscl  36925  bj-gabss  36936  bj-gabeqd  36938  currysetlem2  36949  bj-snsetex  36964  bj-ismooredr2  37111  bj-inftyexpiinj  37210  bj-finsumval0  37286  bj-fvimacnv0  37287  bj-bary1lem1  37312  bj-bary1  37313  f1omptsnlem  37337  iooelexlt  37363  relowlpssretop  37365  rdgeqoa  37371  finxpsuclem  37398  fvineqsneq  37413  pibt2  37418  wl-isseteq  37506  wl-equsal1i  37545  wl-ax11-lem10  37595  ltflcei  37615  sin2h  37617  cos2h  37618  tan2h  37619  lindsenlbs  37622  matunitlindf  37625  poimirlem3  37630  poimirlem4  37631  poimirlem18  37645  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  poimir  37660  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  mbfresfi  37673  cnambfre  37675  ftc1anc  37708  dvasin  37711  areacirclem1  37715  areacirclem4  37718  areacirc  37720  brabg2  37724  fzmul  37748  fdc  37752  incsequz2  37756  isbnd2  37790  opidonOLD  37859  opidon2OLD  37861  grpomndo  37882  elghomlem2OLD  37893  rngoueqz  37947  dvrunz  37961  divrngidl  38035  refressn  38444  dral1-o  38905  lsatn0  39000  l1cvpat  39055  leat2  39295  atnle  39318  cvlcvr1  39340  cvrexchlem  39421  cvratlem  39423  cvrat  39424  atcvrj0  39430  atle  39438  snatpsubN  39752  linepsubN  39754  pmapsub  39770  lneq2at  39780  lncvrelatN  39783  2llnma3r  39790  cdlemblem  39795  paddasslem5  39826  poml4N  39955  lhpmcvr4N  40028  trlval2  40165  cdlemd6  40205  cdleme7ga  40250  cdleme25b  40356  cdleme29b  40377  cdleme35fnpq  40451  cdleme50f1  40545  cdlemf1  40563  cdlemg27b  40698  cdlemk28-3  40910  tendospcanN  41025  diaf11N  41051  dia2dimlem1  41066  dibf11N  41163  dihf11  41269  dihmeetlem1N  41292  dochvalr  41359  dochnel2  41394  dvh4dimlem  41445  dochsat0  41459  mapd1o  41650  hdmapf1oN  41867  hgmapval0  41894  hgmapf1oN  41905  hlhilhillem  41966  nnproddivdvdsd  42001  lcmineqlem  42053  aks4d1p1p5  42076  aks4d1p3  42079  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  fldhmf1  42091  isprimroot2  42095  primrootsunit1  42098  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootlekpowne0  42106  primrootspoweq0  42107  aks6d1c1p1  42108  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  aks6d1c1p7  42114  aks6d1c1p6  42115  aks6d1c1p8  42116  aks6d1c2p2  42120  aks6d1c2lem3  42127  aks6d1c2lem4  42128  hashnexinj  42129  hashnexinjle  42130  aks6d1c2  42131  aks6d1c5lem0  42136  aks6d1c5lem1  42137  aks6d1c5  42140  sticksstones1  42147  sticksstones3  42149  sticksstones8  42154  sticksstones11  42157  sticksstones12  42159  sticksstones20  42167  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  aks6d1c7  42185  rhmqusspan  42186  unitscyglem2  42197  unitscyglem3  42198  aks5lem8  42202  metakunt7  42212  sn-axprlem3  42256  oexpreposd  42357  frlmsnic  42550  fsuppind  42600  prjspval  42613  rexrabdioph  42805  fphpdo  42828  irrapxlem3  42835  rmxypairf1o  42923  rmxycomplete  42929  zindbi  42958  lermxnn0  42962  ltrmy  42964  rmyeq0  42965  rmyeq  42966  lermy  42967  acongsym  42988  acongneg2  42989  wepwsolem  43054  onsupuni  43241  onsupmaxb  43251  onsucf1o  43285  onov0suclim  43287  oe0suclim  43290  onsucwordi  43301  cantnfresb  43337  omabs2  43345  tfsconcat0b  43359  tfsconcatrev  43361  naddcnffo  43377  oaun3lem1  43387  oaltom  43418  omltoe  43420  sdomne0  43426  sdomne0d  43427  safesnsupfidom1o  43430  intabssd  43532  iscard4  43546  ss2iundf  43672  frege129d  43776  frege133d  43778  axfrege52a  43869  axfrege52c  43900  ntrk0kbimka  44052  gneispace  44147  suprleubrd  44179  suprlubrd  44181  radcnvrat  44333  nzss  44336  expgrowthi  44352  ordpss  44470  bi23impib  44506  rspsbc2  44554  tratrb  44556  sbcim2g  44558  truniALT  44561  3impcombi  44837  tpid3gVD  44862  orbi1rVD  44868  sbc3orgVD  44871  rspsbc2VD  44875  tratrbVD  44881  sbcim2gVD  44895  sbcbiVD  44896  truniALTVD  44898  trintALTVD  44900  trintALT  44901  csbingVD  44904  csbsngVD  44913  csbxpgVD  44914  csbresgVD  44915  csbrngVD  44916  csbima12gALTVD  44917  csbunigVD  44918  csbfv12gALTVD  44919  relopabVD  44921  isosctrlem1ALT  44954  relpfrlem  44974  trfr  44979  fzisoeu  45312  xrralrecnnge  45401  allbutfi  45404  climinf  45621  liminfreuzlem  45817  climliminf  45821  climliminflimsup  45823  xlimpnfxnegmnf  45829  xlimbr  45842  stoweidlem7  46022  stoweidlem62  46077  sge0gerpmpt  46417  meaiuninclem  46495  carageniuncllem2  46537  issmflem  46742  et-sqrtnegnre  46888  ormkglobd  46890  natlocalincr  46891  tworepnotupword  46901  funressnfv  47055  funressnvmo  47057  f1cof1b  47089  2reu3  47122  ralbinrald  47134  afv0fv0  47161  afv0nbfvbi  47163  afvfv0bi  47164  fnbrafvb  47166  afvres  47184  tz6.12-afv  47185  afvco2  47188  ndmaovcl  47215  afv2res  47251  tz6.12-afv2  47252  nelbrim  47287  f1oresf1o2  47303  zm1nn  47314  nltle2tri  47325  subsubelfzo0  47338  iccpartres  47405  iccpartiltu  47409  fargshiftfv  47426  ichnreuop  47459  ichreuopeq  47460  prsprel  47474  sprsymrelf1lem  47478  sprsymrelfolem2  47480  sprsymrelfo  47484  prpair  47488  paireqne  47498  sbcpr  47508  fmtnof1  47522  goldbachthlem2  47533  fmtnoprmfac1  47552  fmtnoprmfac2  47554  lighneallem2  47593  lighneallem4b  47596  lighneallem4  47597  evennodd  47630  oddneven  47631  oexpnegnz  47665  evenltle  47704  fpprwppr  47726  fpprwpprb  47727  gbowge7  47750  gbege6  47752  sbgoldbwt  47764  sbgoldbst  47765  nnsum3primesle9  47781  bgoldbtbndlem2  47793  grimprop  47869  isuspgrimlem  47874  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901  grtriproplem  47906  isgrtri  47910  grimgrtri  47916  stgr1  47928  isubgr3stgr  47942  grlimprop  47951  uspgrlimlem2  47956  uspgrlimlem3  47957  2tceilhalfelfzo1  48018  gpg5nbgrvtx13starlem1  48027  clintop  48124  isassintop  48126  lidldomn1  48147  uzlidlring  48151  2zrngnmlid2  48173  rngccatidALTV  48188  ringccatidALTV  48222  srhmsubcALTV  48241  ztprmneprm  48263  pgrpgt2nabl  48282  lindslinindimp2lem4  48378  lincresunit3  48398  fldivexpfllog2  48486  digexp  48528  naryfvalelfv  48553  affinecomb1  48623  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  eenglngeehlnm  48660  itscnhlc0yqe  48680  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  itsclquadeu  48698  inlinecirc02plem  48707  inlinecirc02p  48708  pm4.71da  48710  mofsn  48753  seposep  48823  idmon  48908  idepi  48909  prsthinc  49111  grptcmon  49190  grptcepi  49191  spd  49197  spcdvw  49198  setrec2fun  49211