Theorem sylbi 217

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbi.1	⊢ (𝜑 ↔ 𝜓)
sylbi.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbi	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 216	. 2 ⊢ (𝜑 → 𝜓)
3		sylbi.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	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:  sylbb  219  biimpr  220  sylbb2  238  3imtr4i  292  sylnbi  330  imp  406  an12s  650  an32s  653  an4s  661  impimprbi  829  jaoi2  1060  ifpor  1073  1fpid3  1082  3impa  1110  syl3anb  1162  nanass  1512  nfntht2  1796  19.33b  1887  spimfw  1967  sbi1  2077  spsbe  2088  sb1v  2093  ax8  2120  ax9  2128  hbe1a  2150  sp  2191  aecoms  2433  mobi  2548  mo3  2565  mo4  2567  mopick  2626  2euexv  2632  2euex  2642  2mo  2649  2eu3  2655  eqcoms  2745  elex2  2814  elissetv  2818  eleq2s  2855  nfcr  2889  nfcrALT  2890  pm2.61ine  3016  rexex  3068  ral2imi  3077  rexlimiva  3131  r19.36v  3166  r19.45v  3172  r19.44v  3173  rspw  3215  rsp  3226  r19.37  3241  rexeq  3294  rabid2im  3433  ceqsralv  3483  gencl  3484  gencbvex  3501  vtoclgf  3527  elrabi  3644  mo2icl  3674  mob2  3675  reu3  3687  rmoim  3700  2reuswap  3706  2reuswap2  3707  2reurex  3720  2rmoswap  3721  sbcex  3752  ssel  3929  sseq1  3961  sseq2  3962  ssralv  4004  ssrexv  4005  ralss  4010  rexss  4011  unineq  4242  dfrab3ss  4277  rspn0  4310  pssdif  4323  difin0ss  4327  reldisj  4407  disjel  4411  uneqdifeq  4447  rexn0  4451  r19.2z  4454  r19.3rz  4456  raaan2  4477  ifnefalse  4493  ifbi  4504  nelpri  4614  nelprd  4616  elpwunsn  4643  rmosn  4678  rabrsn  4683  prprc1  4724  difprsn2  4759  tpprceq3  4762  tppreqb  4763  pwpw0  4771  ssunsn2  4785  eqsn  4787  snsssn  4799  preqr2  4807  preq12b  4808  opthpr  4809  prneimg  4812  preq12nebg  4821  opthprneg  4823  prproe  4863  intmin4  4934  dfiin2g  4988  invdisj  5086  disjiun  5088  disjss3  5099  brne0  5150  trel  5215  trss  5217  trintss  5225  axrep5  5234  zfrep4  5240  ssex  5268  intex  5291  intnex  5292  intabs  5296  abssexg  5329  reusv2lem1  5345  reusv2lem4  5348  reusv3  5352  axprALT  5369  axpr  5374  axprg  5383  rext  5403  unipw  5405  moabex  5413  moabexOLD  5414  nnullss  5417  exss  5418  sbcop1  5444  copsexgw  5446  copsexg  5447  propeqop  5463  propssopi  5464  opthhausdorff  5473  opthhausdorff0  5474  otiunsndisj  5476  iunopeqop  5477  brabv  5522  pwssun  5524  epelg  5533  0nelelxp  5667  opelxp  5668  elvvuni  5709  posn  5718  frsn  5720  bropaex12  5723  optoclOLD  5727  ssrel  5740  relsnb  5759  xpsspw  5766  relopabi  5779  ralxpf  5803  relop  5807  breldm  5865  elreldm  5892  dmrnssfld  5931  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  resabs1  5973  resima2  5983  iresn0n0  6021  relimasn  6052  asymref  6081  asymref2  6082  xpidtr  6087  trin2  6088  poirr2  6089  cnvimassrndm  6118  xpnz  6125  xp11  6141  xpcan  6142  xpcan2  6143  cnveqb  6162  dfco2a  6212  cores2  6226  coi2  6230  relresfld  6242  unixp0  6249  unixpid  6250  elsnxp  6257  reuop  6259  opreu2reu  6261  frpoinsg  6309  elsuci  6394  ordsssuc2  6418  ordssun  6429  iotanul2  6473  iotauni  6477  iota1  6479  iota4  6481  dffun8  6528  fununfun  6548  funcnvsn  6550  imadif  6584  f1imadifssran  6586  fcoi1  6716  fcoi2  6717  f0rn0  6727  f1ocnv  6794  f1ocnvb  6795  f1o00  6817  fo00  6818  nfunsn  6881  fnrnfv  6901  opabiota  6924  ssimaex  6927  dffv2  6937  fvmptss  6962  fvmptss2  6976  fvimacnv  7007  unpreima  7017  respreima  7020  fimacnvinrn  7025  fvn0ssdmfun  7028  fveqdmss  7032  feldmfvelcdm  7040  elrnrexdm  7043  elrnrexdmb  7044  eldmrexrnb  7046  dffo4  7057  exfo  7059  rnmptss  7077  funopdmsn  7105  funsndifnop  7106  funressn  7114  fnsnbOLD  7122  fndifnfp  7132  fvpr1g  7146  fvtp1  7151  fvtp1g  7154  tpres  7157  fconst5  7162  eufnfv  7185  elunirn  7207  f1ounsn  7228  isores1  7290  riotauni  7331  riotacl2  7341  riota1  7346  riota1a  7347  snriota  7358  eusvobj2  7360  oprabidw  7399  oprabid  7400  oprabv  7428  oprssdm  7549  2mpo0  7617  sorpssun  7685  sorpssin  7686  sorpssuni  7687  sorpssint  7688  onmindif2  7762  ordpwsuc  7767  onsucmin  7773  ordsucelsuc  7774  ordsucun  7777  unon  7783  ordunisuc  7784  0elsuc  7787  onuninsuci  7792  orduninsuc  7795  limsuc  7801  limuni3  7804  tfi  7805  tfisg  7806  tfindsg  7813  limomss  7823  limom  7834  find  7847  findsg  7849  relcnvexb  7878  f1iun  7898  ffoss  7900  f1oweALT  7926  1stval2  7960  2ndval2  7961  fo1stres  7969  fo2ndres  7970  1st2val  7971  2nd2val  7972  xp1st  7975  xp2nd  7976  unielxp  7981  el2xpss  7991  releldm2  7997  brovpreldm  8041  bropopvvv  8042  bropfvvvvlem  8043  bropfvvvv  8044  cnvf1o  8063  fo2ndf  8073  frxp  8078  poxp  8080  frpoins3xpg  8092  frpoins3xp3g  8093  poxp2  8095  poxp3  8102  soseq  8111  suppimacnv  8126  ressuppss  8135  ressuppssdif  8137  mpoxneldm  8164  mpoxopxnop0  8167  brovex  8174  reldmtpos  8186  dftpos4  8197  tpostpos  8198  tpostpos2  8199  frrlem2  8239  frrlem3  8240  frrlem4  8241  frrlem8  8245  smoel  8302  tfrlem4  8320  tfrlem7  8324  tfrlem8  8325  tfrlem9  8326  tfr2b  8337  rdgsucg  8364  frsuc  8378  tz7.48lem  8382  tz7.48-1  8384  tz7.49  8386  oesuclem  8462  oaord  8484  nnaord  8557  nneob  8594  ecexr  8650  brinxper  8675  swoord1  8678  swoord2  8679  0er  8684  ecdmn0  8698  mapprc  8779  mapfoss  8801  fsetdmprc0  8804  fsetprcnex  8811  fsetexb  8813  mapsnconst  8842  ixpprc  8869  ixpf  8870  ixpn0  8880  ixp0  8881  undifixp  8884  mptelixpg  8885  boxriin  8890  idssen  8946  ener  8950  en0ALT  8968  en1  8973  en1b  8974  en1uniel  8978  2dom  8979  snfi  8992  xpsnen  9001  sbthlem1  9027  sbthlem10  9036  domnsym  9043  2pwuninel  9072  ssenen  9091  dif1en  9098  findcard  9100  findcard2  9101  pssnn  9105  ssfi  9109  ssfiALT  9110  cnvfi  9112  enfi  9123  sbthfilem  9134  php  9143  php3  9145  ordfin  9152  ominf  9176  isinf  9177  en1eqsn  9187  enp1i  9191  findcard3  9195  difinf  9223  infcntss  9235  fiint  9239  infssuni  9258  card2on  9471  brwdomn0  9486  unwdomg  9501  unxpwdom2  9505  ixpiunwdom  9507  inf0  9542  inf3lem1  9549  infeq5i  9557  infeq5  9558  dfom3  9568  fict  9574  ttrcltr  9637  dmttrcl  9642  rnttrcl  9643  trcl  9649  epfrs  9652  setind2  9669  setinds  9670  setinds2f  9671  frinsg  9675  tz9.12lem3  9713  rankwflemb  9717  rankf  9718  rankidb  9724  snwf  9733  uniwf  9743  rankpwi  9747  rankunb  9774  rankuni2b  9777  rankuni  9787  rankxpsuc  9806  tcrank  9808  scottex  9809  scott0  9810  bnd2  9817  karden  9819  djuexb  9833  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  finnum  9872  carduni  9905  cardiun  9906  dif1card  9932  infxpenlem  9935  fseqenlem2  9947  acnrcl  9964  acndom  9973  acnnum  9974  alephfp  10030  iunfictbso  10036  dfac4  10044  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  dfac9  10059  dfac12r  10069  kmlem2  10074  kmlem4  10076  kmlem12  10084  kmlem13  10085  ackbij2  10164  cardcf  10174  cfeq0  10178  cfsuc  10179  alephsing  10198  fin4en1  10231  enfin2i  10243  fin23lem16  10257  fin23lem21  10261  fin23lem29  10263  fin23lem30  10264  isfin32i  10287  isfin1-2  10307  fin34  10312  fin17  10316  fin67  10317  isfin7-2  10318  fin1a2lem7  10328  fin1a2lem10  10331  fin1a2lem12  10333  itunitc  10343  axcc4dom  10363  dcomex  10369  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ac6c4  10403  ac6sf  10411  ac6s4  10412  zorn2lem6  10423  zorn2lem7  10424  zorng  10426  zornn0g  10427  ttukeylem6  10436  ttukey2g  10438  brdom5  10451  brdom4  10452  alephval2  10495  alephadd  10500  alephmul  10501  alephsuc3  10503  alephexp2  10504  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  fpwwe2lem7  10560  gchinf  10580  pwfseq  10587  winaon  10611  winacard  10615  winainf  10617  tsk0  10686  tskcard  10704  r1tskina  10705  gruima  10725  intgru  10737  ingru  10738  gruina  10741  axgroth6  10751  grothomex  10752  indpi  10830  nqereu  10852  nqerf  10853  ordpipq  10865  prn0  10912  prpssnq  10913  nqpr  10937  ltexprlem4  10962  reclem2pr  10971  recexsrlem  11026  map2psrpr  11033  supsr  11035  axpre-sup  11092  ltxrlt  11215  dedekind  11308  dedekindle  11309  negf1o  11579  lemul1a  12007  sup3  12111  supmul1  12123  supmullem1  12124  supmul  12126  peano2nn  12169  nn0ge0  12438  elnnnn0b  12457  nn0sub  12463  nn0ge2m1nn  12483  xnn0xr  12491  xnn0nemnf  12497  xnn0nnn0pnf  12499  zle0orge1  12517  nn0lt10b  12566  zeo  12590  nn0ind  12599  nn0ind-raph  12604  uzn0  12780  uznn0sub  12798  uz3m2nn  12819  uznnssnn  12820  uz2m1nn  12848  uz2mulcl  12851  indstr2  12852  uzinfi  12853  nn01to3  12866  qmulz  12876  qre  12878  qnegcl  12891  qreccl  12894  rphalflt  12948  nn0ledivnn  13032  xrltnr  13045  xnn0n0n1ge2b  13058  xnn0ge0  13060  xnegcl  13140  xnegneg  13141  xltnegi  13143  xnn0xaddcl  13162  xnegid  13165  xaddrid  13168  xnn0lenn0nn0  13172  xnn0xadd0  13174  xmulrid  13206  xrsupsslem  13234  xrinfmsslem  13235  xrsupss  13236  xrinfmss  13237  reltxrnmnf  13270  elioore  13303  ioorebas  13379  xnn0xrge0  13434  elfzuz2  13457  fzn0  13466  fz0  13467  uzsubsubfz  13474  fzdisj  13479  fzmmmeqm  13485  ssfzunsn  13498  elfz1b  13521  fzdif1  13533  fz0dif1  13534  elfz0ubfz0  13560  elfz0fzfz0  13561  fz0fzelfz0  13562  fz0fzdiffz0  13565  elfzmlbp  13567  difelfzle  13569  difelfznle  13570  nn0disj  13572  2ffzeq  13577  prednn  13579  fzon0  13605  fzoss1  13614  elfzo0z  13629  elfzo0le  13631  fzonmapblen  13636  fzofzim  13637  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  elfzonlteqm1  13669  fzonn0p1p1  13672  elfzo0l  13684  ssfzo12bi  13689  fzoopth  13690  ubmelm1fzo  13691  elfznelfzo  13701  elfzr  13709  fzind2  13716  injresinjlem  13718  injresinj  13719  subfzo0  13720  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  fleqceilz  13786  zmodidfzoimp  13833  modaddmodup  13869  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  om2uzrani  13887  uzrdgfni  13893  fzfi  13907  ssnn0fi  13920  nnsinds  13923  nn0sinds  13924  fsuppmapnn0fiub0  13928  expcl2lem  14008  m1expeven  14044  zzlesq  14141  crreczi  14163  expnngt1  14176  nn0opthlem2  14204  nn0opthi  14205  facp1  14213  facnn2  14217  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem3  14230  bcn1  14248  hashnn0pnf  14277  hashnnn0genn0  14278  hashnemnf  14279  hashv01gt1  14280  hashrabrsn  14307  hashrabsn01  14308  hashrabsn1  14309  hashunx  14321  elprchashprn2  14331  hashprdifel  14333  hash1snb  14354  hashgt12el  14357  hashgt12el2  14358  hashgt23el  14359  hashfz0  14367  hashfun  14372  hashf1lem2  14391  hash2prde  14405  hash2pwpr  14411  hashle2prv  14413  hashge2el2dif  14415  hashtpg  14420  hash2sspr  14424  exprelprel  14425  hash3tpde  14428  fi1uzind  14442  brfi1indALT  14445  iswrdi  14452  wrdf  14453  swrd00  14580  swrdcl  14581  swrdnd  14590  swrdnd2  14591  swrdnnn0nd  14592  swrdnd0  14593  swrd0  14594  pfx00  14610  pfx0  14611  pfxcl  14613  pfxnd0  14624  swrdswrdlem  14639  swrdswrd  14640  swrdccatin1  14660  pfxccatin12lem2a  14662  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  pfxccatin12  14668  pfxccat3  14669  swrdccat  14670  swrdccat3blem  14674  repswswrd  14719  cshword  14726  cshwidxmod  14738  cshwidxmodr  14739  cshwidx0  14741  cshwidxm1  14742  cshwidxm  14743  cshwidxn  14744  cshf1  14745  2cshw  14748  cshweqrep  14756  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  s7f1o  14901  trclfvcotr  14944  relexpsucl  14966  relexpsucr  14967  relexpcnv  14970  relexprelg  14973  relexpdmg  14977  relexprng  14981  relexpfld  14984  relexpaddg  14988  rexanuz  15281  fclim  15488  climmo  15492  rlimdiv  15581  caurcvg2  15613  fsum2dlem  15705  fsumcom2  15709  modfsummods  15728  arisum  15795  arisum2  15796  pwdif  15803  prodmo  15871  fprodfac  15908  fprod2dlem  15915  fprodcom2  15919  fallfacfac  15980  bpoly2  15992  bpoly3  15993  bpoly4  15994  ef01bndlem  16121  sin01gt0  16127  cos01gt0  16128  sin02gt0  16129  dvdsdivcl  16255  addmodlteqALT  16264  odd2np1  16280  oddge22np1  16288  m1expe  16313  nn0enne  16316  nn0o1gt2  16320  nno  16321  sumodd  16327  divalglem1  16333  divalglem6  16337  ndvdsadd  16349  gcdaddmlem  16463  dfgcd2  16485  mulgcd  16487  algcvgblem  16516  algfx  16519  lcmfn0val  16562  lcmftp  16575  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  coprmproddvdslem  16601  prmind2  16624  prm2orodd  16630  oddprmgt2  16638  ge2nprmge4  16640  maxprmfct  16648  dfphi2  16713  modprm0  16745  nnnn0modprm0  16746  prm23lt5  16754  prm23ge5  16755  pythagtriplem2  16757  pcz  16821  dvdsprmpweqnn  16825  oddprmdvds  16843  prmunb  16854  prmreclem3  16858  4sqlem4  16892  4sqlem19  16903  ramz  16965  fvprmselelfz  16984  prmgaplem3  16993  prmgaplem5  16995  prmgaplem6  16996  prmgaplem7  16997  cshwshashlem1  17035  cshwshashlem2  17036  cshwshash  17044  setsstruct2  17113  setsstruct  17115  ressval3d  17185  firest  17364  imasaddfnlem  17461  mreiincl  17527  mreunirn  17532  mremre  17535  fnmrc  17542  mrcfval  17543  fnhomeqhomf  17626  ismon2  17670  isepi2  17677  sscpwex  17751  funcres2b  17833  funcpropd  17838  funcres2c  17839  isfull  17848  isfth  17852  initoeu2lem1  17950  initoeu2  17952  homa1  17973  homahom2  17974  latlem  18372  latjcom  18382  latmcom  18398  clatlubcl2  18439  clatglbcl2  18441  cnvpsb  18514  opifismgm  18596  gsumval2  18623  mgmhmf  18634  mgmhmlin  18636  smndex1basss  18842  smndex1mndlem  18846  sgrp2nmndlem3  18862  pwmnd  18874  dfgrp3e  18982  mulgnn0gsum  19022  subgint  19092  giclcl  19214  gicrcl  19215  gicsym  19216  gicen  19219  gicsubgen  19220  cntzssv  19269  oppgsubm  19303  oppgsubg  19304  gsmsymgreqlem2  19372  f1otrspeq  19388  pmtrdifellem1  19417  pmtrdifellem2  19418  pmtrdifellem4  19420  gsmtrcl  19457  gexcl3  19528  sylow3lem6  19573  efgmnvl  19655  efgsf  19670  efgsrel  19675  efgs1b  19677  efgredlema  19681  efgredlemd  19685  efgrelexlema  19690  efgrelexlemb  19691  frgpnabllem1  19814  cygabl  19832  cyggex2  19838  giccyg  19841  gsumpr  19896  gsumzunsnd  19897  dprddomprc  19943  dprdval0prc  19945  dprdval  19946  dprdssv  19959  pgpfac1  20023  omndmul2  20074  rngdi  20107  rngdir  20108  srgbinomlem4  20176  dvdsrval  20309  isunit  20321  rnghmghm  20395  rnghmmul  20397  rimisrngim  20443  0ringnnzr  20470  0ring1eq0  20478  opprsubrng  20504  subrngint  20505  subrgsubrng  20523  opprsubrg  20538  subrgint  20540  rhmsubcrngclem1  20611  ringcbasbas  20618  srhmsubc  20625  drngmuleq0  20708  fldcat  20728  sdrgss  20738  abvn0b  20781  rmodislmodlem  20892  rmodislmod  20893  lmhmlem  20993  lmiclcl  21034  lmicrcl  21035  lmicsym  21036  lvecvscan  21078  lspsncv0  21113  cnsubdrglem  21385  prmirred  21441  nzerooringczr  21447  pzriprnglem4  21451  pzriprnglem6  21453  pzriprnglem12  21459  zlmlmod  21489  frgpcyg  21540  psgninv  21549  thlle  21664  lindfrn  21788  lmiclbs  21804  psrbagf  21886  mpfrcl  22052  psdmul  22121  coe1ae0  22169  gsummoncoe1  22264  ply1frcl  22274  pf1rcl  22305  pf1ind  22311  mat0dimcrng  22426  mulmarep1gsum2  22530  mdetralt  22564  symgmatr01lem  22609  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  pmatcollpw3fi1lem1  22742  pmatcollpw3fi1  22744  mp2pm2mplem4  22765  chpscmat  22798  chmaidscmat  22804  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  toprntopon  22881  distop  22951  ssntr  23014  isclo2  23044  indiscld  23047  neiptopuni  23086  lecldbas  23175  pnfnei  23176  mnfnei  23177  lmrcl  23187  cmpsublem  23355  cmpsub  23356  hauscmplem  23362  bwth  23366  iunconn  23384  2ndctop  23403  2ndcsb  23405  2ndcredom  23406  2ndc1stc  23407  2ndcdisj  23412  2ndcsep  23415  kgenuni  23495  kgenftop  23496  kgenss  23499  kgenidm  23503  iskgen3  23505  kgencn3  23514  txuni2  23521  dfac14  23574  txcn  23582  txindis  23590  kqtop  23701  kqt0  23702  hmeocnvb  23730  hmphref  23737  hmphsym  23738  hmphen  23741  haushmphlem  23743  cmphmph  23744  connhmph  23745  reghmph  23749  nrmhmph  23750  hmphdis  23752  hmphindis  23753  indishmph  23754  hmphen2  23755  ist1-5lem  23776  fbncp  23795  isfil2  23812  fbasfip  23824  fgcl  23834  filunirn  23838  cfinfil  23849  fiufl  23872  ufinffr  23885  isfcls  23965  alexsubALTlem2  24004  alexsubALTlem3  24005  tmdcn2  24045  ustbas  24183  xmetunirn  24293  lpbl  24459  blcld  24461  met1stc  24477  met2ndci  24478  dscmet  24528  qdensere  24725  blssioo  24751  xrtgioo  24763  divcnOLD  24825  iimulcl  24901  iimulcn  24902  iimulcnOLD  24903  iccpnfcnv  24910  isphtpc  24961  phtpc01  24963  cvsi  25098  ncvsi  25119  ncvsprp  25120  ncvsm1  25122  ncvsdif  25123  ncvspi  25124  ncvs1  25125  ncvspds  25129  cmetcaulem  25256  bcthlem4  25295  cmssmscld  25318  rrx0  25365  ehl1eudis  25388  ehl2eudis  25390  elovolm  25444  ovolmge0  25446  ovolgelb  25449  iunmbl  25522  iunmbl2  25526  ioombl1  25531  ioorcl2  25541  ioorf  25542  ioorinv2  25544  ioorinv  25545  ioorcl  25546  dyaddisj  25565  dyadmax  25567  opnmblALT  25572  vitali  25582  mbfid  25604  itg1addlem4  25668  itg2uba  25712  itg2splitlem  25717  limcdif  25845  ellimc2  25846  limcres  25855  limccnp  25860  dvexp2  25926  dvexp3  25950  elply2  26169  plyssc  26173  elqaa  26298  aannenlem1  26304  aannenlem2  26305  aannenlem3  26306  aaliou2  26316  taylfval  26334  ulmscl  26356  pserdvlem2  26406  reeff1o  26425  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12gt0  26484  logfac  26578  dvloglem  26625  logf1o2  26627  logtayl  26637  cxpexp  26645  2irrexpq  26708  resqrtcn  26727  logbcl  26745  elogb  26748  logbchbase  26749  relogbreexp  26753  relogbmul  26755  relogbcxp  26763  cxplogb  26764  logbf  26767  logblog  26770  reasinsin  26874  birthdaylem1  26929  harmonicbnd3  26986  igamgam  27027  wilthimp  27050  sqff1o  27160  musum  27169  fsumdvdsmul  27173  bpos1  27262  zabsle1  27275  gausslemma2dlem0f  27340  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  gausslemma2dlem4  27348  2lgslem1a1  27368  2lgslem3  27383  2lgsoddprmlem3  27393  2lgsoddprm  27395  2sqlem2  27397  2sqlem10  27407  2sq2  27412  2sqnn0  27417  2sqnn  27418  chebbnd1  27451  chtppilim  27454  chpo1ub  27459  dchrisum0lem2a  27496  rplogsum  27506  pnt2  27592  ostth  27618  nofun  27629  nodmon  27630  norn  27631  ltsval2  27636  ltsintdifex  27641  ltsres  27642  nosepnelem  27659  noresle  27677  sltsex1  27771  sltsex2  27772  sltsss1  27773  sltsss2  27774  sltssep  27775  sltstr  27795  sltsun1  27796  sltsun2  27797  cutsf  27800  eqcuts3  27812  bday1  27822  sltsleft  27868  sltsright  27869  cofcutr  27932  addsprop  27984  sltmuls1  28155  sltmuls2  28156  precsexlem11  28225  oncutlt  28272  nnsge1  28351  n0fincut  28363  onsfi  28364  dfnns2  28380  n0zs  28397  zaddscl  28402  eln0zs  28408  zsbday  28414  zcuts  28415  zcuts0  28416  zseo  28430  z12no  28484  z12shalf  28488  z12zsodd  28490  tglnunirn  28632  axlowdimlem13  29039  axlowdim1  29044  axcontlem4  29052  elntg2  29070  snstrvtxval  29122  snstriedgval  29123  vtxvalprc  29130  iedgvalprc  29131  umgrislfupgrlem  29207  upgredg  29222  umgredg  29223  ausgrusgrb  29250  usgruspgrb  29268  usgrislfuspgr  29272  uhgr2edg  29293  uspgredg2v  29309  usgredg2v  29312  uhgr0edgfi  29325  lfuhgr1v0e  29339  usgr1v  29341  usgrexmplef  29344  griedg0ssusgr  29350  subusgr  29374  upgrreslem  29389  umgrreslem  29390  fusgrfis  29415  nbgrisvtx  29426  nbupgr  29429  nbumgrvtx  29431  nbgr2vtx1edg  29435  nbuhgr2vtx1edgblem  29436  nbgr1vtx  29443  nbupgrres  29449  nb3grprlem1  29465  nb3grprlem2  29466  uvtx01vtx  29482  cusgredg  29509  cplgr1vlem  29514  cplgr1v  29515  cusgrsizeinds  29538  fusgrmaxsize  29550  vtxdg0e  29560  fusgrn0degnn0  29585  uhgrvd00  29620  vtxdginducedm1lem4  29628  vtxdginducedm1  29629  finsumvtxdg2ssteplem4  29634  fusgrregdegfi  29655  rgrusgrprc  29675  wlk2f  29715  wlkcompim  29717  wlk1walk  29724  uspgr2wlkeqi  29733  g0wlk0  29736  wlkreslem  29753  wlkdlem4  29769  lfgrwlkprop  29771  lfgriswlk  29772  trlf1  29782  pthdivtx  29812  dfpth2  29814  spthdifv  29818  spthdep  29819  pthdepisspth  29820  upgrwlkdvdelem  29821  spthonepeq  29837  uhgrwkspthlem2  29839  usgr2wlkneq  29841  pthdlem2lem  29852  cyclnumvtx  29885  cyclnspth  29886  uspgrn2crct  29893  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  crctcshwlkn0lem7  29901  crctcshtrl  29908  wwlknp  29928  wlkswwlksf1o  29964  wwlksm1edg  29966  wlknewwlksn  29972  wlknwwlksnbij  29973  wwlksnext  29978  wwlksnndef  29990  wspthsnwspthsnon  30001  wspthsnonn0vne  30002  wspn0  30009  wwlks2onv  30038  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgrnumwwlkslem  30057  rusgrnumwwlks  30062  clwwlk1loop  30075  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlkflem  30091  clwwisshclwwslem  30101  clwwlkneq0  30116  clwwlknwrd  30121  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkext2edg  30143  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  umgr2cwwkdifex  30152  eleclclwwlkn  30163  clwlknf1oclwwlknlem1  30168  clwlknf1oclwwlkn  30171  clwwlknon  30177  clwwlknonfin  30181  clwwlknonex2lem2  30195  clwwlknonex2e  30197  clwwlkvbij  30200  0spth  30213  uhgr3cyclexlem  30268  1conngr  30281  eupth2lem3lem4  30318  eulerpath  30328  eulercrct  30329  eucrctshift  30330  eucrct2eupth  30332  konigsberglem5  30343  frcond4  30357  frgr1v  30358  frgr3vlem1  30360  frgr3vlem2  30361  3vfriswmgrlem  30364  1to2vfriswmgr  30366  1to3vfriswmgr  30367  2pthfrgrrn  30369  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrncvvdeqlem7  30392  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  frgrwopreglem4a  30397  frgrwopreglem2  30400  frgrwopreg1  30405  frgrwopreg2  30406  frgrwopreglem5ALT  30409  frgrwopreg  30410  frgrregorufr0  30411  frgrregorufr  30412  frgrhash2wsp  30419  clwwnonrepclwwnon  30432  2clwwlk2clwwlklem  30433  2clwwlk2clwwlk  30437  numclwwlk1lem2fo  30445  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  frgrregord013  30482  nmobndseqi  30867  nmobndseqiALT  30868  ipasslem5  30923  h2hcau  31067  hvsubeq0i  31151  hvmulcan  31160  hvmulcan2  31161  bcsiALT  31267  hlimf  31325  isch3  31329  hsn0elch  31336  hhssnv  31352  shintcli  31417  hsupcl  31427  hsupunss  31431  sshjcl  31443  shsleji  31458  shsidmi  31472  hsupval2  31497  sshjval2  31499  spanuni  31632  h1de2i  31641  spanunsni  31667  cmbr3i  31688  osumcor2i  31732  spansncvi  31740  5oalem7  31748  3oalem3  31752  pjss2i  31768  pjssmii  31769  mayete3i  31816  nmop0h  32079  riesz3i  32150  nmopcoi  32183  opsqrlem5  32232  pjnmopi  32236  pjorthcoi  32257  pjssdif1i  32263  dfpjop  32270  elpjch  32277  pjin2i  32281  pjclem1  32283  pjclem2  32284  pjclem4a  32286  pj3lem1  32294  strlem1  32338  strlem3  32341  strlem4  32342  strlem5  32343  stri  32345  hstrlem3  32349  hstrlem4  32350  hstrlem5  32351  hstri  32353  dmdbr5  32396  mdsl1i  32409  mdslmd1lem2  32414  atne0  32433  atom1d  32441  shatomici  32446  chrelat2i  32453  atssma  32466  chirredi  32482  cmmdi  32504  sumdmdi  32508  dmdbr4ati  32509  dmdbr5ati  32510  dmdbr6ati  32511  dmdbr7ati  32512  cdj3lem1  32522  opreu2reuALT  32563  2reu2reu2  32569  reuxfrdf  32577  rexunirn  32578  elim2ifim  32632  iuninc  32647  iunpreima  32651  fcoinver  32691  br8d  32698  ac6sf2  32712  unipreima  32733  xppreima  32735  2ndimaxp  32736  xrofsup  32858  xrsclat  33104  gsummpt2co  33142  cntzun  33173  fzto1st  33197  psgnfzto1st  33199  isarchi3  33281  1fldgenq  33416  krull  33572  crefdf  34026  xrge0iifcnv  34111  xrge0iifiso  34113  xrge0iifhom  34115  esumc  34229  esumpinfval  34251  hasheuni  34263  esumiun  34272  ofcfval  34276  volmeas  34409  ddemeas  34414  truae  34421  sxbrsigalem0  34449  dya2icobrsiga  34454  dya2iocucvr  34462  sxbrsigalem2  34464  omssubaddlem  34477  omssubadd  34478  carsggect  34496  eulerpartlemgc  34540  eulerpartlemb  34546  eulerpartlemf  34548  eulerpartlemr  34552  sseqfn  34568  sseqf  34570  ballotlem2  34667  ballotlem7  34714  plymulx0  34725  plymulx  34726  signstfvn  34747  signsvfn  34760  chtvalz  34807  tgoldbachgt  34841  bnj158  34906  bnj228  34912  bnj563  34920  bnj832  34935  bnj835  34936  bnj836  34937  bnj837  34938  bnj769  34939  bnj770  34940  bnj771  34941  bnj1098  34960  bnj1143  34966  bnj1232  34979  bnj1238  34982  bnj1254  34985  bnj1385  35008  bnj1533  35028  bnj110  35034  bnj98  35043  bnj517  35061  bnj518  35062  bnj535  35066  bnj543  35069  bnj544  35070  bnj546  35072  bnj570  35081  bnj605  35083  bnj590  35086  bnj594  35088  bnj600  35095  bnj906  35106  bnj916  35109  bnj944  35114  bnj953  35115  bnj970  35123  bnj998  35133  bnj1006  35136  bnj1018g  35139  bnj1018  35140  bnj1118  35160  bnj1128  35166  bnj1125  35168  bnj1145  35169  bnj1498  35237  funen1cnv  35265  r1omfi  35282  axprALT2  35287  fineqvac  35294  fineqvnttrclselem1  35299  fineqvnttrclselem2  35300  axregscl  35306  axregszf  35307  setinds2regs  35309  lfuhgr  35334  lfuhgr3  35336  acycgr0v  35364  prclisacycgr  35367  subfacval3  35405  erdszelem2  35408  kur14lem7  35428  kur14lem9  35430  rellysconn  35467  cvmliftlem15  35514  cvmlift2lem12  35530  satfv0  35574  satfrnmapom  35586  satfv0fun  35587  satf0suc  35592  sat1el2xp  35595  fmla1  35603  gonarlem  35610  gonar  35611  goalr  35613  satffunlem1lem1  35618  satffunlem2lem1  35620  satfvel  35628  satefvfmla0  35634  ex-sategoelel  35637  mrsubcv  35726  msrid  35761  mppsval  35788  elmpps  35789  untangtr  35930  fz0n  35947  bccolsum  35955  br8  35972  br6  35973  br4  35974  eldm3  35977  opelco3  35991  dfon2lem3  35999  dfon2lem7  36003  dfon2lem8  36004  dfrdg2  36009  txpss3v  36092  pprodss4v  36098  fnimage  36143  imageval  36144  dfrdg4  36167  altopthsn  36177  altxpsspw  36193  linethru  36369  rankeq1o  36387  finminlem  36534  nn0prpwlem  36538  nn0prpw  36539  cldbnd  36542  fnemeet2  36583  waj-ax  36630  subsym1  36643  ordtoplem  36651  onsucconni  36653  onintopssconn  36656  onsuct0  36657  limsucncmpi  36661  ordcmp  36663  onint1  36665  bj-ififc  36807  bj-andnotim  36813  bj-ax12ig  36872  bj-cbveaw  36886  bj-cbvaew  36887  bj-ssbid2ALT  36908  bj-19.12  36966  bj-nnfalt  37028  bj-nnfext  37029  bj-hbs1  37060  bj-sblem  37092  bj-sbievw1  37093  bj-sbievw2  37094  bj-sbievw  37095  bj-vtoclg1f1  37165  bj-xpnzex  37207  bj-snglss  37218  bj-0nelsngl  37219  bj-snglex  37221  bj-tagci  37232  bj-bm1.3ii  37312  bj-rep  37321  bj-axseprep  37322  bj-restsnss  37336  bj-restsnss2  37337  bj-rest10b  37342  bj-0int  37354  bj-ismoored0  37359  bj-ismooredr2  37363  bj-snmoore  37366  bj-prmoore  37368  copsex2b  37395  bj-brresdm  37401  bj-idres  37415  bj-xpcossxp  37444  bj-ccinftydisj  37468  taupi  37578  mptsnunlem  37593  topdifinffinlem  37602  topdifinfeq  37605  icoreclin  37612  iooelexlt  37617  relowlssretop  37618  relowlpssretop  37619  rdgeqoa  37625  finxp1o  37647  pibt2  37672  wl-moteq  37769  wl-sb8et  37808  wl-2spsbbi  37820  wl-mo3t  37831  uncf  37850  curfv  37851  unccur  37854  finixpnum  37856  sin2h  37861  cos2h  37862  tan2h  37863  ptrecube  37871  poimirlem4  37875  poimirlem23  37894  poimirlem25  37896  poimirlem26  37897  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  heicant  37906  mblfinlem3  37910  ismblfin  37912  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  mbfposadd  37918  dvtan  37921  itg2addnclem  37922  itgaddnclem2  37930  ftc1anclem3  37946  dvasin  37955  areacirclem1  37959  areacirclem4  37962  fdc  37996  subspopn  38003  sstotbnd3  38027  totbndbnd  38040  heiborlem3  38064  heiborlem8  38069  ismgmOLD  38101  isexid2  38106  exidcl  38127  grposnOLD  38133  rngo1cl  38190  riscer  38239  divrngidl  38279  smprngopr  38303  orfa  38333  tsbi3  38386  relcnveq3  38578  rsp3  38617  mopickr  38622  moantr  38623  xrnss3v  38632  refressn  38784  refrelredund2  38971  eldisjim3  39066  eldisjdmqsim  39068  dmqsblocks  39218  prtlem9  39240  prtlem16  39245  prtlem14  39250  axc11n-16  39314  opposet  39557  op01dm  39559  hlsuprexch  39757  hlhgt4  39764  atex  39782  dalemkehl  39999  dalempea  40002  dalemqea  40003  dalemrea  40004  dalemsea  40005  dalemtea  40006  dalemuea  40007  dalemyeo  40008  dalemzeo  40009  dalemclpjs  40010  dalemclqjt  40011  dalemclrju  40012  dalem-clpjq  40013  dalemceb  40014  dalemcnes  40026  dalempnes  40027  dalemqnet  40028  dalemswapyz  40032  dalemrot  40033  dalem5  40043  dalem-cly  40047  dalemccea  40059  dalemddea  40060  dalem-ddly  40062  dalemccnedd  40063  dalemclccjdd  40064  linepsubN  40128  pmapsub  40144  paddasslem9  40204  paddasslem10  40205  pclfinN  40276  pclcmpatN  40277  4atexlemk  40423  4atexlemw  40424  4atexlempw  40425  4atexlemq  40427  4atexlems  40428  4atexlemt  40429  4atexlemutvt  40430  4atexlempnq  40431  4atexlemnslpq  40432  4atexlemswapqr  40439  4atexlemnclw  40446  4atexlemcnd  40448  isltrn2N  40496  dochsnkrlem1  41845  aks6d1c6lem1  42540  aks6d1c6lem3  42542  fisdomnn  42614  nnn1suc  42636  readvcot  42734  sn-0tie0  42821  ricsym  42889  prjspertr  42963  prjspersym  42965  cmpfiiin  43054  ismrcd1  43055  isnacs3  43067  fzsplit1nn0  43111  eldiophss  43131  2nn0ind  43302  jm2.23  43353  expdiophlem1  43378  expdioph  43380  setindtrs  43382  dfac11  43419  lnmlmic  43445  gicabl  43456  isnumbasgrplem2  43461  dfacbasgrp  43465  hbtlem5  43485  itgocn  43521  onsupcl2  43582  onsupuni2  43587  onsupintrab2  43589  onuniintrab2  43592  limnsuc  43622  omge2  43655  cantnf2  43682  dflim5  43686  omabs2  43689  onsucunipr  43729  safesnsupfidom1o  43773  faosnf0.11b  43783  ifpbi13  43845  dfsucon  43879  sn1dom  43882  infordmin  43888  pr2eldif1  43910  pr2eldif2  43911  relintabex  43937  cnvrcl0  43981  relexpmulg  44066  iunrelexpmin2  44068  relexp0a  44072  relexpxpmin  44073  brtrclfv2  44083  snhesn  44142  frege55b  44253  frege65b  44266  frege55lem1c  44272  frege55c  44274  frege70  44289  frege131  44350  frege133  44352  ntrk0kbimka  44395  clsk1indlem3  44399  ntrf2  44480  grucollcld  44616  mnurndlem1  44637  grumnudlem  44641  nanorxor  44661  dvradcnv2  44703  pm10.251  44716  pm11.63  44751  axc11next  44762  iotain  44773  iotasbc  44775  bi123imp0  44852  2sb5nd  44916  uun132  45140  uun132p1  45141  uun2131p1  45147  ax6e2eqVD  45262  2sb5ndVD  45265  2sb5ndALT  45287  orbitcl  45313  xpwf  45320  dmwf  45321  rnwf  45322  wfaxsep  45351  wfaxpow  45353  wfac8prim  45358  permaxext  45361  permac8prim  45370  r19.36vf  45495  r19.3rzf  45517  disjinfi  45551  rnmptssf  45605  rnmptssff  45632  dvnprodlem1  46304  stirlinglem13  46444  fourierdlem76  46540  fourierdlem87  46551  fourierswlem  46588  natglobalincr  47235  hirstL-ax3  47252  absnsb  47387  eldmressn  47397  funressnfv  47403  fsetprcnexALT  47422  rexrsb  47460  euoreqb  47469  2reu3  47470  2reu8i  47473  2reuimp0  47474  dfatelrn  47491  afvpcfv0  47506  afvfv0bi  47512  afveu  47513  afvres  47532  tz6.12-afv  47533  afvco2  47536  aovvdm  47545  aovvfunressn  47547  aovrcl  47549  aovnuoveq  47551  aovvoveq  47552  aovovn0oveq  47554  aoprssdm  47562  ndmaovass  47566  ndmaovdistr  47567  funressndmafv2rn  47583  afv2ndefb  47584  afv2res  47599  tz6.12-afv2  47600  dfatsnafv2  47612  dfatdmfcoafv2  47614  dfatcolem  47615  afv2ndeffv0  47620  afv2fv0  47625  otiunsndisjX  47639  funop1  47643  fvmptrabdm  47653  zm1nn  47662  eluzge0nn0  47672  ssfz12  47674  2elfz3nn0  47676  elfzelfzlble  47681  fzopredsuc  47683  1fzopredsuc  47684  subsubelfzo0  47686  2tceilhalfelfzo1  47692  ceilhalfnn  47696  zplusmodne  47703  plusmod5ne  47705  minusmod5ne  47709  submodlt  47710  m1modnep2mod  47712  m1modmmod  47718  mod2addne  47724  modm2nep1  47726  modp2nep1  47727  modm1nep2  47728  modm1nem2  47729  modm1p1ne  47730  iccpartiltu  47782  iccpartigtl  47783  iccpartgt  47787  iccelpart  47793  iccpartnel  47798  fargshiftf1  47801  ich2exprop  47831  ichnreuop  47832  ichreuopeq  47833  sprssspr  47841  sprsymrelfvlem  47850  sprsymrelfo  47857  prproropf1olem4  47866  sbcpr  47881  reupr  47882  odz2prm2pw  47923  fmtnofac1  47930  fmtno4prmfac  47932  fmtnofz04prm  47937  prmdvdsfmtnof1lem1  47944  prmdvdsfmtnof  47946  prmdvdsfmtnof1  47947  prminf2  47948  31prm  47957  lighneallem2  47966  lighneallem3  47967  lighneallem4b  47969  lighneallem4  47970  evenm1odd  47999  evenp1odd  48000  evennodd  48003  oddneven  48004  m1expevenALTV  48007  opoeALTV  48043  opeoALTV  48044  oddprmALTV  48047  nn0o1gt2ALTV  48054  nnoALTV  48055  nn0oALTV  48056  oddprmuzge3  48076  perfectALTVlem2  48082  fppr2odd  48091  fpprel2  48101  gbepos  48118  gbowpos  48119  gbegt5  48121  gbowgt5  48122  gbowge7  48123  gboge9  48124  sbgoldbalt  48141  sbgoldbm  48144  sbgoldbo  48147  nnsum3primesgbe  48152  nnsum3primesle9  48154  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  evengpop3  48158  evengpoap3  48159  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  clnbgrisvtx  48190  isubgredg  48226  upgrimwlklem2  48258  gricrcl  48274  gricen  48285  cycldlenngric  48288  clnbgrgrim  48294  usgrgrtrirex  48310  grlicrcl  48367  grilcbri2  48371  grlicen  48377  gricgrlic  48378  usgrexmpl12ngric  48398  usgrexmpl12ngrlic  48399  gpgprismgriedgdmss  48412  gpgusgralem  48416  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpg3nbgrvtx0  48436  gpgprismgr4cycllem2  48456  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem10  48464  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  pgnbgreunbgrlem6  48484  uspgrsprf  48506  uspgrsprfo  48508  ovn0dmfun  48516  opmpoismgm  48527  assintop  48569  2zlidl  48600  2zrngamgm  48605  2zrngagrp  48609  2zrngnmrid  48616  cznnring  48622  ringcbasbasALTV  48672  srhmsubcALTV  48685  fldcatALTV  48691  ztprmneprm  48707  linccl  48774  ldepsnlinclem1  48865  ldepsnlinclem2  48866  elfzolborelfzop1  48879  elbigof  48914  elbigodm  48915  rege1logbrege0  48918  relogbmulbexp  48921  relogbdivb  48922  fllog2  48928  blennn0elnn  48937  blen1b  48948  nnolog2flm1  48950  nn0digval  48960  dignn0fr  48961  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  0aryfvalel  48994  rrx2xpref1o  49078  eenglngeehlnmlem1  49097  rrx2linest  49102  rrx2linesl  49103  line2ylem  49111  mosssn  49174  mo0sn  49175  mofsssn  49205  mofmo  49206  f102g  49211  tposres0  49236  f1omo  49252  i0oii  49279  iscnrm3lem4  49295  oppcendc  49377  sectrcl  49381  invrcl  49383  isoval2  49394  cicrcl2  49402  funcf2lem2  49441  idemb  49518  setcsnterm  49849  isinito3  49859  termc2  49877  2arwcat  49959  setc1onsubc  49961  rellan  49982  relran  49983  termolmd  50029  setrec2lem2  50053  ifnmfalse  50122  aacllem  50160