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  1834  spvv  1989  spfw  2034  cbvalw  2036  sbequi  2089  chvarfv  2245  cbvalv1  2343  spv  2395  chvar  2397  cbval  2400  sb1  2480  nfsb4t  2501  exmoeu  2578  euim  2614  2eu3  2651  eqrdav  2732  ralbida  3244  rgen2a  3338  ralcom2  3344  ceqsalt  3471  ceqsalgALT  3474  spcimgft  3500  vtoclegft  3540  spcdv  3545  rspcdv  3565  rspcebdv  3567  rexraleqim  3598  sbcn1  3790  sbcbi1  3795  sbeqalb  3800  sbcel21v  3805  elpwunsn  4638  rabsnifsb  4676  ssunsn2  4780  preqr1g  4805  iuneqconst  4955  axprlem3  5367  axprlem3OLD  5370  sbcop1  5433  propeqop  5452  euotd  5458  rexopabb  5473  sotr2  5563  relop  5796  elinxp  5975  elimasni  6047  sotri2  6083  onmindif  6408  dffv2  6926  mpteqb  6957  elfvmptrab  6967  chfnrn  6991  elpreima  7000  iinpreima  7011  exfo  7047  ffnfv  7061  f1elima  7206  f1ounsn  7215  f1eqcocnv  7244  fliftfun  7255  soisores  7270  isotr  7279  isomin  7280  ovmpodv2  7513  difsnexi  7703  onint  7732  oneqmin  7742  ordunisuc2  7783  tfindsg  7800  findsg  7836  resf1extb  7873  f1oweALT  7913  el2mpocl  8025  poseq  8097  soseq  8098  ressuppss  8122  funsssuppss  8129  suppofssd  8142  smoiso  8291  seqomlem2  8379  oaordi  8470  oawordri  8474  oaordex  8482  oalimcl  8484  omwordi  8495  oewordi  8515  oelim2  8519  nnmwordi  8559  xpider  8721  iiner  8722  undifixp  8868  mptelixpg  8869  dom2lem  8925  findcard2s  9086  pssnn  9089  nneneq  9126  fineqvlem  9161  dif1ennnALT  9172  unfilem2  9201  domunfican  9217  f1dmvrnfibi  9236  fsuppimp  9263  dffi2  9318  infsupprpr  9401  wemaplem2  9444  suc11reg  9520  noinfep  9561  cantnflem1  9590  r1fin  9677  tcrank  9788  cardlim  9876  fseqenlem1  9926  alephnbtwn  9973  alephord2i  9979  alephf1  9987  cardaleph  9991  alephiso  10000  dfac12lem2  10047  ackbij1lem16  10136  cflm  10152  cfcoflem  10174  sornom  10179  fin23lem27  10230  isf32lem7  10261  fin17  10296  fin1a2lem2  10303  fin1a2lem4  10305  fin1a2lem6  10307  fin1a2lem9  10310  axdc3lem2  10353  zorn2lem7  10404  uniimadom  10446  inar1  10677  grothomex  10731  addcanpi  10801  mulcanpi  10802  enqer  10823  genpcd  10908  genpnmax  10909  ltexprlem4  10941  reclem3pr  10951  reclem4pr  10952  suplem2pr  10955  axpre-ltadd  11069  axpre-sup  11071  ltletr  11216  00id  11299  addn0nid  11548  mul0or  11768  prodgt02  11980  lemul1a  11986  mulgt1OLD  11991  divgt0  12001  divge0  12002  ledivp1i  12058  ltdivp1i  12059  cju  12132  nnsub  12180  nominpos  12369  nn0n0n1ge2  12460  btwnnz  12559  suprfinzcl  12597  ublbneg  12837  zmax  12849  cnref1o  12889  ltsubrp  12934  ltaddrp  12935  xrltletr  13062  qbtwnre  13105  xltnegi  13122  xnn0xadd0  13153  iccsupr  13349  icoshft  13380  difreicc  13391  iccshftri  13394  iccshftli  13396  iccdili  13398  icccntri  13400  fzen  13448  elfz1b  13500  fzofzim  13616  eluzgtdifelfzo  13634  elfzo1elm1fzo0  13675  injresinjlem  13697  injresinj  13698  flval2  13725  flval3  13726  modmuladdim  13828  modaddmodup  13848  addmodlteq  13860  fseqsupubi  13892  ssnn0fi  13899  mptnn0fsuppr  13913  sq01  14139  hashf1rn  14266  hashgt12el  14336  hashgt12el2  14337  hashfundm  14356  hash2pr  14383  hash2exprb  14385  hashge2el2difr  14395  hashtpg  14399  hash3tr  14405  lswlgt0cl  14483  ccatalpha  14508  pfxfv  14597  pfxsuff1eqwrdeq  14613  ccatopth2  14631  swrdccat  14649  swrdccat3blem  14653  reuccatpfxs1lem  14660  repsdf2  14692  repswsymball  14693  repswrevw  14701  cshweqrep  14735  cshw1  14736  2cshwcshw  14739  scshwfzeqfzo  14740  cshwcsh2id  14742  swrdco  14751  swrd2lsw  14866  2swrd2eqwrdeq  14867  wwlktovfo  14872  cjre  15053  icodiamlt  15352  reusq0  15379  o1lo1  15451  o1of2  15527  o1rlimmul  15533  zsum  15632  modfsummods  15707  zprod  15851  reeff1  16036  dvdsmod0  16176  dvds2lem  16186  muldvds1  16198  dvdscmulr  16202  dvdsmulcr  16203  dvdsdivcl  16234  mod2eq1n2dvds  16265  oddnn02np1  16266  divalglem8  16318  ndvdsadd  16328  zeqzmulgcd  16428  dfgcd2  16464  absproddvds  16535  lcmftp  16554  coprmdvds  16571  2mulprm  16611  isprm5  16625  divgcdodd  16628  isprm6  16632  prmdvdsexpr  16635  prmdvdsbc  16644  cncongrprm  16647  phiprmpw  16694  modprm0  16724  pythagtriplem4  16738  pcz  16800  difsqpwdvds  16806  1arith  16846  prmgaplem5  16974  prmgaplem6  16975  cshwrepswhash1  17021  sbcie2s  17079  divsfval  17459  catsubcat  17754  fthmon  17844  isinitoi  17914  istermoi  17915  iszeroi  17924  setcmon  18002  setcepi  18003  funcestrcsetclem8  18061  fthestrcsetc  18064  funcsetcestrclem8  18076  fthsetcestrc  18079  odupos  18240  pltnle  18250  pltval3  18251  lublecllem  18272  latasym  18357  mrelatglb  18474  mrelatlub  18476  cnvpsb  18493  chninf  18549  mgmpropd  18567  isgrpid2  18897  ghmghmrn  19155  ghmf1  19166  kerf1ghm  19167  orbsta  19233  resscntz  19253  gsmsymgrfixlem1  19347  gsmsymgreqlem2  19351  mndodcongi  19463  odf1  19482  lsmss1  19585  lsmss2  19587  efgredeu  19672  cntzcmnss  19761  imasabl  19796  lt6abl  19815  ablfaclem3  20009  ogrpaddlt  20058  ringinvnz1ne0  20226  0ringnnzr  20449  subrngringnsg  20477  srhmsubc  20604  domnmuln0  20633  lspsneq  21068  lspsneu  21069  lsmcv  21087  rnglidlmcl  21162  rngqiprngimf1lem  21240  lidldvgen  21280  domnchr  21478  znf1o  21497  zntoslem  21502  znfld  21506  cygznlem2a  21513  cygznlem3  21515  phlssphl  21605  islindf4  21784  uvcendim  21793  psdmul  22100  ply1scln0  22225  gsummoncoe1  22243  matvscl  22366  scmataddcl  22451  scmatsubcl  22452  scmatfo  22465  scmatghm  22468  maducoeval2  22575  slesolinv  22615  cramerimplem2  22619  cpmatelimp  22647  cpmatelimp2  22649  cpmatacl  22651  cpmatinvcl  22652  pm2mpf1  22734  cayhamlem1  22801  cayleyhamilton1  22827  0ntr  23006  islpi  23084  lmss  23233  cmpcld  23337  cmpfi  23343  1stcelcls  23396  comppfsc  23467  ptcnplem  23556  qtophmeo  23752  fbdmn0  23769  fbasrn  23819  elfm3  23885  fmfnfmlem4  23892  fclscf  23960  cnpfcf  23976  alexsubALTlem3  23984  tsmsres  24079  blval2  24497  tnggrpr  24590  nmoleub  24666  nmhmcn  25067  ncvs1  25104  iscau4  25226  caussi  25244  cmssmscld  25297  cmslssbn  25319  cniccbdd  25409  ovoliunnul  25455  mbfinf  25613  itg2splitlem  25696  dvcn  25870  c1lip1  25949  c1lip3  25951  dvcnvrelem1  25969  dvfsumlem2  25980  ply1divex  26089  quotcan  26264  aannenlem1  26283  taylf  26315  taylthlem2  26329  ulmcaulem  26350  ulmcau  26351  reeff1o  26404  logccv  26619  rtprmirr  26717  logreclem  26719  isosctrlem2  26776  xrlimcnp  26925  rlimcxp  26931  ftalem7  27036  vmappw  27073  fsumdvdsmul  27152  fsumvma  27171  dchreq  27216  dchrptlem1  27222  dchrsum  27227  bposlem7  27248  lgsqrlem2  27305  lgsdchr  27313  gausslemma2dlem1a  27323  lgseisenlem2  27334  lgsquad2  27344  2lgslem1b  27350  2sqlem6  27381  2sqnn0  27396  addsq2reu  27398  2sqreulem2  27410  sltval2  27615  sltres  27621  nodenselem8  27650  nodense  27651  noresle  27656  scutun12  27771  madeval2  27814  elmade  27832  negsf1o  28016  muls0ord  28144  recsex  28177  bdayon  28229  noseqrdgfn  28256  n0subs  28309  eln0zs  28344  zsoring  28352  tgcgrcomimp  28475  isperp2  28713  xmstrkgc  28884  brbtwn  28898  brcgr  28899  axcgrid  28915  axeuclidlem  28961  axeuclid  28962  elntg2  28984  lpvtx  29067  upgrex  29091  upgrpredgv  29138  upgredgpr  29141  uhgr0v0e  29237  subgrprop  29272  fusgrfisbase  29327  edgnbusgreu  29366  nbusgredgeu0  29367  cusgredg  29423  structtocusgr  29445  cusgrsize2inds  29453  cusgrsize  29454  usgredgsscusgredg  29459  fusgrmaxsize  29464  uspgrloopvtxel  29516  umgr2v2e  29525  vtxdginducedm1fi  29544  finsumvtxdg2sstep  29549  rgrprop  29560  rusgrprop  29562  0uhgrrusgr  29578  rusgrpropedg  29584  ewlkprop  29603  upgrewlkle2  29606  wlkprop  29611  upgrwlkcompim  29642  uspgr2wlkeq  29645  wlklenvclwlk  29653  wlkonprop  29656  wlkres  29668  redwlk  29670  wlkdlem2  29681  wksonproplem  29702  usgr2trlspth  29760  usgr2pth  29763  pthdlem1  29765  crctcshwlkn0lem4  29812  wwlksnprcl  29838  wlkiswwlks2  29874  wwlksm1edg  29880  wlknewwlksn  29886  wwlksnred  29891  wwlksnextbi  29893  wwlksnextwrd  29896  wwlksnextinj  29898  wwlksnextsurj  29899  umgr2wlk  29948  usgrwwlks2on  29957  umgrwwlks2on  29958  elwwlks2  29968  clwwlk1loop  29989  umgrclwwlkge2  29992  clwlkclwwlklem2a1  29993  clwlkclwwlklem2a4  29998  clwlkclwwlklem2a  29999  clwlkclwwlklem2  30001  clwlkclwwlkfo  30010  clwwisshclwwslemlem  30014  clwwlknwwlksn  30039  clwwlknlbonbgr1  30040  clwwlkn1loopb  30044  clwwlkf  30048  clwwlknon1  30098  clwwlknonwwlknonb  30107  clwwlknonex2lem2  30109  vdn0conngrumgrv2  30197  frgrnbnb  30294  frgrncvvdeqlem2  30301  frgrncvvdeqlem3  30302  frgrncvvdeqlem6  30305  frgrwopreglem4a  30311  fusgr2wsp2nb  30335  frrusgrord0lem  30340  numclwwlk2lem1lem  30343  2clwwlk2clwwlklem  30347  2clwwlk2clwwlk  30351  numclwwlk1lem2foa  30355  numclwwlk1lem2f1  30358  frgrreg  30395  hlipgt0  30915  ocin  31297  ocnel  31299  shmodsi  31390  pjmf1  31717  unopf1o  31917  staddi  32247  stadd3i  32249  mdi  32296  dmdmd  32301  dmdi  32303  dmdbr2  32304  dmdbr3  32306  dmdbr4  32307  dmdi4  32308  mdsl1i  32322  superpos  32355  cvbr4i  32368  atssma  32379  atcv1  32381  atomli  32383  chirredlem1  32391  addltmulALT  32447  bian1dOLD  32457  ifeqeqx  32543  disjxpin  32589  suppss3  32730  fpwrelmap  32740  expgt0b  32825  mndlactfo  33037  mndractfo  33039  qsfld  33507  ply1degltdimlem  33707  ply1degltdim  33708  metider  33979  tpr2rico  33997  xrge0iifiso  34020  qqhcn  34076  qqhucn  34077  esumlub  34145  esumpinfval  34158  esumpinfsum  34162  ballotlemfc0  34578  ballotlemfcc  34579  ftc2re  34683  bnj517  34969  axsepg2  35166  axsepg2ALT  35167  fnrelpredd  35174  rankfilimbi  35184  axnulg  35191  pfxwlk  35240  subgrwlk  35248  loop1cycl  35253  erdsze2lem2  35320  satfv1  35479  satfdmlem  35484  satf0op  35493  fmlasuc  35502  dfrdg4  36067  altopthsn  36077  btwncomim  36129  btwnexch3  36136  btwnexch2  36139  endofsegid  36201  opnrebl2  36437  nn0prpwlem  36438  onsuct0  36557  ordcmp  36563  nndivsub  36573  dnibndlem13  36606  bj-cbval  36765  bj-cbvex  36766  bj-cbvexw  36793  bj-cbv3tb  36904  bj-spimtv  36911  bj-equsal  36943  bj-sbsb  36954  bj-vtoclf  37032  bj-zfauscl  37041  bj-gabss  37052  bj-gabeqd  37054  currysetlem2  37065  bj-snsetex  37080  bj-ismooredr2  37227  bj-inftyexpiinj  37326  bj-finsumval0  37402  bj-fvimacnv0  37403  bj-bary1lem1  37428  bj-bary1  37429  f1omptsnlem  37453  iooelexlt  37479  relowlpssretop  37481  rdgeqoa  37487  finxpsuclem  37514  fvineqsneq  37529  pibt2  37534  wl-isseteq  37622  wl-equsal1i  37661  ltflcei  37721  sin2h  37723  cos2h  37724  tan2h  37725  lindsenlbs  37728  matunitlindf  37731  poimirlem3  37736  poimirlem4  37737  poimirlem18  37751  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem24  37757  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  poimirlem31  37764  poimir  37766  heicant  37768  mblfinlem1  37770  mblfinlem2  37771  mblfinlem3  37772  mblfinlem4  37773  mbfresfi  37779  cnambfre  37781  ftc1anc  37814  dvasin  37817  areacirclem1  37821  areacirclem4  37824  areacirc  37826  brabg2  37830  fzmul  37854  fdc  37858  incsequz2  37862  isbnd2  37896  opidonOLD  37965  opidon2OLD  37967  grpomndo  37988  elghomlem2OLD  37999  rngoueqz  38053  dvrunz  38067  divrngidl  38141  refressn  38618  dral1-o  39076  lsatn0  39171  l1cvpat  39226  leat2  39466  atnle  39489  cvlcvr1  39511  cvrexchlem  39591  cvratlem  39593  cvrat  39594  atcvrj0  39600  atle  39608  snatpsubN  39922  linepsubN  39924  pmapsub  39940  lneq2at  39950  lncvrelatN  39953  2llnma3r  39960  cdlemblem  39965  paddasslem5  39996  poml4N  40125  lhpmcvr4N  40198  trlval2  40335  cdlemd6  40375  cdleme7ga  40420  cdleme25b  40526  cdleme29b  40547  cdleme35fnpq  40621  cdleme50f1  40715  cdlemf1  40733  cdlemg27b  40868  cdlemk28-3  41080  tendospcanN  41195  diaf11N  41221  dia2dimlem1  41236  dibf11N  41333  dihf11  41439  dihmeetlem1N  41462  dochvalr  41529  dochnel2  41564  dvh4dimlem  41615  dochsat0  41629  mapd1o  41820  hdmapf1oN  42037  hgmapval0  42064  hgmapf1oN  42075  hlhilhillem  42132  nnproddivdvdsd  42166  lcmineqlem  42218  aks4d1p1p5  42241  aks4d1p3  42244  aks4d1p8d2  42251  aks4d1p8  42253  aks4d1p9  42254  fldhmf1  42256  isprimroot2  42260  primrootsunit1  42263  primrootscoprmpow  42265  posbezout  42266  primrootscoprbij  42268  primrootlekpowne0  42271  primrootspoweq0  42272  aks6d1c1p1  42273  aks6d1c1p2  42275  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p7  42279  aks6d1c1p6  42280  aks6d1c1p8  42281  aks6d1c2p2  42285  aks6d1c2lem3  42292  aks6d1c2lem4  42293  hashnexinj  42294  hashnexinjle  42295  aks6d1c2  42296  aks6d1c5lem0  42301  aks6d1c5lem1  42302  aks6d1c5  42305  sticksstones1  42312  sticksstones3  42314  sticksstones8  42319  sticksstones11  42322  sticksstones12  42324  sticksstones20  42332  sticksstones22  42334  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c6isolem1  42340  aks6d1c6isolem2  42341  aks6d1c6lem5  42343  aks6d1c7  42350  rhmqusspan  42351  unitscyglem2  42362  unitscyglem3  42363  aks5lem8  42367  sn-axprlem3  42388  oexpreposd  42492  sn-remul0ord  42578  frlmsnic  42710  fsuppind  42748  prjspval  42761  rexrabdioph  42951  fphpdo  42974  irrapxlem3  42981  rmxypairf1o  43068  rmxycomplete  43074  zindbi  43103  lermxnn0  43107  ltrmy  43109  rmyeq0  43110  rmyeq  43111  lermy  43112  acongsym  43133  acongneg2  43134  wepwsolem  43199  onsupuni  43386  onsupmaxb  43396  onsucf1o  43429  onov0suclim  43431  oe0suclim  43434  onsucwordi  43445  cantnfresb  43481  omabs2  43489  tfsconcat0b  43503  tfsconcatrev  43505  naddcnffo  43521  oaun3lem1  43531  oaltom  43562  omltoe  43564  sdomne0  43570  sdomne0d  43571  safesnsupfidom1o  43574  intabssd  43676  iscard4  43690  ss2iundf  43816  frege129d  43920  frege133d  43922  axfrege52a  44013  axfrege52c  44044  ntrk0kbimka  44196  gneispace  44291  suprleubrd  44323  suprlubrd  44325  radcnvrat  44471  nzss  44474  expgrowthi  44490  ordpss  44607  bi23impib  44643  rspsbc2  44691  tratrb  44693  sbcim2g  44695  truniALT  44698  3impcombi  44973  tpid3gVD  44998  orbi1rVD  45004  sbc3orgVD  45007  rspsbc2VD  45011  tratrbVD  45017  sbcim2gVD  45031  sbcbiVD  45032  truniALTVD  45034  trintALTVD  45036  trintALT  45037  csbingVD  45040  csbsngVD  45049  csbxpgVD  45050  csbresgVD  45051  csbrngVD  45052  csbima12gALTVD  45053  csbunigVD  45054  csbfv12gALTVD  45055  relopabVD  45057  isosctrlem1ALT  45090  relpfrlem  45110  trfr  45119  fzisoeu  45464  xrralrecnnge  45550  allbutfi  45553  climinf  45768  liminfreuzlem  45962  climliminf  45966  climliminflimsup  45968  xlimpnfxnegmnf  45974  xlimbr  45987  stoweidlem7  46167  stoweidlem62  46222  sge0gerpmpt  46562  meaiuninclem  46640  carageniuncllem2  46682  issmflem  46887  et-sqrtnegnre  47033  ormkglobd  47035  natlocalincr  47036  funressnfv  47205  funressnvmo  47207  f1cof1b  47239  2reu3  47272  ralbinrald  47284  afv0fv0  47311  afv0nbfvbi  47313  afvfv0bi  47314  fnbrafvb  47316  afvres  47334  tz6.12-afv  47335  afvco2  47338  ndmaovcl  47365  afv2res  47401  tz6.12-afv2  47402  nelbrim  47437  f1oresf1o2  47453  zm1nn  47464  nltle2tri  47475  subsubelfzo0  47488  2tceilhalfelfzo1  47494  iccpartres  47580  iccpartiltu  47584  fargshiftfv  47601  ichnreuop  47634  ichreuopeq  47635  prsprel  47649  sprsymrelf1lem  47653  sprsymrelfolem2  47655  sprsymrelfo  47659  prpair  47663  paireqne  47673  sbcpr  47683  fmtnof1  47697  goldbachthlem2  47708  fmtnoprmfac1  47727  fmtnoprmfac2  47729  lighneallem2  47768  lighneallem4b  47771  lighneallem4  47772  evennodd  47805  oddneven  47806  oexpnegnz  47840  evenltle  47879  fpprwppr  47901  fpprwpprb  47902  gbowge7  47925  gbege6  47927  sbgoldbwt  47939  sbgoldbst  47940  nnsum3primesle9  47956  bgoldbtbndlem2  47968  grimprop  48045  isuspgrimlem  48057  uhgrimisgrgriclem  48092  clnbgrgrimlem  48095  grtriproplem  48101  isgrtri  48105  grimgrtri  48111  stgr1  48123  isubgr3stgr  48137  grlimprop  48146  uspgrlimlem2  48151  uspgrlimlem3  48152  grlimprclnbgr  48158  gpg5nbgrvtx13starlem1  48233  clintop  48370  isassintop  48372  lidldomn1  48393  uzlidlring  48397  2zrngnmlid2  48419  rngccatidALTV  48434  ringccatidALTV  48468  srhmsubcALTV  48487  ztprmneprm  48509  pgrpgt2nabl  48528  lindslinindimp2lem4  48623  lincresunit3  48643  fldivexpfllog2  48727  digexp  48769  naryfvalelfv  48794  affinecomb1  48864  eenglngeehlnmlem1  48899  eenglngeehlnmlem2  48900  eenglngeehlnm  48901  itscnhlc0yqe  48921  itsclc0yqsol  48926  itscnhlc0xyqsol  48927  itschlc0xyqsol1  48928  itschlc0xyqsol  48929  itsclquadeu  48939  inlinecirc02plem  48948  inlinecirc02p  48949  pm4.71da  48951  mofsn  49005  seposep  49087  resipos  49136  idmon  49181  idepi  49182  prsthinc  49625  grptcmon  49754  grptcepi  49755  spd  49839  spcdvw  49840  setrec2fun  49853