Theorem 3ad2ant3 1158

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant3	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 469	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 1153	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simp3  1161  3anim123i  1183  simp3l  1251  simp3r  1252  simp31  1259  simp32  1260  simp33  1261  simp3ll  1318  simp3lr  1319  simp3rl  1320  simp3rr  1321  simp3l1  1370  simp3l2  1371  simp3l3  1372  simp3r1  1373  simp3r2  1374  simp3r3  1375  simp31l  1388  simp31r  1389  simp32l  1390  simp32r  1391  simp33l  1392  simp33r  1393  simp311  1412  simp312  1413  simp313  1414  simp321  1415  simp322  1416  simp323  1417  simp331  1418  simp332  1419  simp333  1420  3jaao  1550  ceqsalt  3422  ceqsralt  3423  disjtpsn  4442  disjtp2  4443  elpwdifsn  4511  ssprsseq  4546  tpssi  4557  prnebg  4576  prnesn  4581  prel12g  4586  snopeqop  5160  poltletr  5739  predeq123  5894  predpo  5911  fntpg  6156  funcnvpr  6158  funcnvtp  6159  f1resf1  6320  ftpg  6643  fsnunf  6672  fsnunfv  6674  fvpr1g  6679  fvpr2g  6680  fpropnf1  6744  weniso  6824  ovmpt3rab1  7117  epne3  7206  limsuc  7275  oteqimp  7413  el2xptp0  7440  funsssuppss  7552  smoel  7689  smoord  7694  omwordi  7884  oneo  7894  oeord  7901  oewordi  7904  nnmwordi  7948  nnneo  7964  uniinqs  8058  undifixp  8177  enfixsn  8304  domss2  8354  domssex2  8355  unxpdomlem3  8401  dif1en  8428  rneqdmfinf1o  8477  mapfien2  8549  dffi2  8564  unwdomg  8724  ixpiunwdom  8731  en3lplem1  8750  oemapvali  8824  updjud  9039  fodomfi2  9162  infcdaabs  9309  infunabs  9310  infdif  9312  ackbij1lem9  9331  ackbij1lem16  9338  coflim  9364  cfsmolem  9373  isfin2-2  9422  fin1a2lem9  9511  hsmexlem2  9530  axcc2lem  9539  axcc3  9541  domtriomlem  9545  axdc3lem4  9556  axcclem  9560  zornn0g  9608  axacndlem4  9713  axacndlem5  9714  axacnd  9715  gchdomtri  9732  fpwwe  9749  tskssel  9860  tskint  9888  tskurn  9892  gruurn  9901  gruixp  9912  grudomon  9920  gruina  9921  adderpqlem  10057  mulerpqlem  10058  addassnq  10061  mulassnq  10062  distrnq  10064  ltsonq  10072  ltanq  10074  ltmnq  10075  reclem3pr  10152  dedekind  10481  addid2  10500  addcan2  10502  divdir  10991  divcan5  11008  ltdiv1  11168  infrelb  11289  lt2halves  11530  zdivmul  11711  ledivge1le  12111  addlelt  12154  xaddass  12293  xleadd1  12299  xltadd1  12300  xmulasslem3  12330  xmulass  12331  xlemul1  12334  xlemul2  12335  xltmul1  12336  xadddir  12340  elioo5  12445  iccsupr  12481  iccneg  12510  icoshft  12511  icoshftf1o  12512  iccsplit  12524  zltaddlt1le  12543  fzen  12577  ssfzunsn  12606  elfz1b  12628  fzrevral  12644  fzshftral  12647  elfz0ubfz0  12663  elfz0fzfz0  12664  fz0fzelfz0  12665  fz0fzdiffz0  12668  elfzo  12692  elfzonlteqm1  12764  ltdifltdiv  12855  modabs  12923  modcyc  12925  modaddmulmod  12957  moddi  12958  modsubdir  12959  expdiv  13130  leexp2a  13135  bcval3  13309  hashnnn0genn0  13347  hashgadd  13380  hashunx  13389  hashfun  13437  hashres  13438  hashtpg  13480  fun2dmnop0  13489  hashdifsnp1  13491  ccatval1  13570  ccatval2  13571  ccatval3  13572  ccatsymb  13575  ccatass  13581  ccats1val2  13621  swrdval2  13639  swrd0len0  13656  swrd0fv  13659  swrdeq  13664  swrdspsleq  13669  2swrdeqwrdeq  13673  swrdswrdlem  13679  swrdswrd  13680  swrd0swrd  13681  ccats1swrdeq  13689  ccats1swrdeqrex  13698  swrdccatin12lem2  13709  swrdccat3b  13716  swrdccatid  13717  splval  13722  repswswrd  13751  cshwidxmod  13769  cshwidx0mod  13771  cshf1  13776  cshwleneq  13783  scshwfzeqfzo  13792  cshimadifsn  13795  cshimadifsn0  13796  ccatco  13801  cshco  13802  swrdco  13803  f1oun2prg  13882  swrds2  13905  eqwrds3  13925  trclfvss  13966  elicc4abs  14278  mulcn2  14545  fsumsplitsnun  14703  fsumsplitsnunOLD  14705  modfsummods  14743  prodfrec  14844  ntrivcvgfvn0  14848  binomrisefac  14989  demoivreALT  15147  rpnnen2lem4  15162  dvdsval2  15202  dvdsmodexp  15207  modmulconst  15232  dvdsexp  15268  oddge22np1  15289  modremain  15347  mulgcd  15480  mulgcdr  15482  gcddiv  15483  rpmulgcd  15490  rplpwr  15491  lcmfn0val  15551  lcmftp  15564  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  coprmdvds  15581  cncongr1  15595  dvdsnprmd  15617  prmexpb  15643  rpexp  15645  cncongrprm  15650  modprm0  15723  modprmn0modprm0  15725  coprimeprodsq  15726  pythagtriplem1  15734  pythagtriplem3  15736  pythagtriplem10  15738  pythagtriplem6  15739  pythagtriplem11  15743  pythagtriplem12  15744  pythagtriplem13  15745  pythagtriplem15  15747  pythagtriplem17  15749  pythagtriplem19  15751  pcdvdsb  15786  dvdsprmpweqle  15803  pcfaclem  15815  vdwapun  15891  ramval  15925  0ram2  15938  0ramcl  15940  fvprmselgcd1  15962  prmgaplem6  15973  setsstructOLD  16106  imasaddvallem  16390  imasvscaval  16399  mreiincl  16457  mremre  16465  mrieqv2d  16500  cofurid  16751  initoeu2lem0  16863  initoeu2lem2  16865  funcestrcsetclem6  16986  funcestrcsetclem9  16989  funcsetcestrclem6  17001  funcsetcestrclem9  17004  xpcpropd  17049  clatleglb  17327  ress0g  17520  gsumccat  17579  gsumccatsn  17581  sgrp2nmndlem3  17613  sgrp2nmndlem5  17617  dfgrp3lem  17714  mulgdirlem  17771  mulgp1  17773  mulgmodid  17779  eqglact  17843  fvcosymgeq  18046  gsmsymgreqlem2  18048  pmtrprfv3  18071  pmtr3ncomlem1  18090  mndodcongi  18159  oddvdsnn0  18160  odngen  18189  gexnnod  18200  lsmlub  18275  lsmass  18280  efgsval2  18343  efgsrel  18344  ghmplusg  18446  odadd1  18448  odadd2  18449  srg1zr  18727  dvrcan1  18889  dvrcan3  18890  irredrmul  18905  srngadd  19057  srngmul  19058  rmodislmodlem  19130  rmodislmod  19131  lmhmvsca  19248  reslmhm2  19256  pwssplit3  19264  lbspss  19285  lsmsp  19289  lspsneu  19326  lidldvgen  19460  assa2ass  19527  evlsval  19723  evlsval2  19724  psropprmul  19812  coe1add  19838  coe1addfv  19839  coe1subfv  19840  coe1tm  19847  coe1sclmul  19856  coe1sclmul2  19858  coe1fzgsumdlem  19875  lply1binom  19880  evl1gsumdlem  19924  zrhpsgninv  20134  zrhpsgnevpm  20140  zrhpsgnodpm  20141  psgndiflemB  20150  cssmre  20243  frlmup4  20346  islindf2  20359  lindsind2  20364  f1lindf  20367  lindsss  20369  f1linds  20370  lindsmm  20373  lbslcic  20386  mndvcl  20403  mndvass  20404  mhmvlin  20409  matecl  20437  matvscacell  20448  mamulid  20453  mamurid  20454  mattposm  20472  madetsumid  20474  matepmcl  20475  matepm2cl  20476  mat1dimbas  20485  mavmulsolcl  20564  mulmarep1el  20585  mulmarep1gsum1  20586  mulmarep1gsum2  20587  1marepvsma1  20596  m1detdiag  20610  mdetdiaglem  20611  mdetdiag  20612  mdetunilem7  20631  mdetunilem9  20633  mdetmul  20636  gsummatr01lem3  20671  gsummatr01lem4  20672  gsummatr01  20673  smadiadetglem2  20686  matinv  20691  slesolinv  20694  cramerimplem1  20697  cramerimplem1OLD  20698  cramerimp  20701  cramerlem1  20702  pmatcoe1fsupp  20715  mat2pmatbas  20740  decpmatmullem  20785  pmatcollpw3lem  20797  chpscmat  20856  iuncld  21059  clsss  21068  ntrcls0  21090  iscldtop  21109  neiss  21123  neips  21127  restcldi  21187  cnpnei  21278  cnconst2  21297  cnpresti  21302  sslm  21313  cnt0  21360  cnt1  21364  cnhaus  21368  cncmp  21405  cmpcld  21415  cnconn  21435  conncompss  21446  ssref  21525  elptr  21586  upxp  21636  qtoptop2  21712  ordthmeolem  21814  opnfbas  21855  isfil2  21869  fbasweak  21878  snfbas  21879  fgss  21886  fgcl  21891  fbasrn  21897  trnei  21905  cfinfil  21906  csdfil  21907  supfil  21908  filufint  21933  fin1aufil  21945  fmval  21956  fmf  21958  elfm  21960  elfm3  21963  imaelfm  21964  rnelfmlem  21965  rnelfm  21966  flimclslem  21997  flfneii  22005  cnpfcfi  22053  alexsubALT  22064  ptcmplem3  22067  ustref  22231  ustelimasn  22235  utop3cls  22264  ressusp  22278  cfiluexsm  22303  prdsxmetlem  22382  txmetcn  22562  nmmtri  22635  nmrtri  22637  unitnmn0  22681  nminvr  22682  nmotri  22752  nghmplusg  22753  isclmi  23085  isclmp  23105  ncvsi  23159  fmcfil  23278  srabn  23364  rrxmvallem  23395  itgconst  23795  dvn2bss  23903  deg1mul3  24085  deg1mul3le  24086  deg1tmle  24087  q1peqb  24124  r1pcl  24127  r1pdeglt  24128  r1pid  24129  dvdsq1p  24130  dvdsr1p  24131  ptolemy  24459  sincosq1eq  24475  logeq0im1  24534  logmul2  24572  logdiv2  24573  cxplt2  24654  logbchbase  24719  relogbreexp  24723  relogbexp  24728  pythag  24757  lgamgulmlem1  24965  bcmono  25212  efexple  25216  lgsdirnn0  25279  gausslemma2dlem1a  25300  gausslemma2dlem3  25303  2lgslem1a1  25324  2lgsoddprmlem1  25343  2lgsoddprmlem2  25344  selberglem3  25446  brbtwn2  25995  axcgrid  26006  ax5seglem1  26018  ax5seglem2  26019  ax5seg  26028  axpasch  26031  axlowdimlem16  26047  axcontlem7  26060  structiedg0val  26121  lpvtx  26173  incistruhgr  26184  upgredg2vtx  26247  upgredgpr  26248  edglnl  26249  ausgrumgri  26273  ausgrusgri  26274  usgredg2vtxeuALT  26325  ushgredgedg  26332  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  uspgr1v1eop  26353  usgr1v0edg  26361  uhgrissubgr  26379  egrsubgr  26381  0uhgrsubgr  26383  nbupgrres  26477  nb3grprlem1  26494  cplgr3v  26555  umgr2v2enb1  26646  finsumvtxdgeven  26672  vtxdgoddnumeven  26673  rusgrnumwrdl2  26706  rusgr1vtx  26708  isewlk  26722  ewlkinedg  26724  upgrewlkle2  26726  wlkvtxeledg  26743  wlkeq  26753  wlkl1loop  26758  wlk1walk  26759  uspgr2wlkeq  26766  uspgr2wlkeq2  26767  wlksoneq1eq2  26784  wlkonl1iedg  26785  wlkon2n0  26786  wlkres  26791  wlkp1lem8  26801  lfgriswlk  26809  lfgrwlknloop  26810  spthonpthon  26871  spthonepeq  26872  uhgrwkspth  26875  usgr2wlkspth  26879  usgr2pth  26884  wwlknp  26960  wwlknvtx  26962  wwlknlsw  26965  0enwwlksnge1  26987  wlknwwlksnbij  27015  wwlksnred  27025  wwlksnredwwlkn  27028  wwlksnextsur  27033  wlksnwwlknvbij  27041  wlksnwwlknvbijOLD  27042  wwlksnextproplem1  27043  wwlksnwwlksnon  27049  wspthsnwspthsnon  27050  umgr2adedgwlkonALT  27083  umgr2wlkon  27086  umgrwwlks2on  27094  elwspths2spth  27105  rusgr0edg  27111  rusgrnumwwlks  27112  clwlkclwwlkf1lem2  27144  clwlkclwwlkf1lem3  27145  clwlkclwwlkfolem  27146  clwwisshclwwslemlem  27152  clwwlkinwwlk  27185  loopclwwlkn1b  27187  clwwlkf  27192  clwwlkext2edg  27202  wwlksext2clwwlk  27203  clwlksfclwwlkOLD  27232  clwlksf1clwwlklem2OLD  27236  clwlksf1clwwlklemOLD  27238  clwlknf1oclwwlkn  27244  clwwlknon1  27261  clwwlknonwwlknonbOLD  27271  clwwlknonex2lem2  27273  clwwlknonex2  27274  clwwlknun  27277  clwwlkvbij  27278  clwwlkvbijOLDOLD  27279  clwwlkvbijOLD  27280  clwwlknunOLD  27282  1ewlk  27284  0clwlkv  27300  1pthon2v  27322  3wlkdlem9  27337  uhgr3cyclex  27351  umgr3cyclex  27352  upgr4cycl4dv4e  27354  upgreupthseg  27378  eupth2lem3lem6  27402  eulercrct  27411  nfrgr2v  27443  frgr3vlem1  27444  3vfriswmgr  27449  extwwlkfablem1OLD  27513  numclwwlk2lem1lem  27514  numclwwlk1lem2foalem  27526  numclwwlk1lem2foa  27529  numclwwlk1lem2f1  27532  numclwwlk1lem2fo  27533  numclwwlk1  27537  clwwlknonclwlknonf1o  27538  dlwwlknonclwlknonf1olem1  27540  dlwwlknondlwlknonf1o  27541  wlkl0  27543  clwlknon2num  27544  numclwwlk2lem1  27552  numclwlk2lem2f  27553  numclwlk2lem2f1o  27555  numclwwlk2  27557  numclwwlk2lem1OLD  27559  numclwlk2lem2fOLD  27560  numclwlk2lem2f1oOLD  27562  numclwwlk2OLD  27564  numclwwlk3  27569  numclwwlk5lem  27571  numclwwlk6  27574  frgrreggt1  27577  frgrreg  27578  frgrregord013  27579  vcidOLD  27743  vcdi  27744  vcdir  27745  vcass  27746  imsmetlem  27869  0oval  27967  ajval  28041  shlub  28597  hmopco  29206  adjlnop  29269  mdslmd4i  29516  fcoinvbr  29740  fresf1o  29756  divnumden2  29887  ressnm  29972  ress1r  30110  smatfval  30182  pstmfval  30260  pl1cn  30322  ind1  30400  ind0  30401  sigaclcuni  30502  sigagenss2  30534  measun  30595  measvuni  30598  dya2iocnrect  30664  omsmeas  30706  ballotlemieq  30899  ballotlemrv1  30903  sgn3da  30924  bnj837  31149  bnj517  31273  bnj553  31286  bnj594  31300  bnj967  31333  bnj1097  31367  bnj1110  31368  bnj1118  31370  bnj1128  31376  bnj1125  31378  bnj1145  31379  bnj1136  31383  bnj1173  31388  bnj1189  31395  bnj1204  31398  bnj1279  31404  bnj1321  31413  bnj1413  31421  erdszelem2  31492  cnpconn  31530  cvmscld  31573  mrsubcv  31725  mrsubvr  31726  iprodefisumlem  31943  dvdspw  31953  dfon2lem3  32005  dfon2lem7  32009  nosupfv  32168  nosupres  32169  noetalem1  32179  btwndiff  32450  brcolinear2  32481  btwnconn1  32524  nn0prpwlem  32633  hmeoclda  32644  hmeocldb  32645  ivthALT  32646  fnemeet1  32677  fnejoin1  32679  nnssi3  32767  nndivsub  32768  bj-ceqsalt1  33177  bj-evalidval  33337  onsucuni3  33526  curfv  33697  lindsdom  33711  lindsenlbs  33712  ftc1anclem4  33795  areacirclem2  33808  areacirclem5  33811  areacirc  33812  upixp  33831  filbcmb  33842  cnresima  33869  smprngopr  34157  igenval2  34171  brxrn  34444  xrnresex  34472  lsmsat  34783  lsmsatcv  34785  lsatcvatlem  34824  islshpcv  34828  l1cvpat  34829  lfli  34836  lshpset2N  34894  cvrnbtwn  35046  meetat2  35072  atcmp  35086  atcvreq0  35089  atlatmstc  35094  cvlcvr1  35114  cvlcvrp  35115  cvlatcvr2  35117  cvr2N  35186  cvratlem  35196  2atjm  35220  athgt  35231  2lplnmN  35334  2llnmj  35335  2lplnmj  35397  dalemswapyzps  35465  dalem23  35471  dalem24  35472  dalem25  35473  dalem27  35474  dalem28  35475  dalem38  35485  dalem39  35486  dalem44  35491  dalem45  35492  dalem51  35498  dalem52  35499  dalem56  35503  pmapglbx  35544  pmapjat1  35628  pmapjat2  35629  paddatclN  35724  osumcllem4N  35734  osumcllem7N  35737  ltrncoval  35920  cdleme0aa  35985  cdleme0b  35987  cdleme8  36025  cdlemesner  36071  cdleme22eALTN  36120  cdleme26eALTN  36136  cdleme35h  36231  cdleme50trn2  36326  cdleme  36335  tgrpov  36523  tendotp  36536  tendoidcl  36544  tendo0co2  36563  cdlemkvcl  36617  dvhopvadd  36868  dvhopellsm  36892  dihmeetlem1N  37065  dihmeetlem9N  37090  dihatexv  37113  lcfl7lem  37274  mapdrvallem2  37420  mapdh9a  37564  hdmapevec  37610  ismrcd1  37757  istopclsd  37759  ismrc  37760  mapfzcons  37775  eldioph2  37821  diophrex  37835  diophren  37873  pellexlem1  37889  pellexlem5  37893  pellqrexplicit  37937  reglogmul  37953  reglogexp  37954  rmxycomplete  37977  congmul  38029  congabseq  38036  acongsym  38038  acongneg2  38039  fzneg  38044  acongeq  38045  jm2.19  38055  jm2.22  38057  jm2.23  38058  jm2.20nn  38059  rmydioph  38076  rmxdiophlem  38077  jm3.1  38082  pwssplit4  38154  hbtlem2  38189  idomrootle  38268  pwinfi2  38361  relexpaddss  38504  trclimalb2  38512  brtrclfv2  38513  trclfvdecomr  38514  ntrclsneine0lem  38856  ntrclsk2  38860  ntrclsk3  38862  ntrclsk13  38863  ntrclsk4  38864  gneispace  38926  dvconstbi  39027  expgrowth  39028  chordthmALT  39657  restuni3  39787  wessf1ornlem  39854  disjf1o  39861  elrnmpt2id  39906  funimassd  39909  infnsuprnmpt  39942  infrnmptle  40123  fmul01lt1lem1  40290  climsuselem1  40313  climsuse  40314  limcperiod  40334  lptre2pt  40346  limclner  40357  climbddf  40393  limsupvaluz2  40444  supcnvlimsup  40446  cncfshift  40561  cncfperiod  40566  icccncfext  40574  dvnmptconst  40630  dvnprodlem1  40635  dvnprodlem2  40636  iblspltprt  40662  itgspltprt  40668  stoweidlem3  40693  stoweidlem16  40706  stoweidlem17  40707  stoweidlem26  40716  stoweidlem34  40724  stoweidlem57  40747  fourierdlem41  40838  fourierdlem42  40839  fourierdlem52  40848  fourierdlem54  40850  fourierdlem74  40870  fourierdlem75  40871  fourierdlem80  40876  fourierdlem94  40890  fourierdlem102  40898  fourierdlem114  40910  etransclem18  40942  etransclem29  40953  etransclem46  40970  rrxtopnfi  40979  subsaliuncl  41049  sge0f1o  41072  sge0xp  41119  meadjiunlem  41155  voliunsge0lem  41162  volmea  41164  carageniuncllem1  41211  caratheodorylem1  41216  caratheodory  41218  isomenndlem  41220  hoicvr  41238  ovnsubaddlem2  41261  hoidmvlelem1  41285  hoidmvlelem2  41286  hoidmvlelem3  41287  hspmbllem2  41317  smfaddlem1  41447  smfco  41485  smfsuplem1  41493  f1oresf1o2  41875  2leaddle2  41882  ssfz12  41893  fsumsplitsndif  41912  fsummmodsndifre  41913  fsummmodsnunz  41914  iccpartiltu  41927  icceuelpart  41941  pfxnd  41964  pfxlen0  41965  pfxfv  41968  pfxeq  41973  pfxsuffeqwrdeq  41975  pfxpfx  41984  ccats1pfxeq  41990  ccats1pfxeqrex  41991  pfxccatin12lem2  41993  pfxccatpfx1  41996  pfxccatid  41999  repswpfx  42005  goldbachth  42028  prmdvdsfmtnof1lem1  42065  pwdif  42070  lighneallem1  42091  lighneallem2  42092  lighneallem4a  42094  lighneallem4  42096  lighneal  42097  oexpnegALTV  42157  oexpnegnz  42158  even3prm2  42197  gbepos  42215  gbegt5  42218  gboge9  42221  sbgoldbwt  42234  nnsum3primesgbe  42249  nnsum4primeseven  42257  nnsum4primesevenALTV  42258  bgoldbtbndlem1  42262  bgoldbtbndlem2  42263  bgoldbtbndlem3  42264  tgblthelfgott  42272  sprsymrelfolem2  42305  rngdir  42444  c0snmhm  42477  rngccatidALTV  42551  funcringcsetcALTV2lem6  42603  funcringcsetcALTV2lem9  42606  ringccatidALTV  42614  funcringcsetclem6ALTV  42626  ofaddmndmap  42684  mapprop  42686  nn0sumltlt  42690  gsumpr  42701  domnmsuppn0  42712  scmsuppss  42715  mndpsuppfi  42718  gsumlsscl  42726  ply1ass23l  42732  ply1mulgsumlem1  42736  lincfsuppcl  42764  linccl  42765  lincvalsng  42767  lincvalpr  42769  lincdifsn  42775  ellcoellss  42786  lincext1  42805  lincext2  42806  lincext3  42807  lindslinindimp2lem2  42810  ldepspr  42824  lincresunit3lem1  42830  lincresunit3lem2  42831  islindeps2  42834  logcxp0  42891  elbigo2r  42909  elbigolo1  42913  fllog2  42924  nnolog2flm1  42946  digvalnn0  42955  nn0digval  42956  dignn0fr  42957  dignn0ldlem  42958  dignnld  42959  digexp  42963  dignn0flhalflem1  42971  dignn0flhalflem2  42972  dignn0ehalf  42973  dignn0flhalf  42974  amgmwlem  43113