Theorem mpan2 692

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	⊢ 𝜓
mpan2.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpan2	⊢ (𝜑 → 𝜒)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpan2.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpdan 688	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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  df-an 396

This theorem is referenced by:  mpanr12  706  mp3an23  1456  elvd  3448  elabg  3633  eueq2  3670  sbcgf  3813  sbcralg  3826  csbconstgf  3869  sbcnestgw  4377  csbnestgw  4378  sbcnestg  4382  csbnestg  4383  csbnest1g  4386  iinexg  5295  eusv2nf  5342  reusv2lem5  5349  nnullss  5417  xpss1  5651  xpiindi  5792  reldm0  5885  elrnmpt1s  5916  resdm  5993  eliniseg  6061  trinxp  6090  ssrnres  6144  cnveq0  6163  coi2  6230  relrelss  6239  cnviin  6252  elpred  6284  onelssex  6374  ord0eln0  6381  funcnvres  6578  funimaex  6588  fnresin1  6625  fnresin2  6626  fresin  6711  ssimaex  6927  fvmpt  6949  fvmptnf  6972  fvimacnvALT  7011  dff3  7054  fsn  7090  fsn2  7091  funop  7104  fvrnressn  7116  fnsnbg  7120  fninfp  7130  fndifnfp  7132  fnnfpeq0  7134  fprb  7150  elabrex  7198  elabrexg  7199  f1elima  7219  f1ofvswap  7262  fliftel1  7266  f1owe  7309  sorpssuni  7687  sorpssint  7688  eldifpw  7723  ordeleqon  7737  ordsson  7738  ssnlim  7838  abrexexg  7915  tposfun  8194  tpostpos2  8199  fpr3g  8237  wfr3g  8271  tfrlem10  8328  tfrlem12  8330  tfr3  8340  seqomlem1  8391  seqomlem2  8392  seqomlem4  8394  ondif2  8439  oa0  8453  om0  8454  oa1suc  8468  om1  8479  oe1  8481  oe1m  8482  omass  8517  om2  8523  oeoalem  8534  oeoelem  8536  nnmsucr  8563  nnm1  8590  nnm2  8591  naddrid  8621  naddlid  8622  ecelqs  8716  xpider  8737  mapdm0  8791  fvdiagfn  8841  ixpsnf1o  8888  xp1en  9003  undom  9005  sbthlem7  9033  domunsn  9067  xpmapenlem  9084  infensuc  9095  findcard2d  9103  diffi  9111  cnvfi  9112  enreffi  9119  snnen2o  9157  1sdom2dom  9166  infi  9182  finresfin  9184  unblem1  9204  unblem2  9205  unblem3  9206  unblem4  9207  isfinite2  9210  infn0ALT  9215  unfilem1  9217  unfilem2  9218  unfir  9220  fofinf1o  9244  cnvfiALT  9251  mptfi  9263  finsschain  9271  imafi2  9273  marypha2  9354  inf0  9542  trcl  9649  frr3g  9680  r1rankidb  9728  snwf  9733  unwf  9734  uniwf  9743  rankval3b  9750  rankr1a  9760  rankxplim3  9805  scott0  9810  djueq1  9829  card1  9892  pm54.43  9925  infxpenc2  9944  dfac8clem  9954  alephsuc2  10002  alephle  10010  cardaleph  10011  dfac12lem2  10067  undjudom  10090  djudom1  10105  pwdju1  10113  nnadju  10120  ackbij1lem18  10158  cflem  10167  cflemOLD  10168  cflecard  10175  cfeq0  10178  cfslb  10188  cfsmolem  10192  cfcoflem  10194  cfidm  10197  isfin4p1  10237  fin23lem12  10253  fin23lem16  10257  fin23lem28  10262  fin23lem38  10271  fin23lem41  10274  fin1a2lem7  10328  fin1a2lem12  10333  fin1a2lem13  10334  hsmexlem8  10346  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ac6num  10401  ttukeylem4  10434  ttukeylem7  10437  ttukey2g  10438  axdclem  10441  brdom3  10450  brdom5  10451  cardeq0  10474  unsnen  10475  konigthlem  10491  pwcfsdom  10506  canthp1lem1  10575  wunex2  10661  wuncval2  10670  eltsk2g  10674  ingru  10738  grutsk  10745  axgroth6  10751  mulidpi  10809  nlt1pi  10829  indpi  10830  pinq  10850  mulidnq  10886  1idpr  10952  prlem934  10956  0idsr  11020  1idsr  11021  00sr  11022  negexsr  11025  recexsrlem  11026  sqgt0sr  11029  ax1rid  11084  axcnre  11087  ne0gt0  11250  peano2cn  11317  peano2re  11318  00id  11320  mul02lem2  11322  mul01  11324  subid  11412  subid1  11413  negid  11440  negeq0  11447  peano2cnm  11459  peano2rem  11460  lt0neg1  11655  le0neg1  11657  relin01  11673  div2neg  11876  recgt0ii  12060  divgt0i2i  12069  ledivp1i  12079  ltdivp1i  12080  inelr  12147  peano5nni  12160  peano2nn  12169  nnge1  12185  nnne0  12191  times2  12289  addltmul  12389  nn0p1nn  12452  peano2nn0  12453  nn0lele2xi  12469  fcdmnn0supp  12470  fcdmnn0fsupp  12471  fcdmnn0suppg  12472  peano2z  12544  peano2zm  12546  suprzcl  12584  zeo  12590  eluzaddi  12794  uzwo  12836  uzwo2  12837  infssuzle  12856  infssuzcl  12857  zq  12879  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  rphalfcl  12946  zgt1rpn0n1  12960  ltpnf  13046  nltmnf  13055  pnfge  13056  nltpnft  13091  xlemnf  13094  qsqueeze  13128  xlt0neg1  13146  xle0neg1  13148  xaddpnf1  13153  xaddmnf1  13155  xaddrid  13168  xsubge0  13188  xmul01  13194  xmulneg1  13196  xmulpnf1  13201  xmulrid  13206  supxrbnd  13255  supxrgtmnf  13256  supxrre1  13257  supxrre2  13258  elioopnf  13371  elicopnf  13373  iccshftri  13415  iccshftli  13417  iccdili  13419  icccntri  13421  fzprval  13513  fz0add1fz1  13663  fzofzp1  13692  fzostep1  13714  injresinj  13719  flge0nn0  13752  flge1nn  13753  btwnzge0  13760  modfrac  13816  om2uzsuci  13883  axdc4uzlem  13918  ser1const  13993  exp0  14000  exp1  14002  expn1  14006  nn0sqcl  14024  sqval  14049  sqeq0  14055  resqcl  14059  zsqcl  14064  expubnd  14113  binom21  14154  expnbnd  14167  nn0opthlem2  14204  bcnn  14247  bcn2  14254  bcn2p1  14260  bcnm1  14262  hasheq0  14298  hashsng  14304  hashen1  14305  hashunsnggt  14329  hashin  14346  hashdif  14348  hashgt23el  14359  hashxplem  14368  hashf1lem2  14391  hash2pr  14404  hash2prde  14405  pr2pwpr  14414  hash3tr  14426  iswrd  14450  wrdval  14451  hashwrdn  14482  ccatval2  14513  ccatrid  14523  eqs1  14548  s111  14551  ccatws1len  14556  repsw0  14712  repsw1  14718  cshw0  14729  wwlktovf  14891  relexpsucnnl  14965  reim0  15053  imval2  15086  cjne0  15098  abssq  15241  max0add  15245  abs2dif  15268  rddif  15276  absrdbnd  15277  rexuz3  15284  isershft  15599  isercolllem2  15601  isercoll  15603  fsum  15655  fsumadd  15675  fsumsplitsnun  15690  bcxmas  15770  infcvgaux2i  15793  fprod  15876  risefac0  15962  fallfac0  15963  risefac1  15968  fallfac1  15969  bpoly2  15992  bpoly3  15993  bpoly4  15994  fsumcube  15995  efi4p  16074  resin4p  16075  recos4p  16076  sinbnd  16117  cosbnd  16118  rpnnen2lem8  16158  rpnnen2lem12  16162  cnso  16184  dvdsmul2  16217  dvdslelem  16248  odd2np1lem  16279  mod2eq1n2dvds  16286  divalglem0  16332  divalglem1  16333  divalglem4  16335  divalglem5  16336  divalglem8  16339  flodddiv4  16354  bits0  16367  bitsp1o  16372  bitsf1  16385  sadadd2lem2  16389  gcd1  16467  lcm0val  16533  dvdslcm  16537  lcmeq0  16539  lcmgcd  16546  lcm1  16549  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  prm2orodd  16630  phiprm  16716  pc0  16794  pcdvdstr  16816  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  hashbc0  16945  setsval  17106  fsets  17108  setsres  17117  ressinbas  17184  ressress  17186  elrestr  17360  pwssnf1o  17431  xpsfrnel  17495  xpscf  17498  ismred2  17534  submre  17536  mreacs  17593  oppchomfval  17649  brssc  17750  isssc  17756  yonedalem4c  18212  oduleval  18224  isprs  18231  oduclatb  18442  chninf  18570  gsumval2a  18622  smndex1n0mnd  18849  mulg1  19023  mulgnegnn  19026  isghmOLD  19157  ghmghmrn  19176  cntrnsg  19285  oppgplusfval  19289  pgrpsubgsymg  19350  psgneldm2i  19446  efgrelexlemb  19691  frgp0  19701  frgpmhm  19706  vrgpf  19709  cntrcmnd  19783  cntrabl  19784  cygctb  19833  dprd0  19974  dprd2da  19985  mgpplusg  20091  opprmulfval  20287  subrngint  20505  subrgint  20540  lsp0  20972  rlmval2  21156  cncrng  21355  cnfld1  21360  zringcyg  21436  mulgrhm2  21445  zlmsca  21487  fermltlchr  21496  chrnzr  21497  zrhpsgnelbas  21561  ocvz  21645  cssincl  21655  css0  21656  css1  21657  frlmip  21745  fczpsrbag  21889  ply1idvr1OLD  22251  evls1rhmlem  22277  evl1fval1lem  22286  marrepeval  22519  decpmatid  22726  0opn  22860  topopn  22862  basdif0  22909  tgval  22911  isopn2  22988  0cld  22994  ntropn  23005  ntrval2  23007  ntrdif  23008  clsdif  23009  cmclsopn  23018  ntrtop  23026  ntr0  23037  mretopd  23048  neips  23069  neiptopnei  23088  maxlp  23103  isperf2  23108  rest0  23125  iocpnfordt  23171  icomnfordt  23172  mnfnei  23177  refref  23469  unisngl  23483  1stckgen  23510  ptbasfi  23537  pthaus  23594  fbssfi  23793  isfil2  23812  ssfg  23828  filconn  23839  fbasrn  23840  filufint  23876  imaelfm  23907  fmfnfmlem4  23913  fclsfnflim  23983  alexsubALTlem3  24005  alexsubALTlem4  24006  ustfilxp  24169  ustuqtop2  24198  ustuqtop4  24200  utopsnneiplem  24203  utopsnnei  24205  utop2nei  24206  cfiluweak  24250  neipcfilu  24251  xmetres  24320  metres  24321  mopnex  24475  prdsms  24487  metucn  24527  tngds  24604  tngngp3  24612  nmoge0  24677  cnfldnm  24734  tgioo  24752  xrtgioo  24763  xrsmopn  24769  negcncf  24883  negcncfOLD  24884  phtpy01  24952  pco0  24982  tcphtopn  25194  tchnmfval  25196  caussi  25265  rrxip  25358  minveclem3b  25396  ovolfioo  25436  ovolficc  25437  ovolfsf  25440  ovolctb  25459  ovolctb2  25461  ovolfiniun  25470  ovoliun2  25475  ovolshftlem1  25478  ovolscalem1  25482  ovolicopnf  25493  iunmbl2  25526  uniioombllem2  25552  opnmblALT  25572  ismbf  25597  mbfinf  25634  0plef  25641  itg1climres  25683  itg2cnlem1  25730  iblitg  25737  ibl0  25756  itgcn  25814  cnlimc  25857  dvfre  25923  dvnfre  25924  dveflem  25951  dvef  25952  dvlipcn  25967  lhop2  25988  itgsubstlem  26023  deg1val  26069  ply1rem  26139  coefv0  26221  plyrecj  26255  vieta1lem2  26287  aannenlem1  26304  aaliou2b  26317  ulmval  26357  ulmpm  26360  ulmdvlem1  26377  mtest  26381  efcn  26421  sin2pim  26462  cos2pim  26463  sinmpi  26464  cosmpi  26465  sinppi  26466  cosppi  26467  efimpi  26468  sincosq1lem  26474  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12gt0  26484  sinq34lt0t  26486  sincosq1eq  26489  abssinper  26498  efif1o  26523  loglt1b  26611  relogcn  26615  ellogdm  26616  efopn  26635  cxp0  26647  cxp1  26648  cxpsqrt  26680  logsqrt  26681  logb1  26747  atandm3  26856  atanbnd  26904  atancn  26914  leibpi  26920  efrlim  26947  efrlimOLD  26948  logdifbnd  26972  vmaprm  27095  ppip1le  27139  ppieq0  27154  prmorcht  27156  ppiublem1  27181  ppiub  27183  chpeq0  27187  chtub  27191  fsumvma  27192  pclogsum  27194  chpval2  27197  dchrresb  27238  dchrptlem1  27243  lgs0  27289  lgs2  27293  lgsdir2lem2  27305  lgsdir2lem4  27307  lgsdchrval  27333  lgsdchr  27334  lgseisenlem2  27355  2lgslem1c  27372  2lgsoddprmlem2  27388  addsq2nreurex  27423  dirith2  27507  selberg2lem  27529  qabvle  27604  qabvexp  27605  ostth  27618  noextendseq  27647  noetasuplem4  27716  noetainflem4  27720  cutsun12  27798  madebdayim  27896  bdayiun  27923  addsrid  27972  addsfo  27991  peano2no  27992  negscl  28044  subsfo  28073  subsid1  28076  muls01  28120  mulsrid  28121  divs1  28212  recsex  28227  abssnid  28251  peano2ons  28288  noseqp1  28299  noseqind  28300  peano2nns  28358  n0fincut  28363  n0lts1e0  28376  dfnns2  28380  oldfib  28385  elzs2  28407  elnnzs  28409  elznns  28410  zsoring  28417  n0seo  28429  exps0  28435  exps1  28436  bdaypw2n0bndlem  28471  bdayfin  28495  istrkg2ld  28544  istrkg3ld  28545  ttgval  28959  brbtwn  28984  colinearalglem4  28994  upgr0eop  29199  uspgrushgr  29262  usgruspgr  29265  usgr0eop  29331  0grsubgr  29363  uspgrloopvtx  29601  umgr2v2evtx  29607  usgr0edg0rusgr  29661  rgrusgrprc  29675  wlkvtxiedg  29710  pthdivtx  29812  usgr2pthlem  29848  wlkswwlksf1o  29964  wwlksext2clwwlk  30144  konigsbergssiedgw  30337  frgrncvvdeqlem7  30392  2clwwlk2  30435  ex-po  30522  pliguhgr  30574  nvnd  30776  ipval2lem3  30793  ipval2  30795  ipidsq  30798  dipcj  30802  dip0r  30805  nmlnogt0  30885  blocni  30893  ipasslem2  30920  ipasslem8  30925  ipasslem9  30926  ajval  30949  ubthlem1  30958  hvaddlid  31111  hvsub0  31164  hi02  31185  hlimi  31276  isch2  31311  chlimi  31322  chsupunss  31432  shsupunss  31434  chlejb1i  31564  h1dei  31638  h1de2ci  31644  spanunsni  31667  pjoml2i  31673  pjorthi  31757  mayete3i  31816  hosubid1  31886  nmopge0  31999  nmfnge0  32015  adj1  32021  adjeq  32023  lnop0  32054  lnopmi  32088  nmophmi  32119  cnlnadjlem5  32159  cnlnadjeui  32165  unierri  32192  leoprf2  32215  leopnmid  32226  nmopleid  32227  hstles  32319  hst0  32321  strlem3a  32340  dmdbr2  32391  mdsl1i  32409  mdsl2i  32410  mdsl2bi  32411  cvmdi  32412  mdslmd1lem1  32413  mdslmd1lem2  32414  mdslmd1i  32417  mdslmd2i  32418  csmdsymi  32422  mdexchi  32423  superpos  32442  atomli  32470  atordi  32472  chirredlem1  32478  chirredlem2  32479  atcvat4i  32485  atabsi  32489  mdsymlem1  32491  mdsymlem5  32495  mdsymlem6  32496  sumdmdii  32503  dmdbr5ati  32510  dmdbr6ati  32511  mddmdin0i  32519  cdj3lem2  32523  unidifsnel  32622  unidifsnne  32623  xppreima  32735  abfmpunirn  32742  abfmpel  32745  aciunf1lem  32752  fgreu  32761  padct  32808  fpwrelmapffslem  32822  fpwrelmap  32823  xrge0infss  32851  xrdifh  32871  indconst0  32950  indconst1  32951  pfx1s2  33032  clatp0cl  33069  clatp1cl  33070  cntrcrng  33175  cycpmco2lem4  33223  rmfsupp2  33332  1fldgenq  33416  resvval  33422  rearchi  33439  qusxpid  33456  opprabs  33575  zringfrac  33647  psrbasfsupp  33705  rlmdim  33787  constrfiss  33929  2sqr3minply  33958  locfinreflem  34018  locfinref  34019  ordtconnlem1  34102  rge0scvg  34127  lmxrge0  34130  qqh0  34162  qqh1  34163  rrh0  34193  zrhre  34197  esumcst  34241  esumfzf  34247  esumfsupre  34249  hasheuni  34263  sgon  34302  dmvlsiga  34307  sigainb  34314  measval  34376  ismeas  34377  sxbrsigalem0  34449  omssubadd  34478  carsggect  34496  eulerpartlemmf  34553  eulerpartlemgs2  34558  eulerpartlemn  34559  rrvsum  34632  ballotlem2  34667  ballotlemfcc  34672  ballotlem4  34677  signsplypnf  34728  signsply0  34729  signsw0glem  34731  signswrid  34736  signlem0  34765  signshf  34766  bnj535  35066  bnj580  35089  bnj907  35143  bnj1253  35193  funen1cnv  35265  rankval4b  35277  fineqvnttrclse  35302  noinfepfnregs  35310  onvf1odlem1  35319  onvf1od  35323  loop1cycl  35353  ptpconn  35449  cvmsss2  35490  cvmlift2lem12  35530  cvmlift2lem13  35531  cvmliftphtlem  35533  cvmliftpht  35534  fmlafvel  35601  mppsthm  35795  bcneg1  35952  fv1stcnv  35993  fv2ndcnv  35994  wlimeq1  36034  imagesset  36169  altopeq1  36179  brcolinear2  36274  cldbnd  36542  ivthALT  36551  refssfne  36574  ontgval  36647  onint1  36665  axc11n11r  36928  bj-pm11.53a  37013  bj-bm1.3ii  37312  bj-restsn0  37338  bj-restsn10  37339  bj-restsnid  37340  bj-rest10  37341  bj-rest0  37346  bj-inftyexpiinv  37463  bj-inftyexpidisj  37465  taupilem1  37576  irrdiff  37581  f1omptsnlem  37591  mptsnunlem  37593  topdifinffinlem  37602  inunissunidif  37630  rdgssun  37633  exrecfnlem  37634  exrecfnpw  37636  finixpnum  37856  tan2h  37863  matunitlindflem2  37868  ptrest  37870  poimirlem22  37893  poimirlem25  37896  mblfinlem1  37908  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  ftc1anclem5  37948  ftc1anclem8  37951  dvasin  37955  dvacos  37956  sdclem2  37993  totbndbnd  38040  heibor1lem  38060  heiborlem7  38068  bfplem1  38073  prnc  38318  brxrn  38634  ecxrn2  38659  dfpeters2  39225  riotasv  39335  glbconN  39753  atpointN  40119  polsubN  40283  pol0N  40285  pol1N  40286  2polvalN  40290  2polssN  40291  3polN  40292  pcl0N  40298  2pmaplubN  40302  pnonsingN  40309  polsubclN  40328  cdlemefs32sn1aw  40790  cdleme43fsv1snlem  40796  cdleme41sn3a  40809  cdleme32a  40817  cdleme40m  40843  cdleme40n  40844  cdleme42b  40854  istendo  41136  cdlemk40  41293  cdlemkid  41312  dihvalcqpre  41611  facp2  42513  relt0neg1  42826  sn-nnne0  42830  frlmsnic  42910  prjspnerlem  42975  prjspnval2  42976  0prjspn  42986  3cubes  43047  mapfzcons1cl  43075  eldioph3b  43122  eldiophss  43131  0dioph  43135  vdioph  43136  eldioph4b  43168  eldioph4i  43169  rencldnfilem  43177  rmxy1  43279  rmxy0  43280  rmxm1  43291  rmym1  43292  monotoddzzfi  43299  wepwso  43400  aomclem6  43416  pwslnmlem0  43448  isnumbasabl  43463  areaquad  43573  onexlimgt  43600  oaabsb  43651  nadd1suc  43749  oe2  43762  safesnsupfidom1o  43773  onnoxp  43789  oa1cl  43803  finona1cl  43809  reabsifneg  43988  reabsifnneg  43991  relexp2  44033  eltrclrec  44036  elrtrclrec  44037  brtrclrec  44052  brrtrclrec  44053  relexpxpmin  44073  dftrcl3  44076  dfrtrcl3  44089  heeq1  44133  seff  44665  lhe4.4ex1a  44685  eelT0  45130  snssl  45185  sineq0ALT  45292  trfr  45318  xpwf  45320  dmwf  45321  rnwf  45322  modelaxreplem1  45334  modelaxreplem3  45336  0elaxnul  45339  prclaxpr  45341  uniclaxun  45342  wfac8prim  45358  permaxinf2lem  45368  elrnmpt1sf  45548  founiiun0  45549  supxrgere  45692  supxrgelem  45696  fmuldfeqlem1  45942  fmuldfeq  45943  climneg  45970  sumnnodd  45990  liminfltlem  46162  xlimpnfxnegmnf2  46216  addccncf2  46234  dvsinax  46271  stoweidlem18  46376  stoweidlem19  46377  stoweidlem22  46380  stoweidlem34  46392  stoweidlem40  46398  stoweidlem41  46399  stoweidlem55  46413  stoweidlem59  46417  dirker2re  46450  dirkerdenne0  46451  fourierdlem48  46512  fourierdlem49  46513  fourierdlem70  46534  fourierdlem71  46535  fourierdlem104  46568  fourierdlem112  46576  fouriersw  46589  etransclem46  46638  etransclem48  46640  nnfoctbdjlem  46813  ormklocald  47232  natlocalincr  47234  cjnpoly  47249  sinnpoly  47251  sqrtnegnre  47667  fsummmodsnunz  47735  flsqrt5  47954  bits0ALTV  48039  mogoldbblem  48080  sgoldbeven3prm  48143  nnsum3primes4  48148  isubgr0uhgr  48233  ushggricedg  48287  2zrngnmlid  48615  2zrngnmrid  48616  mpoexxg2  48698  lco0  48787  zlmodzxzldeplem3  48862  0dig1  48969  naryfvalel  48990  ackvalsuc0val  49047  iinxp  49190  0funclem  49445  aacllem  50160