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  4632  rabsnifsb  4670  ssunsn2  4774  preqr1g  4799  iuneqconst  4948  axprlem3  5358  axprlem3OLD  5361  sbcop1  5423  propeqop  5442  euotd  5448  rexopabb  5463  sotr2  5553  relop  5785  elinxp  5963  elimasni  6035  sotri2  6071  onmindif  6395  dffv2  6912  mpteqb  6943  elfvmptrab  6953  chfnrn  6977  elpreima  6986  iinpreima  6997  exfo  7033  ffnfv  7047  f1elima  7192  f1ounsn  7201  f1eqcocnv  7230  fliftfun  7241  soisores  7256  isotr  7265  isomin  7266  ovmpodv2  7499  difsnexi  7689  onint  7718  oneqmin  7728  ordunisuc2  7769  tfindsg  7786  findsg  7822  resf1extb  7859  f1oweALT  7899  el2mpocl  8011  poseq  8083  soseq  8084  ressuppss  8108  funsssuppss  8115  suppofssd  8128  smoiso  8277  seqomlem2  8365  oaordi  8456  oawordri  8460  oaordex  8468  oalimcl  8470  omwordi  8481  oewordi  8501  oelim2  8505  nnmwordi  8545  xpider  8707  iiner  8708  undifixp  8853  mptelixpg  8854  dom2lem  8909  findcard2s  9070  pssnn  9073  nneneq  9110  fineqvlem  9145  dif1ennnALT  9156  unfilem2  9185  domunfican  9201  f1dmvrnfibi  9220  fsuppimp  9247  dffi2  9302  infsupprpr  9385  wemaplem2  9428  suc11reg  9504  noinfep  9545  cantnflem1  9574  r1fin  9661  tcrank  9772  cardlim  9860  fseqenlem1  9910  alephnbtwn  9957  alephord2i  9963  alephf1  9971  cardaleph  9975  alephiso  9984  dfac12lem2  10031  ackbij1lem16  10120  cflm  10136  cfcoflem  10158  sornom  10163  fin23lem27  10214  isf32lem7  10245  fin17  10280  fin1a2lem2  10287  fin1a2lem4  10289  fin1a2lem6  10291  fin1a2lem9  10294  axdc3lem2  10337  zorn2lem7  10388  uniimadom  10430  inar1  10661  grothomex  10715  addcanpi  10785  mulcanpi  10786  enqer  10807  genpcd  10892  genpnmax  10893  ltexprlem4  10925  reclem3pr  10935  reclem4pr  10936  suplem2pr  10939  axpre-ltadd  11053  axpre-sup  11055  ltletr  11200  00id  11283  addn0nid  11532  mul0or  11752  prodgt02  11964  lemul1a  11970  mulgt1OLD  11975  divgt0  11985  divge0  11986  ledivp1i  12042  ltdivp1i  12043  cju  12116  nnsub  12164  nominpos  12353  nn0n0n1ge2  12444  btwnnz  12544  suprfinzcl  12582  ublbneg  12826  zmax  12838  cnref1o  12878  ltsubrp  12923  ltaddrp  12924  xrltletr  13051  qbtwnre  13093  xltnegi  13110  xnn0xadd0  13141  iccsupr  13337  icoshft  13368  difreicc  13379  iccshftri  13382  iccshftli  13384  iccdili  13386  icccntri  13388  fzen  13436  elfz1b  13488  fzofzim  13604  eluzgtdifelfzo  13622  elfzo1elm1fzo0  13663  injresinjlem  13685  injresinj  13686  flval2  13713  flval3  13714  modmuladdim  13816  modaddmodup  13836  addmodlteq  13848  fseqsupubi  13880  ssnn0fi  13887  mptnn0fsuppr  13901  sq01  14127  hashf1rn  14254  hashgt12el  14324  hashgt12el2  14325  hashfundm  14344  hash2pr  14371  hash2exprb  14373  hashge2el2difr  14383  hashtpg  14387  hash3tr  14393  lswlgt0cl  14471  ccatalpha  14496  pfxfv  14585  pfxsuff1eqwrdeq  14601  ccatopth2  14619  swrdccat  14637  swrdccat3blem  14641  reuccatpfxs1lem  14648  repsdf2  14680  repswsymball  14681  repswrevw  14689  cshweqrep  14723  cshw1  14724  2cshwcshw  14727  scshwfzeqfzo  14728  cshwcsh2id  14730  swrdco  14739  swrd2lsw  14854  2swrd2eqwrdeq  14855  wwlktovfo  14860  cjre  15041  icodiamlt  15340  reusq0  15367  o1lo1  15439  o1of2  15515  o1rlimmul  15521  zsum  15620  modfsummods  15695  zprod  15839  reeff1  16024  dvdsmod0  16164  dvds2lem  16174  muldvds1  16186  dvdscmulr  16190  dvdsmulcr  16191  dvdsdivcl  16222  mod2eq1n2dvds  16253  oddnn02np1  16254  divalglem8  16306  ndvdsadd  16316  zeqzmulgcd  16416  dfgcd2  16452  absproddvds  16523  lcmftp  16542  coprmdvds  16559  2mulprm  16599  isprm5  16613  divgcdodd  16616  isprm6  16620  prmdvdsexpr  16623  prmdvdsbc  16632  cncongrprm  16635  phiprmpw  16682  modprm0  16712  pythagtriplem4  16726  pcz  16788  difsqpwdvds  16794  1arith  16834  prmgaplem5  16962  prmgaplem6  16963  cshwrepswhash1  17009  sbcie2s  17067  divsfval  17446  catsubcat  17741  fthmon  17831  isinitoi  17901  istermoi  17902  iszeroi  17911  setcmon  17989  setcepi  17990  funcestrcsetclem8  18048  fthestrcsetc  18051  funcsetcestrclem8  18063  fthsetcestrc  18066  odupos  18227  pltnle  18237  pltval3  18238  lublecllem  18259  latasym  18344  mrelatglb  18461  mrelatlub  18463  cnvpsb  18480  chninf  18536  mgmpropd  18554  isgrpid2  18884  ghmghmrn  19142  ghmf1  19153  kerf1ghm  19154  orbsta  19220  resscntz  19240  gsmsymgrfixlem1  19334  gsmsymgreqlem2  19338  mndodcongi  19450  odf1  19469  lsmss1  19572  lsmss2  19574  efgredeu  19659  cntzcmnss  19748  imasabl  19783  lt6abl  19802  ablfaclem3  19996  ogrpaddlt  20045  ringinvnz1ne0  20213  0ringnnzr  20435  subrngringnsg  20463  srhmsubc  20590  domnmuln0  20619  lspsneq  21054  lspsneu  21055  lsmcv  21073  rnglidlmcl  21148  rngqiprngimf1lem  21226  lidldvgen  21266  domnchr  21464  znf1o  21483  zntoslem  21488  znfld  21492  cygznlem2a  21499  cygznlem3  21501  phlssphl  21591  islindf4  21770  uvcendim  21779  psdmul  22076  ply1scln0  22201  gsummoncoe1  22218  matvscl  22341  scmataddcl  22426  scmatsubcl  22427  scmatfo  22440  scmatghm  22443  maducoeval2  22550  slesolinv  22590  cramerimplem2  22594  cpmatelimp  22622  cpmatelimp2  22624  cpmatacl  22626  cpmatinvcl  22627  pm2mpf1  22709  cayhamlem1  22776  cayleyhamilton1  22802  0ntr  22981  islpi  23059  lmss  23208  cmpcld  23312  cmpfi  23318  1stcelcls  23371  comppfsc  23442  ptcnplem  23531  qtophmeo  23727  fbdmn0  23744  fbasrn  23794  elfm3  23860  fmfnfmlem4  23867  fclscf  23935  cnpfcf  23951  alexsubALTlem3  23959  tsmsres  24054  blval2  24472  tnggrpr  24565  nmoleub  24641  nmhmcn  25042  ncvs1  25079  iscau4  25201  caussi  25219  cmssmscld  25272  cmslssbn  25294  cniccbdd  25384  ovoliunnul  25430  mbfinf  25588  itg2splitlem  25671  dvcn  25845  c1lip1  25924  c1lip3  25926  dvcnvrelem1  25944  dvfsumlem2  25955  ply1divex  26064  quotcan  26239  aannenlem1  26258  taylf  26290  taylthlem2  26304  ulmcaulem  26325  ulmcau  26326  reeff1o  26379  logccv  26594  rtprmirr  26692  logreclem  26694  isosctrlem2  26751  xrlimcnp  26900  rlimcxp  26906  ftalem7  27011  vmappw  27048  fsumdvdsmul  27127  fsumvma  27146  dchreq  27191  dchrptlem1  27197  dchrsum  27202  bposlem7  27223  lgsqrlem2  27280  lgsdchr  27288  gausslemma2dlem1a  27298  lgseisenlem2  27309  lgsquad2  27319  2lgslem1b  27325  2sqlem6  27356  2sqnn0  27371  addsq2reu  27373  2sqreulem2  27385  sltval2  27590  sltres  27596  nodenselem8  27625  nodense  27626  noresle  27631  scutun12  27746  madeval2  27789  elmade  27807  negsf1o  27991  muls0ord  28119  recsex  28152  bdayon  28204  noseqrdgfn  28231  n0subs  28284  eln0zs  28319  zsoring  28327  tgcgrcomimp  28450  isperp2  28688  xmstrkgc  28859  brbtwn  28872  brcgr  28873  axcgrid  28889  axeuclidlem  28935  axeuclid  28936  elntg2  28958  lpvtx  29041  upgrex  29065  upgrpredgv  29112  upgredgpr  29115  uhgr0v0e  29211  subgrprop  29246  fusgrfisbase  29301  edgnbusgreu  29340  nbusgredgeu0  29341  cusgredg  29397  structtocusgr  29419  cusgrsize2inds  29427  cusgrsize  29428  usgredgsscusgredg  29433  fusgrmaxsize  29438  uspgrloopvtxel  29490  umgr2v2e  29499  vtxdginducedm1fi  29518  finsumvtxdg2sstep  29523  rgrprop  29534  rusgrprop  29536  0uhgrrusgr  29552  rusgrpropedg  29558  ewlkprop  29577  upgrewlkle2  29580  wlkprop  29585  upgrwlkcompim  29616  uspgr2wlkeq  29619  wlklenvclwlk  29627  wlkonprop  29630  wlkres  29642  redwlk  29644  wlkdlem2  29655  wksonproplem  29676  usgr2trlspth  29734  usgr2pth  29737  pthdlem1  29739  crctcshwlkn0lem4  29786  wwlksnprcl  29812  wlkiswwlks2  29848  wwlksm1edg  29854  wlknewwlksn  29860  wwlksnred  29865  wwlksnextbi  29867  wwlksnextwrd  29870  wwlksnextinj  29872  wwlksnextsurj  29873  umgr2wlk  29922  umgrwwlks2on  29930  elwwlks2  29939  clwwlk1loop  29960  umgrclwwlkge2  29963  clwlkclwwlklem2a1  29964  clwlkclwwlklem2a4  29969  clwlkclwwlklem2a  29970  clwlkclwwlklem2  29972  clwlkclwwlkfo  29981  clwwisshclwwslemlem  29985  clwwlknwwlksn  30010  clwwlknlbonbgr1  30011  clwwlkn1loopb  30015  clwwlkf  30019  clwwlknon1  30069  clwwlknonwwlknonb  30078  clwwlknonex2lem2  30080  vdn0conngrumgrv2  30168  frgrnbnb  30265  frgrncvvdeqlem2  30272  frgrncvvdeqlem3  30273  frgrncvvdeqlem6  30276  frgrwopreglem4a  30282  fusgr2wsp2nb  30306  frrusgrord0lem  30311  numclwwlk2lem1lem  30314  2clwwlk2clwwlklem  30318  2clwwlk2clwwlk  30322  numclwwlk1lem2foa  30326  numclwwlk1lem2f1  30329  frgrreg  30366  hlipgt0  30886  ocin  31268  ocnel  31270  shmodsi  31361  pjmf1  31688  unopf1o  31888  staddi  32218  stadd3i  32220  mdi  32267  dmdmd  32272  dmdi  32274  dmdbr2  32275  dmdbr3  32277  dmdbr4  32278  dmdi4  32279  mdsl1i  32293  superpos  32326  cvbr4i  32339  atssma  32350  atcv1  32352  atomli  32354  chirredlem1  32362  addltmulALT  32418  bian1dOLD  32428  ifeqeqx  32514  disjxpin  32560  suppss3  32698  fpwrelmap  32708  expgt0b  32791  mndlactfo  33000  mndractfo  33002  qsfld  33455  ply1degltdimlem  33627  ply1degltdim  33628  metider  33899  tpr2rico  33917  xrge0iifiso  33940  qqhcn  33996  qqhucn  33997  esumlub  34065  esumpinfval  34078  esumpinfsum  34082  ballotlemfc0  34498  ballotlemfcc  34499  ftc2re  34603  bnj517  34889  axsepg2  35086  axsepg2ALT  35087  fnrelpredd  35094  rankfilimbi  35104  axnulg  35111  pfxwlk  35160  subgrwlk  35168  loop1cycl  35173  erdsze2lem2  35240  satfv1  35399  satfdmlem  35404  satf0op  35413  fmlasuc  35422  dfrdg4  35985  altopthsn  35995  btwncomim  36047  btwnexch3  36054  btwnexch2  36057  endofsegid  36119  opnrebl2  36355  nn0prpwlem  36356  onsuct0  36475  ordcmp  36481  nndivsub  36491  dnibndlem13  36524  bj-cbval  36683  bj-cbvex  36684  bj-cbvexw  36710  bj-cbv3tb  36821  bj-spimtv  36828  bj-equsal  36860  bj-sbsb  36871  bj-vtoclf  36949  bj-zfauscl  36958  bj-gabss  36969  bj-gabeqd  36971  currysetlem2  36982  bj-snsetex  36997  bj-ismooredr2  37144  bj-inftyexpiinj  37243  bj-finsumval0  37319  bj-fvimacnv0  37320  bj-bary1lem1  37345  bj-bary1  37346  f1omptsnlem  37370  iooelexlt  37396  relowlpssretop  37398  rdgeqoa  37404  finxpsuclem  37431  fvineqsneq  37446  pibt2  37451  wl-isseteq  37539  wl-equsal1i  37578  wl-ax11-lem10  37628  ltflcei  37648  sin2h  37650  cos2h  37651  tan2h  37652  lindsenlbs  37655  matunitlindf  37658  poimirlem3  37663  poimirlem4  37664  poimirlem18  37678  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem24  37684  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  poimirlem31  37691  poimir  37693  heicant  37695  mblfinlem1  37697  mblfinlem2  37698  mblfinlem3  37699  mblfinlem4  37700  mbfresfi  37706  cnambfre  37708  ftc1anc  37741  dvasin  37744  areacirclem1  37748  areacirclem4  37751  areacirc  37753  brabg2  37757  fzmul  37781  fdc  37785  incsequz2  37789  isbnd2  37823  opidonOLD  37892  opidon2OLD  37894  grpomndo  37915  elghomlem2OLD  37926  rngoueqz  37980  dvrunz  37994  divrngidl  38068  refressn  38480  dral1-o  38943  lsatn0  39038  l1cvpat  39093  leat2  39333  atnle  39356  cvlcvr1  39378  cvrexchlem  39458  cvratlem  39460  cvrat  39461  atcvrj0  39467  atle  39475  snatpsubN  39789  linepsubN  39791  pmapsub  39807  lneq2at  39817  lncvrelatN  39820  2llnma3r  39827  cdlemblem  39832  paddasslem5  39863  poml4N  39992  lhpmcvr4N  40065  trlval2  40202  cdlemd6  40242  cdleme7ga  40287  cdleme25b  40393  cdleme29b  40414  cdleme35fnpq  40488  cdleme50f1  40582  cdlemf1  40600  cdlemg27b  40735  cdlemk28-3  40947  tendospcanN  41062  diaf11N  41088  dia2dimlem1  41103  dibf11N  41200  dihf11  41306  dihmeetlem1N  41329  dochvalr  41396  dochnel2  41431  dvh4dimlem  41482  dochsat0  41496  mapd1o  41687  hdmapf1oN  41904  hgmapval0  41931  hgmapf1oN  41942  hlhilhillem  41999  nnproddivdvdsd  42033  lcmineqlem  42085  aks4d1p1p5  42108  aks4d1p3  42111  aks4d1p8d2  42118  aks4d1p8  42120  aks4d1p9  42121  fldhmf1  42123  isprimroot2  42127  primrootsunit1  42130  primrootscoprmpow  42132  posbezout  42133  primrootscoprbij  42135  primrootlekpowne0  42138  primrootspoweq0  42139  aks6d1c1p1  42140  aks6d1c1p2  42142  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p7  42146  aks6d1c1p6  42147  aks6d1c1p8  42148  aks6d1c2p2  42152  aks6d1c2lem3  42159  aks6d1c2lem4  42160  hashnexinj  42161  hashnexinjle  42162  aks6d1c2  42163  aks6d1c5lem0  42168  aks6d1c5lem1  42169  aks6d1c5  42172  sticksstones1  42179  sticksstones3  42181  sticksstones8  42186  sticksstones11  42189  sticksstones12  42191  sticksstones20  42199  sticksstones22  42201  aks6d1c6lem3  42205  aks6d1c6lem4  42206  aks6d1c6isolem1  42207  aks6d1c6isolem2  42208  aks6d1c6lem5  42210  aks6d1c7  42217  rhmqusspan  42218  unitscyglem2  42229  unitscyglem3  42230  aks5lem8  42234  sn-axprlem3  42250  oexpreposd  42355  sn-remul0ord  42441  frlmsnic  42573  fsuppind  42623  prjspval  42636  rexrabdioph  42827  fphpdo  42850  irrapxlem3  42857  rmxypairf1o  42944  rmxycomplete  42950  zindbi  42979  lermxnn0  42983  ltrmy  42985  rmyeq0  42986  rmyeq  42987  lermy  42988  acongsym  43009  acongneg2  43010  wepwsolem  43075  onsupuni  43262  onsupmaxb  43272  onsucf1o  43305  onov0suclim  43307  oe0suclim  43310  onsucwordi  43321  cantnfresb  43357  omabs2  43365  tfsconcat0b  43379  tfsconcatrev  43381  naddcnffo  43397  oaun3lem1  43407  oaltom  43438  omltoe  43440  sdomne0  43446  sdomne0d  43447  safesnsupfidom1o  43450  intabssd  43552  iscard4  43566  ss2iundf  43692  frege129d  43796  frege133d  43798  axfrege52a  43889  axfrege52c  43920  ntrk0kbimka  44072  gneispace  44167  suprleubrd  44199  suprlubrd  44201  radcnvrat  44347  nzss  44350  expgrowthi  44366  ordpss  44483  bi23impib  44519  rspsbc2  44567  tratrb  44569  sbcim2g  44571  truniALT  44574  3impcombi  44849  tpid3gVD  44874  orbi1rVD  44880  sbc3orgVD  44883  rspsbc2VD  44887  tratrbVD  44893  sbcim2gVD  44907  sbcbiVD  44908  truniALTVD  44910  trintALTVD  44912  trintALT  44913  csbingVD  44916  csbsngVD  44925  csbxpgVD  44926  csbresgVD  44927  csbrngVD  44928  csbima12gALTVD  44929  csbunigVD  44930  csbfv12gALTVD  44931  relopabVD  44933  isosctrlem1ALT  44966  relpfrlem  44986  trfr  44995  fzisoeu  45341  xrralrecnnge  45428  allbutfi  45431  climinf  45646  liminfreuzlem  45840  climliminf  45844  climliminflimsup  45846  xlimpnfxnegmnf  45852  xlimbr  45865  stoweidlem7  46045  stoweidlem62  46100  sge0gerpmpt  46440  meaiuninclem  46518  carageniuncllem2  46560  issmflem  46765  et-sqrtnegnre  46911  ormkglobd  46913  natlocalincr  46914  funressnfv  47074  funressnvmo  47076  f1cof1b  47108  2reu3  47141  ralbinrald  47153  afv0fv0  47180  afv0nbfvbi  47182  afvfv0bi  47183  fnbrafvb  47185  afvres  47203  tz6.12-afv  47204  afvco2  47207  ndmaovcl  47234  afv2res  47270  tz6.12-afv2  47271  nelbrim  47306  f1oresf1o2  47322  zm1nn  47333  nltle2tri  47344  subsubelfzo0  47357  2tceilhalfelfzo1  47363  iccpartres  47449  iccpartiltu  47453  fargshiftfv  47470  ichnreuop  47503  ichreuopeq  47504  prsprel  47518  sprsymrelf1lem  47522  sprsymrelfolem2  47524  sprsymrelfo  47528  prpair  47532  paireqne  47542  sbcpr  47552  fmtnof1  47566  goldbachthlem2  47577  fmtnoprmfac1  47596  fmtnoprmfac2  47598  lighneallem2  47637  lighneallem4b  47640  lighneallem4  47641  evennodd  47674  oddneven  47675  oexpnegnz  47709  evenltle  47748  fpprwppr  47770  fpprwpprb  47771  gbowge7  47794  gbege6  47796  sbgoldbwt  47808  sbgoldbst  47809  nnsum3primesle9  47825  bgoldbtbndlem2  47837  grimprop  47914  isuspgrimlem  47926  uhgrimisgrgriclem  47961  clnbgrgrimlem  47964  grtriproplem  47970  isgrtri  47974  grimgrtri  47980  stgr1  47992  isubgr3stgr  48006  grlimprop  48015  uspgrlimlem2  48020  uspgrlimlem3  48021  grlimprclnbgr  48027  gpg5nbgrvtx13starlem1  48102  clintop  48239  isassintop  48241  lidldomn1  48262  uzlidlring  48266  2zrngnmlid2  48288  rngccatidALTV  48303  ringccatidALTV  48337  srhmsubcALTV  48356  ztprmneprm  48378  pgrpgt2nabl  48397  lindslinindimp2lem4  48493  lincresunit3  48513  fldivexpfllog2  48597  digexp  48639  naryfvalelfv  48664  affinecomb1  48734  eenglngeehlnmlem1  48769  eenglngeehlnmlem2  48770  eenglngeehlnm  48771  itscnhlc0yqe  48791  itsclc0yqsol  48796  itscnhlc0xyqsol  48797  itschlc0xyqsol1  48798  itschlc0xyqsol  48799  itsclquadeu  48809  inlinecirc02plem  48818  inlinecirc02p  48819  pm4.71da  48821  mofsn  48875  seposep  48957  resipos  49006  idmon  49052  idepi  49053  prsthinc  49496  grptcmon  49625  grptcepi  49626  spd  49710  spcdvw  49711  setrec2fun  49724