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  2087  chvarfv  2243  cbvalv1  2341  spv  2393  chvar  2395  cbval  2398  sb1  2478  nfsb4t  2499  exmoeu  2576  euim  2612  2eu3  2649  eqrdav  2730  ralbida  3243  rgen2a  3337  ralcom2  3343  ceqsalt  3470  ceqsalgALT  3473  spcimgft  3499  vtoclegft  3539  spcdv  3544  rspcdv  3564  rspcebdv  3566  rexraleqim  3597  sbcn1  3789  sbcbi1  3794  sbeqalb  3799  sbcel21v  3804  elpwunsn  4634  rabsnifsb  4672  ssunsn2  4776  preqr1g  4801  iuneqconst  4951  axprlem3  5361  axprlem3OLD  5364  sbcop1  5426  propeqop  5445  euotd  5451  rexopabb  5466  sotr2  5556  relop  5789  elinxp  5967  elimasni  6039  sotri2  6075  onmindif  6400  dffv2  6917  mpteqb  6948  elfvmptrab  6958  chfnrn  6982  elpreima  6991  iinpreima  7002  exfo  7038  ffnfv  7052  f1elima  7197  f1ounsn  7206  f1eqcocnv  7235  fliftfun  7246  soisores  7261  isotr  7270  isomin  7271  ovmpodv2  7504  difsnexi  7694  onint  7723  oneqmin  7733  ordunisuc2  7774  tfindsg  7791  findsg  7827  resf1extb  7864  f1oweALT  7904  el2mpocl  8016  poseq  8088  soseq  8089  ressuppss  8113  funsssuppss  8120  suppofssd  8133  smoiso  8282  seqomlem2  8370  oaordi  8461  oawordri  8465  oaordex  8473  oalimcl  8475  omwordi  8486  oewordi  8506  oelim2  8510  nnmwordi  8550  xpider  8712  iiner  8713  undifixp  8858  mptelixpg  8859  dom2lem  8914  findcard2s  9075  pssnn  9078  nneneq  9115  fineqvlem  9150  dif1ennnALT  9161  unfilem2  9190  domunfican  9206  f1dmvrnfibi  9225  fsuppimp  9252  dffi2  9307  infsupprpr  9390  wemaplem2  9433  suc11reg  9509  noinfep  9550  cantnflem1  9579  r1fin  9666  tcrank  9777  cardlim  9865  fseqenlem1  9915  alephnbtwn  9962  alephord2i  9968  alephf1  9976  cardaleph  9980  alephiso  9989  dfac12lem2  10036  ackbij1lem16  10125  cflm  10141  cfcoflem  10163  sornom  10168  fin23lem27  10219  isf32lem7  10250  fin17  10285  fin1a2lem2  10292  fin1a2lem4  10294  fin1a2lem6  10296  fin1a2lem9  10299  axdc3lem2  10342  zorn2lem7  10393  uniimadom  10435  inar1  10666  grothomex  10720  addcanpi  10790  mulcanpi  10791  enqer  10812  genpcd  10897  genpnmax  10898  ltexprlem4  10930  reclem3pr  10940  reclem4pr  10941  suplem2pr  10944  axpre-ltadd  11058  axpre-sup  11060  ltletr  11205  00id  11288  addn0nid  11537  mul0or  11757  prodgt02  11969  lemul1a  11975  mulgt1OLD  11980  divgt0  11990  divge0  11991  ledivp1i  12047  ltdivp1i  12048  cju  12121  nnsub  12169  nominpos  12358  nn0n0n1ge2  12449  btwnnz  12549  suprfinzcl  12587  ublbneg  12831  zmax  12843  cnref1o  12883  ltsubrp  12928  ltaddrp  12929  xrltletr  13056  qbtwnre  13098  xltnegi  13115  xnn0xadd0  13146  iccsupr  13342  icoshft  13373  difreicc  13384  iccshftri  13387  iccshftli  13389  iccdili  13391  icccntri  13393  fzen  13441  elfz1b  13493  fzofzim  13609  eluzgtdifelfzo  13627  elfzo1elm1fzo0  13668  injresinjlem  13690  injresinj  13691  flval2  13718  flval3  13719  modmuladdim  13821  modaddmodup  13841  addmodlteq  13853  fseqsupubi  13885  ssnn0fi  13892  mptnn0fsuppr  13906  sq01  14132  hashf1rn  14259  hashgt12el  14329  hashgt12el2  14330  hashfundm  14349  hash2pr  14376  hash2exprb  14378  hashge2el2difr  14388  hashtpg  14392  hash3tr  14398  lswlgt0cl  14476  ccatalpha  14501  pfxfv  14590  pfxsuff1eqwrdeq  14606  ccatopth2  14624  swrdccat  14642  swrdccat3blem  14646  reuccatpfxs1lem  14653  repsdf2  14685  repswsymball  14686  repswrevw  14694  cshweqrep  14728  cshw1  14729  2cshwcshw  14732  scshwfzeqfzo  14733  cshwcsh2id  14735  swrdco  14744  swrd2lsw  14859  2swrd2eqwrdeq  14860  wwlktovfo  14865  cjre  15046  icodiamlt  15345  reusq0  15372  o1lo1  15444  o1of2  15520  o1rlimmul  15526  zsum  15625  modfsummods  15700  zprod  15844  reeff1  16029  dvdsmod0  16169  dvds2lem  16179  muldvds1  16191  dvdscmulr  16195  dvdsmulcr  16196  dvdsdivcl  16227  mod2eq1n2dvds  16258  oddnn02np1  16259  divalglem8  16311  ndvdsadd  16321  zeqzmulgcd  16421  dfgcd2  16457  absproddvds  16528  lcmftp  16547  coprmdvds  16564  2mulprm  16604  isprm5  16618  divgcdodd  16621  isprm6  16625  prmdvdsexpr  16628  prmdvdsbc  16637  cncongrprm  16640  phiprmpw  16687  modprm0  16717  pythagtriplem4  16731  pcz  16793  difsqpwdvds  16799  1arith  16839  prmgaplem5  16967  prmgaplem6  16968  cshwrepswhash1  17014  sbcie2s  17072  divsfval  17451  catsubcat  17746  fthmon  17836  isinitoi  17906  istermoi  17907  iszeroi  17916  setcmon  17994  setcepi  17995  funcestrcsetclem8  18053  fthestrcsetc  18056  funcsetcestrclem8  18068  fthsetcestrc  18071  odupos  18232  pltnle  18242  pltval3  18243  lublecllem  18264  latasym  18349  mrelatglb  18466  mrelatlub  18468  cnvpsb  18485  chninf  18541  mgmpropd  18559  isgrpid2  18889  ghmghmrn  19147  ghmf1  19158  kerf1ghm  19159  orbsta  19225  resscntz  19245  gsmsymgrfixlem1  19339  gsmsymgreqlem2  19343  mndodcongi  19455  odf1  19474  lsmss1  19577  lsmss2  19579  efgredeu  19664  cntzcmnss  19753  imasabl  19788  lt6abl  19807  ablfaclem3  20001  ogrpaddlt  20050  ringinvnz1ne0  20218  0ringnnzr  20440  subrngringnsg  20468  srhmsubc  20595  domnmuln0  20624  lspsneq  21059  lspsneu  21060  lsmcv  21078  rnglidlmcl  21153  rngqiprngimf1lem  21231  lidldvgen  21271  domnchr  21469  znf1o  21488  zntoslem  21493  znfld  21497  cygznlem2a  21504  cygznlem3  21506  phlssphl  21596  islindf4  21775  uvcendim  21784  psdmul  22081  ply1scln0  22206  gsummoncoe1  22223  matvscl  22346  scmataddcl  22431  scmatsubcl  22432  scmatfo  22445  scmatghm  22448  maducoeval2  22555  slesolinv  22595  cramerimplem2  22599  cpmatelimp  22627  cpmatelimp2  22629  cpmatacl  22631  cpmatinvcl  22632  pm2mpf1  22714  cayhamlem1  22781  cayleyhamilton1  22807  0ntr  22986  islpi  23064  lmss  23213  cmpcld  23317  cmpfi  23323  1stcelcls  23376  comppfsc  23447  ptcnplem  23536  qtophmeo  23732  fbdmn0  23749  fbasrn  23799  elfm3  23865  fmfnfmlem4  23872  fclscf  23940  cnpfcf  23956  alexsubALTlem3  23964  tsmsres  24059  blval2  24477  tnggrpr  24570  nmoleub  24646  nmhmcn  25047  ncvs1  25084  iscau4  25206  caussi  25224  cmssmscld  25277  cmslssbn  25299  cniccbdd  25389  ovoliunnul  25435  mbfinf  25593  itg2splitlem  25676  dvcn  25850  c1lip1  25929  c1lip3  25931  dvcnvrelem1  25949  dvfsumlem2  25960  ply1divex  26069  quotcan  26244  aannenlem1  26263  taylf  26295  taylthlem2  26309  ulmcaulem  26330  ulmcau  26331  reeff1o  26384  logccv  26599  rtprmirr  26697  logreclem  26699  isosctrlem2  26756  xrlimcnp  26905  rlimcxp  26911  ftalem7  27016  vmappw  27053  fsumdvdsmul  27132  fsumvma  27151  dchreq  27196  dchrptlem1  27202  dchrsum  27207  bposlem7  27228  lgsqrlem2  27285  lgsdchr  27293  gausslemma2dlem1a  27303  lgseisenlem2  27314  lgsquad2  27324  2lgslem1b  27330  2sqlem6  27361  2sqnn0  27376  addsq2reu  27378  2sqreulem2  27390  sltval2  27595  sltres  27601  nodenselem8  27630  nodense  27631  noresle  27636  scutun12  27751  madeval2  27794  elmade  27812  negsf1o  27996  muls0ord  28124  recsex  28157  bdayon  28209  noseqrdgfn  28236  n0subs  28289  eln0zs  28324  zsoring  28332  tgcgrcomimp  28455  isperp2  28693  xmstrkgc  28864  brbtwn  28877  brcgr  28878  axcgrid  28894  axeuclidlem  28940  axeuclid  28941  elntg2  28963  lpvtx  29046  upgrex  29070  upgrpredgv  29117  upgredgpr  29120  uhgr0v0e  29216  subgrprop  29251  fusgrfisbase  29306  edgnbusgreu  29345  nbusgredgeu0  29346  cusgredg  29402  structtocusgr  29424  cusgrsize2inds  29432  cusgrsize  29433  usgredgsscusgredg  29438  fusgrmaxsize  29443  uspgrloopvtxel  29495  umgr2v2e  29504  vtxdginducedm1fi  29523  finsumvtxdg2sstep  29528  rgrprop  29539  rusgrprop  29541  0uhgrrusgr  29557  rusgrpropedg  29563  ewlkprop  29582  upgrewlkle2  29585  wlkprop  29590  upgrwlkcompim  29621  uspgr2wlkeq  29624  wlklenvclwlk  29632  wlkonprop  29635  wlkres  29647  redwlk  29649  wlkdlem2  29660  wksonproplem  29681  usgr2trlspth  29739  usgr2pth  29742  pthdlem1  29744  crctcshwlkn0lem4  29791  wwlksnprcl  29817  wlkiswwlks2  29853  wwlksm1edg  29859  wlknewwlksn  29865  wwlksnred  29870  wwlksnextbi  29872  wwlksnextwrd  29875  wwlksnextinj  29877  wwlksnextsurj  29878  umgr2wlk  29927  usgrwwlks2on  29936  umgrwwlks2on  29937  elwwlks2  29947  clwwlk1loop  29968  umgrclwwlkge2  29971  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwlkclwwlkfo  29989  clwwisshclwwslemlem  29993  clwwlknwwlksn  30018  clwwlknlbonbgr1  30019  clwwlkn1loopb  30023  clwwlkf  30027  clwwlknon1  30077  clwwlknonwwlknonb  30086  clwwlknonex2lem2  30088  vdn0conngrumgrv2  30176  frgrnbnb  30273  frgrncvvdeqlem2  30280  frgrncvvdeqlem3  30281  frgrncvvdeqlem6  30284  frgrwopreglem4a  30290  fusgr2wsp2nb  30314  frrusgrord0lem  30319  numclwwlk2lem1lem  30322  2clwwlk2clwwlklem  30326  2clwwlk2clwwlk  30330  numclwwlk1lem2foa  30334  numclwwlk1lem2f1  30337  frgrreg  30374  hlipgt0  30894  ocin  31276  ocnel  31278  shmodsi  31369  pjmf1  31696  unopf1o  31896  staddi  32226  stadd3i  32228  mdi  32275  dmdmd  32280  dmdi  32282  dmdbr2  32283  dmdbr3  32285  dmdbr4  32286  dmdi4  32287  mdsl1i  32301  superpos  32334  cvbr4i  32347  atssma  32358  atcv1  32360  atomli  32362  chirredlem1  32370  addltmulALT  32426  bian1dOLD  32436  ifeqeqx  32522  disjxpin  32568  suppss3  32706  fpwrelmap  32716  expgt0b  32799  mndlactfo  33008  mndractfo  33010  qsfld  33463  ply1degltdimlem  33635  ply1degltdim  33636  metider  33907  tpr2rico  33925  xrge0iifiso  33948  qqhcn  34004  qqhucn  34005  esumlub  34073  esumpinfval  34086  esumpinfsum  34090  ballotlemfc0  34506  ballotlemfcc  34507  ftc2re  34611  bnj517  34897  axsepg2  35094  axsepg2ALT  35095  fnrelpredd  35102  rankfilimbi  35112  axnulg  35119  pfxwlk  35168  subgrwlk  35176  loop1cycl  35181  erdsze2lem2  35248  satfv1  35407  satfdmlem  35412  satf0op  35421  fmlasuc  35430  dfrdg4  35995  altopthsn  36005  btwncomim  36057  btwnexch3  36064  btwnexch2  36067  endofsegid  36129  opnrebl2  36365  nn0prpwlem  36366  onsuct0  36485  ordcmp  36491  nndivsub  36501  dnibndlem13  36534  bj-cbval  36693  bj-cbvex  36694  bj-cbvexw  36720  bj-cbv3tb  36831  bj-spimtv  36838  bj-equsal  36870  bj-sbsb  36881  bj-vtoclf  36959  bj-zfauscl  36968  bj-gabss  36979  bj-gabeqd  36981  currysetlem2  36992  bj-snsetex  37007  bj-ismooredr2  37154  bj-inftyexpiinj  37253  bj-finsumval0  37329  bj-fvimacnv0  37330  bj-bary1lem1  37355  bj-bary1  37356  f1omptsnlem  37380  iooelexlt  37406  relowlpssretop  37408  rdgeqoa  37414  finxpsuclem  37441  fvineqsneq  37456  pibt2  37461  wl-isseteq  37549  wl-equsal1i  37588  ltflcei  37647  sin2h  37649  cos2h  37650  tan2h  37651  lindsenlbs  37654  matunitlindf  37657  poimirlem3  37662  poimirlem4  37663  poimirlem18  37677  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem24  37683  poimirlem25  37684  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem31  37690  poimir  37692  heicant  37694  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  mbfresfi  37705  cnambfre  37707  ftc1anc  37740  dvasin  37743  areacirclem1  37747  areacirclem4  37750  areacirc  37752  brabg2  37756  fzmul  37780  fdc  37784  incsequz2  37788  isbnd2  37822  opidonOLD  37891  opidon2OLD  37893  grpomndo  37914  elghomlem2OLD  37925  rngoueqz  37979  dvrunz  37993  divrngidl  38067  refressn  38544  dral1-o  39002  lsatn0  39097  l1cvpat  39152  leat2  39392  atnle  39415  cvlcvr1  39437  cvrexchlem  39517  cvratlem  39519  cvrat  39520  atcvrj0  39526  atle  39534  snatpsubN  39848  linepsubN  39850  pmapsub  39866  lneq2at  39876  lncvrelatN  39879  2llnma3r  39886  cdlemblem  39891  paddasslem5  39922  poml4N  40051  lhpmcvr4N  40124  trlval2  40261  cdlemd6  40301  cdleme7ga  40346  cdleme25b  40452  cdleme29b  40473  cdleme35fnpq  40547  cdleme50f1  40641  cdlemf1  40659  cdlemg27b  40794  cdlemk28-3  41006  tendospcanN  41121  diaf11N  41147  dia2dimlem1  41162  dibf11N  41259  dihf11  41365  dihmeetlem1N  41388  dochvalr  41455  dochnel2  41490  dvh4dimlem  41541  dochsat0  41555  mapd1o  41746  hdmapf1oN  41963  hgmapval0  41990  hgmapf1oN  42001  hlhilhillem  42058  nnproddivdvdsd  42092  lcmineqlem  42144  aks4d1p1p5  42167  aks4d1p3  42170  aks4d1p8d2  42177  aks4d1p8  42179  aks4d1p9  42180  fldhmf1  42182  isprimroot2  42186  primrootsunit1  42189  primrootscoprmpow  42191  posbezout  42192  primrootscoprbij  42194  primrootlekpowne0  42197  primrootspoweq0  42198  aks6d1c1p1  42199  aks6d1c1p2  42201  aks6d1c1p3  42202  aks6d1c1p4  42203  aks6d1c1p5  42204  aks6d1c1p7  42205  aks6d1c1p6  42206  aks6d1c1p8  42207  aks6d1c2p2  42211  aks6d1c2lem3  42218  aks6d1c2lem4  42219  hashnexinj  42220  hashnexinjle  42221  aks6d1c2  42222  aks6d1c5lem0  42227  aks6d1c5lem1  42228  aks6d1c5  42231  sticksstones1  42238  sticksstones3  42240  sticksstones8  42245  sticksstones11  42248  sticksstones12  42250  sticksstones20  42258  sticksstones22  42260  aks6d1c6lem3  42264  aks6d1c6lem4  42265  aks6d1c6isolem1  42266  aks6d1c6isolem2  42267  aks6d1c6lem5  42269  aks6d1c7  42276  rhmqusspan  42277  unitscyglem2  42288  unitscyglem3  42289  aks5lem8  42293  sn-axprlem3  42309  oexpreposd  42414  sn-remul0ord  42500  frlmsnic  42632  fsuppind  42682  prjspval  42695  rexrabdioph  42886  fphpdo  42909  irrapxlem3  42916  rmxypairf1o  43003  rmxycomplete  43009  zindbi  43038  lermxnn0  43042  ltrmy  43044  rmyeq0  43045  rmyeq  43046  lermy  43047  acongsym  43068  acongneg2  43069  wepwsolem  43134  onsupuni  43321  onsupmaxb  43331  onsucf1o  43364  onov0suclim  43366  oe0suclim  43369  onsucwordi  43380  cantnfresb  43416  omabs2  43424  tfsconcat0b  43438  tfsconcatrev  43440  naddcnffo  43456  oaun3lem1  43466  oaltom  43497  omltoe  43499  sdomne0  43505  sdomne0d  43506  safesnsupfidom1o  43509  intabssd  43611  iscard4  43625  ss2iundf  43751  frege129d  43855  frege133d  43857  axfrege52a  43948  axfrege52c  43979  ntrk0kbimka  44131  gneispace  44226  suprleubrd  44258  suprlubrd  44260  radcnvrat  44406  nzss  44409  expgrowthi  44425  ordpss  44542  bi23impib  44578  rspsbc2  44626  tratrb  44628  sbcim2g  44630  truniALT  44633  3impcombi  44908  tpid3gVD  44933  orbi1rVD  44939  sbc3orgVD  44942  rspsbc2VD  44946  tratrbVD  44952  sbcim2gVD  44966  sbcbiVD  44967  truniALTVD  44969  trintALTVD  44971  trintALT  44972  csbingVD  44975  csbsngVD  44984  csbxpgVD  44985  csbresgVD  44986  csbrngVD  44987  csbima12gALTVD  44988  csbunigVD  44989  csbfv12gALTVD  44990  relopabVD  44992  isosctrlem1ALT  45025  relpfrlem  45045  trfr  45054  fzisoeu  45400  xrralrecnnge  45487  allbutfi  45490  climinf  45705  liminfreuzlem  45899  climliminf  45903  climliminflimsup  45905  xlimpnfxnegmnf  45911  xlimbr  45924  stoweidlem7  46104  stoweidlem62  46159  sge0gerpmpt  46499  meaiuninclem  46577  carageniuncllem2  46619  issmflem  46824  et-sqrtnegnre  46970  ormkglobd  46972  natlocalincr  46973  funressnfv  47142  funressnvmo  47144  f1cof1b  47176  2reu3  47209  ralbinrald  47221  afv0fv0  47248  afv0nbfvbi  47250  afvfv0bi  47251  fnbrafvb  47253  afvres  47271  tz6.12-afv  47272  afvco2  47275  ndmaovcl  47302  afv2res  47338  tz6.12-afv2  47339  nelbrim  47374  f1oresf1o2  47390  zm1nn  47401  nltle2tri  47412  subsubelfzo0  47425  2tceilhalfelfzo1  47431  iccpartres  47517  iccpartiltu  47521  fargshiftfv  47538  ichnreuop  47571  ichreuopeq  47572  prsprel  47586  sprsymrelf1lem  47590  sprsymrelfolem2  47592  sprsymrelfo  47596  prpair  47600  paireqne  47610  sbcpr  47620  fmtnof1  47634  goldbachthlem2  47645  fmtnoprmfac1  47664  fmtnoprmfac2  47666  lighneallem2  47705  lighneallem4b  47708  lighneallem4  47709  evennodd  47742  oddneven  47743  oexpnegnz  47777  evenltle  47816  fpprwppr  47838  fpprwpprb  47839  gbowge7  47862  gbege6  47864  sbgoldbwt  47876  sbgoldbst  47877  nnsum3primesle9  47893  bgoldbtbndlem2  47905  grimprop  47982  isuspgrimlem  47994  uhgrimisgrgriclem  48029  clnbgrgrimlem  48032  grtriproplem  48038  isgrtri  48042  grimgrtri  48048  stgr1  48060  isubgr3stgr  48074  grlimprop  48083  uspgrlimlem2  48088  uspgrlimlem3  48089  grlimprclnbgr  48095  gpg5nbgrvtx13starlem1  48170  clintop  48307  isassintop  48309  lidldomn1  48330  uzlidlring  48334  2zrngnmlid2  48356  rngccatidALTV  48371  ringccatidALTV  48405  srhmsubcALTV  48424  ztprmneprm  48446  pgrpgt2nabl  48465  lindslinindimp2lem4  48561  lincresunit3  48581  fldivexpfllog2  48665  digexp  48707  naryfvalelfv  48732  affinecomb1  48802  eenglngeehlnmlem1  48837  eenglngeehlnmlem2  48838  eenglngeehlnm  48839  itscnhlc0yqe  48859  itsclc0yqsol  48864  itscnhlc0xyqsol  48865  itschlc0xyqsol1  48866  itschlc0xyqsol  48867  itsclquadeu  48877  inlinecirc02plem  48886  inlinecirc02p  48887  pm4.71da  48889  mofsn  48943  seposep  49025  resipos  49074  idmon  49120  idepi  49121  prsthinc  49564  grptcmon  49693  grptcepi  49694  spd  49778  spcdvw  49779  setrec2fun  49792