Theorem 3ad2ant3 1131

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 484	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 1126	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp3  1134  3anim123i  1147  simp3l  1197  simp3r  1198  simp31  1205  simp32  1206  simp33  1207  simp3ll  1240  simp3lr  1241  simp3rl  1242  simp3rr  1243  simp3l1  1274  simp3l2  1275  simp3l3  1276  simp3r1  1277  simp3r2  1278  simp3r3  1279  simp31l  1292  simp31r  1293  simp32l  1294  simp32r  1295  simp33l  1296  simp33r  1297  simp311  1316  simp312  1317  simp313  1318  simp321  1319  simp322  1320  simp323  1321  simp331  1322  simp332  1323  simp333  1324  3jaao  1429  ceqsalt  3527  ceqsralt  3528  disjtpsn  4651  disjtp2  4652  elpwdifsn  4721  ssprsseq  4758  tpssi  4769  prnebg  4786  prnesn  4790  prel12g  4794  snopeqop  5396  poltletr  5992  relcnvtrg  6119  predeq123  6149  predpo  6166  fntpg  6414  funcnvpr  6416  funcnvtp  6417  f1resf1  6583  ftpg  6918  fsnunf  6947  fsnunfv  6949  fvpr1g  6954  fvpr2g  6955  fpropnf1  7025  nf1const  7059  weniso  7107  ovmpt3rab1  7403  epne3  7495  limsuc  7564  oteqimp  7708  el2xptp0  7736  funeldmdif  7747  offsplitfpar  7815  funsssuppss  7856  smoel  7997  smoord  8002  omwordi  8197  oneo  8207  oeord  8214  oewordi  8217  nnmwordi  8261  nnneo  8278  uniinqs  8377  undifixp  8498  enfixsn  8626  domss2  8676  domssex2  8677  unxpdomlem3  8724  dif1en  8751  rneqdmfinf1o  8800  mapfien2  8872  dffi2  8887  unwdomg  9048  ixpiunwdom  9055  en3lplem1  9075  oemapvali  9147  updjud  9363  fodomfi2  9486  infdjuabs  9628  infunabs  9629  infdif  9631  ackbij1lem9  9650  ackbij1lem16  9657  coflim  9683  cfsmolem  9692  isfin2-2  9741  fin1a2lem9  9830  hsmexlem2  9849  axcc2lem  9858  axcc3  9860  domtriomlem  9864  axdc3lem4  9875  axcclem  9879  zornn0g  9927  axacndlem4  10032  axacndlem5  10033  axacnd  10034  gchdomtri  10051  fpwwe  10068  tskssel  10179  tskint  10207  tskurn  10211  gruurn  10220  gruixp  10231  grudomon  10239  gruina  10240  adderpqlem  10376  mulerpqlem  10377  addassnq  10380  mulassnq  10381  distrnq  10383  ltsonq  10391  ltanq  10393  ltmnq  10394  reclem3pr  10471  dedekind  10803  addid2  10823  addcan2  10825  divdir  11323  divcan5  11342  ltdiv1  11504  infrelb  11626  lt2halves  11873  zdivmul  12055  ledivge1le  12461  addlelt  12504  xaddass  12643  xleadd1  12649  xltadd1  12650  xmulasslem3  12680  xmulass  12681  xlemul1  12684  xlemul2  12685  xltmul1  12686  xadddir  12690  elioo5  12795  iccsupr  12831  iccneg  12859  icoshft  12860  icoshftf1o  12861  iccsplit  12872  zltaddlt1le  12891  fzen  12925  ssfzunsn  12954  elfz1b  12977  fzrevral  12993  fzshftral  12996  elfz0ubfz0  13012  elfz0fzfz0  13013  fz0fzelfz0  13014  fz0fzdiffz0  13017  elfzo  13041  elfzonlteqm1  13114  ltdifltdiv  13205  modabs  13273  modcyc  13275  modaddmulmod  13307  moddi  13308  modsubdir  13309  expdiv  13481  leexp2a  13537  expnngt1  13603  bcval3  13667  hashnnn0genn0  13704  hashgadd  13739  hashunx  13748  hashfun  13799  hashres  13800  hashtpg  13844  fun2dmnop0  13853  hashdifsnp1  13855  ccatval1  13930  ccatval1OLD  13931  ccatval2  13932  ccatval3  13933  ccatass  13942  ccats1val2  13983  swrdval2  14008  swrdnnn0nd  14018  pfxfv  14044  pfxnd  14049  pfxsuffeqwrdeq  14060  swrdswrdlem  14066  swrdswrd  14067  pfxswrd  14068  pfxpfx  14070  ccats1pfxeq  14076  ccats1pfxeqrex  14077  pfxccatin12lem2  14093  pfxccatpfx1  14098  swrdccat3b  14102  pfxccatid  14103  splval  14113  repswswrd  14146  repswpfx  14147  cshwidxmod  14165  cshwidx0mod  14167  cshf1  14172  cshwleneq  14179  scshwfzeqfzo  14188  cshimadifsn  14191  cshimadifsn0  14192  ccatco  14197  cshco  14198  swrdco  14199  f1oun2prg  14279  swrds2  14302  eqwrds3  14325  trclfvss  14366  elicc4abs  14679  mulcn2  14952  fsumsplitsnun  15110  modfsummods  15148  pwdif  15223  prodfrec  15251  ntrivcvgfvn0  15255  binomrisefac  15396  demoivreALT  15554  rpnnen2lem4  15570  dvdsval2  15610  dvdsmodexp  15615  modmulconst  15641  dvdsexp  15677  oddge22np1  15698  modremain  15759  mulgcd  15896  mulgcdr  15898  gcddiv  15899  rpmulgcd  15906  rplpwr  15907  lcmfn0val  15967  lcmftp  15980  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  coprmdvds  15997  cncongr1  16011  dvdsnprmd  16034  prmexpb  16062  rpexp  16064  cncongrprm  16069  modprm0  16142  modprmn0modprm0  16144  coprimeprodsq  16145  pythagtriplem1  16153  pythagtriplem3  16155  pythagtriplem10  16157  pythagtriplem6  16158  pythagtriplem11  16162  pythagtriplem12  16163  pythagtriplem13  16164  pythagtriplem15  16166  pythagtriplem17  16168  pythagtriplem19  16170  pcdvdsb  16205  dvdsprmpweqle  16222  pcfaclem  16234  vdwapun  16310  ramval  16344  0ram2  16357  0ramcl  16359  fvprmselgcd1  16381  prmgaplem6  16392  imasaddvallem  16802  imasvscaval  16811  fvprif  16834  mreiincl  16867  mremre  16875  mrieqv2d  16910  cofurid  17161  initoeu2lem0  17273  initoeu2lem2  17275  funcestrcsetclem6  17395  funcestrcsetclem9  17398  funcsetcestrclem6  17410  funcsetcestrclem9  17413  xpcpropd  17458  clatleglb  17736  mgmsscl  17857  ress0g  17939  insubm  17983  gsumccatOLD  18005  gsumccat  18006  gsumccatsn  18008  idresefmnd  18064  sgrp2nmndlem3  18090  sgrp2nmndlem5  18094  dfgrp3lem  18197  mulgdirlem  18258  mulgp1  18260  mulgmodid  18266  eqglact  18331  fvcosymgeq  18557  gsmsymgreqlem2  18559  pmtrprfv3  18582  pmtr3ncomlem1  18601  mndodcongi  18671  oddvdsnn0  18672  odngen  18702  gexnnod  18713  lsmlub  18790  lsmass  18795  efgsrel  18860  ghmplusg  18966  odadd1  18968  odadd2  18969  gsumpr  19075  srg1zr  19279  dvrcan1  19441  dvrcan3  19442  irredrmul  19457  srngadd  19628  srngmul  19629  rmodislmodlem  19701  rmodislmod  19702  lmhmvsca  19817  reslmhm2  19825  pwssplit3  19833  lbspss  19854  lsmsp  19858  lspsneu  19895  lidldvgen  20028  assa2ass  20095  ascldimul  20116  evlsval  20299  evlsval2  20300  psropprmul  20406  coe1add  20432  coe1addfv  20433  coe1subfv  20434  coe1tm  20441  coe1sclmul  20450  coe1sclmul2  20452  coe1fzgsumdlem  20469  lply1binom  20474  evl1gsumdlem  20519  zrhpsgninv  20729  zrhpsgnevpm  20735  zrhpsgnodpm  20736  psgndiflemB  20744  phlssphl  20803  cssmre  20837  frlmup4  20945  islindf2  20958  lindsind2  20963  f1lindf  20966  lindsss  20968  f1linds  20969  lindsmm  20972  lbslcic  20985  mndvcl  21002  mndvass  21003  mhmvlin  21008  matecl  21034  matvscacell  21045  mamulid  21050  mamurid  21051  mattposm  21068  madetsumid  21070  matepmcl  21071  matepm2cl  21072  mat1dimbas  21081  mavmulsolcl  21160  mulmarep1el  21181  mulmarep1gsum1  21182  mulmarep1gsum2  21183  1marepvsma1  21192  m1detdiag  21206  mdetdiaglem  21207  mdetdiag  21208  mdetunilem7  21227  mdetunilem9  21229  mdetmul  21232  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  smadiadetglem2  21281  matinv  21286  slesolinv  21289  cramerimplem1  21292  cramerimp  21295  cramerlem1  21296  pmatcoe1fsupp  21309  mat2pmatbas  21334  decpmatmullem  21379  pmatcollpw3lem  21391  chpscmat  21450  iuncld  21653  clsss  21662  ntrcls0  21684  iscldtop  21703  neiss  21717  neips  21721  restcldi  21781  cnpnei  21872  cnconst2  21891  cnpresti  21896  sslm  21907  cnt0  21954  cnt1  21958  cnhaus  21962  cncmp  22000  cmpcld  22010  cnconn  22030  conncompss  22041  ssref  22120  elptr  22181  upxp  22231  qtoptop2  22307  ordthmeolem  22409  opnfbas  22450  isfil2  22464  fbasweak  22473  snfbas  22474  fgss  22481  fgcl  22486  fbasrn  22492  trnei  22500  cfinfil  22501  csdfil  22502  supfil  22503  filufint  22528  fin1aufil  22540  fmval  22551  fmf  22553  elfm  22555  elfm3  22558  imaelfm  22559  rnelfmlem  22560  rnelfm  22561  flimclslem  22592  flfneii  22600  cnpfcfi  22648  alexsubALT  22659  ptcmplem3  22662  ustref  22827  ustelimasn  22831  utop3cls  22860  ressusp  22874  cfiluexsm  22899  prdsxmetlem  22978  txmetcn  23158  nmmtri  23231  nmrtri  23233  unitnmn0  23277  nminvr  23278  nmotri  23348  nghmplusg  23349  isclmi  23681  isclmp  23701  ncvsi  23755  fmcfil  23875  srabn  23963  cssbn  23978  rrxmvallem  24007  ehleudisval  24022  itgconst  24419  dvn2bss  24527  deg1mul3  24709  deg1mul3le  24710  deg1tmle  24711  q1peqb  24748  r1pcl  24751  r1pdeglt  24752  r1pid  24753  dvdsq1p  24754  dvdsr1p  24755  ptolemy  25082  sincosq1eq  25098  logeq0im1  25161  logmul2  25199  logdiv2  25200  cxplt2  25281  logbchbase  25349  relogbreexp  25353  relogbexp  25358  pythag  25395  lgamgulmlem1  25606  bcmono  25853  efexple  25857  lgsdirnn0  25920  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  2lgslem1a1  25965  2lgsoddprmlem1  25984  2lgsoddprmlem2  25985  2sqreulem2  26028  selberglem3  26123  brbtwn2  26691  axcgrid  26702  ax5seglem1  26714  ax5seglem2  26715  ax5seg  26724  axpasch  26727  axlowdimlem16  26743  axcontlem7  26756  elntg2  26771  structiedg0val  26807  lpvtx  26853  incistruhgr  26864  upgredg2vtx  26926  upgredgpr  26927  edglnl  26928  ausgrumgri  26952  ausgrusgri  26953  usgredg2vtxeuALT  27004  ushgredgedg  27011  ushgredgedgloop  27013  uspgr1v1eop  27031  usgr1v0edg  27039  uhgrissubgr  27057  egrsubgr  27059  0uhgrsubgr  27061  nbupgrres  27146  nb3grprlem1  27162  cplgr3v  27217  umgr2v2enb1  27308  finsumvtxdgeven  27334  vtxdgoddnumeven  27335  rusgrnumwrdl2  27368  rusgr1vtx  27370  isewlk  27384  ewlkinedg  27386  upgrewlkle2  27388  wlkvtxeledg  27405  wlkeq  27415  wlkl1loop  27419  wlk1walk  27420  uspgr2wlkeq  27427  uspgr2wlkeq2  27428  wlksoneq1eq2  27446  wlkonl1iedg  27447  wlkon2n0  27448  wlkres  27452  wlkp1lem8  27462  lfgriswlk  27470  lfgrwlknloop  27471  spthonpthon  27532  spthonepeq  27533  uhgrwkspth  27536  usgr2wlkspth  27540  usgr2pth  27545  wwlknp  27621  wwlknvtx  27623  wwlknlsw  27625  0enwwlksnge1  27642  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnredwwlkn  27673  wwlksnextsurj  27678  wlksnwwlknvbij  27687  wwlksnextproplem1  27688  wwlksnwwlksnon  27694  wspthsnwspthsnon  27695  umgr2adedgwlkonALT  27726  umgr2wlkon  27729  umgrwwlks2on  27736  elwspths2spth  27746  rusgr0edg  27752  rusgrnumwwlks  27753  clwlkclwwlkf1lem2  27783  clwlkclwwlkf1lem3  27784  clwlkclwwlkfolem  27785  clwwisshclwwslemlem  27791  clwwlkinwwlk  27818  loopclwwlkn1b  27820  clwwlkf  27826  clwwlkext2edg  27835  wwlksext2clwwlk  27836  clwlknf1oclwwlkn  27863  clwwlknon1  27876  clwwlknonex2lem2  27887  clwwlknonex2  27888  clwwlknun  27891  clwwlkvbij  27892  1ewlk  27894  0clwlkv  27910  1pthon2v  27932  3wlkdlem9  27947  uhgr3cyclex  27961  umgr3cyclex  27962  upgr4cycl4dv4e  27964  upgreupthseg  27988  eupth2lem3lem6  28012  eulercrct  28021  nfrgr2v  28051  frgr3vlem1  28052  3vfriswmgr  28057  numclwwlk2lem1lem  28121  numclwwlk1lem2foalem  28130  numclwwlk1lem2foa  28133  numclwwlk1lem2f1  28136  numclwwlk1lem2fo  28137  numclwwlk1  28140  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1olem1  28143  dlwwlknondlwlknonf1o  28144  wlkl0  28146  clwlknon2num  28147  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  numclwwlk2  28160  numclwwlk3  28164  numclwwlk5lem  28166  numclwwlk6  28169  frgrreggt1  28172  frgrreg  28173  frgrregord013  28174  vcidOLD  28341  vcdi  28342  vcdir  28343  vcass  28344  imsmetlem  28467  0oval  28565  ajval  28638  shlub  29191  hmopco  29800  adjlnop  29863  mdslmd4i  30110  fcoinvbr  30358  fresf1o  30376  divnumden2  30534  swrdrn2  30628  swrdrn3  30629  cshwrnid  30635  ressnm  30638  ress1r  30860  qusscaval  30921  sralvec  30990  smatfval  31060  pstmfval  31136  pl1cn  31198  ind1  31276  ind0  31277  sigaclcuni  31377  sigagenss2  31409  measun  31470  measvuni  31473  dya2iocnrect  31539  omsmeas  31581  ballotlemieq  31774  ballotlemrv1  31778  sgn3da  31799  signstfvp  31841  bnj837  32032  bnj517  32157  bnj553  32170  bnj594  32184  bnj967  32217  bnj1097  32253  bnj1110  32254  bnj1118  32256  bnj1128  32262  bnj1125  32264  bnj1145  32265  bnj1136  32269  bnj1173  32274  bnj1189  32281  bnj1204  32284  bnj1279  32290  bnj1321  32299  bnj1413  32307  revpfxsfxrev  32362  swrdwlk  32373  loop1cycl  32384  2cycld  32385  umgr2cycllem  32387  erdszelem2  32439  cnpconn  32477  cvmscld  32520  satfsucom  32601  satfvsucom  32604  satfvsuc  32608  satfvsucsuc  32612  satfbrsuc  32613  satf0suclem  32622  sat1el2xp  32626  satfdmfmla  32647  satfv0fvfmla0  32660  ex-sategoelel  32668  satefvfmla1  32672  prv1n  32678  mrsubcv  32757  mrsubvr  32758  iprodefisumlem  32972  dvdspw  32982  dfon2lem3  33030  dfon2lem7  33034  nosupfv  33206  nosupres  33207  noetalem1  33217  btwndiff  33488  brcolinear2  33519  btwnconn1  33562  nn0prpwlem  33670  hmeoclda  33681  hmeocldb  33682  ivthALT  33683  fnemeet1  33714  fnejoin1  33716  nnssi3  33804  nndivsub  33805  bj-ceqsalt1  34204  bj-evalidval  34372  onsucuni3  34651  nlpineqsn  34692  curfv  34887  lindsadd  34900  lindsdom  34901  lindsenlbs  34902  ftc1anclem4  34985  areacirclem2  34998  areacirclem5  35001  areacirc  35002  upixp  35019  filbcmb  35030  cnresima  35057  smprngopr  35345  igenval2  35359  brxrn  35641  xrnresex  35669  lsmsat  36159  lsmsatcv  36161  lsatcvatlem  36200  islshpcv  36204  l1cvpat  36205  lfli  36212  lshpset2N  36270  cvrnbtwn  36422  meetat2  36448  atcmp  36462  atcvreq0  36465  atlatmstc  36470  cvlcvr1  36490  cvlcvrp  36491  cvlatcvr2  36493  cvr2N  36562  cvratlem  36572  2atjm  36596  athgt  36607  2lplnmN  36710  2llnmj  36711  2lplnmj  36773  dalemswapyzps  36841  dalem23  36847  dalem24  36848  dalem25  36849  dalem27  36850  dalem28  36851  dalem38  36861  dalem39  36862  dalem44  36867  dalem45  36868  dalem51  36874  dalem52  36875  dalem56  36879  pmapglbx  36920  pmapjat1  37004  pmapjat2  37005  paddatclN  37100  osumcllem4N  37110  osumcllem7N  37113  ltrncoval  37296  cdleme0aa  37361  cdleme0b  37363  cdleme8  37401  cdlemesner  37447  cdleme22eALTN  37496  cdleme26eALTN  37512  cdleme35h  37607  cdleme50trn2  37702  cdleme  37711  tgrpov  37899  tendotp  37912  tendoidcl  37920  tendo0co2  37939  cdlemkvcl  37993  dvhopvadd  38244  dvhopellsm  38268  dihmeetlem1N  38441  dihmeetlem9N  38466  dihatexv  38489  lcfl7lem  38650  mapdrvallem2  38796  mapdh9a  38940  hdmapevec  38986  nn0rppwr  39231  nn0expgcd  39233  zrtelqelz  39241  zrtdvds  39242  remulcand  39299  prjspvs  39309  ismrcd1  39344  istopclsd  39346  ismrc  39347  mapfzcons  39362  eldioph2  39408  diophrex  39421  diophren  39459  pellexlem1  39475  pellexlem5  39479  pellqrexplicit  39523  reglogmul  39539  reglogexp  39540  rmxycomplete  39563  congmul  39613  congabseq  39620  acongsym  39622  acongneg2  39623  fzneg  39628  acongeq  39629  jm2.19  39639  jm2.22  39641  jm2.23  39642  jm2.20nn  39643  rmydioph  39660  rmxdiophlem  39661  jm3.1  39666  pwssplit4  39738  hbtlem2  39773  idomrootle  39844  pr2eldif1  39962  pr2eldif2  39963  pwinfi2  39970  relexpaddss  40112  trclimalb2  40120  brtrclfv2  40121  trclfvdecomr  40122  ntrclsneine0lem  40463  ntrclsk2  40467  ntrclsk3  40469  ntrclsk13  40470  ntrclsk4  40471  gneispace  40533  dvconstbi  40715  expgrowth  40716  chordthmALT  41316  restuni3  41433  wessf1ornlem  41494  disjf1o  41501  elrnmpoid  41543  funimassd  41546  infnsuprnmpt  41571  infrnmptle  41746  fmul01lt1lem1  41914  climsuselem1  41937  climsuse  41938  limcperiod  41958  lptre2pt  41970  limclner  41981  climbddf  42017  limsupvaluz2  42068  supcnvlimsup  42070  xlimliminflimsup  42192  cncfshift  42206  cncfperiod  42211  icccncfext  42219  dvnmptconst  42275  dvnprodlem1  42280  dvnprodlem2  42281  iblspltprt  42307  itgspltprt  42313  stoweidlem3  42337  stoweidlem16  42350  stoweidlem17  42351  stoweidlem26  42360  stoweidlem34  42368  stoweidlem57  42391  fourierdlem41  42482  fourierdlem42  42483  fourierdlem52  42492  fourierdlem54  42494  fourierdlem74  42514  fourierdlem75  42515  fourierdlem80  42520  fourierdlem94  42534  fourierdlem102  42542  fourierdlem114  42554  etransclem18  42586  etransclem29  42597  etransclem46  42614  rrxtopnfi  42621  subsaliuncl  42690  sge0f1o  42713  sge0xp  42760  meadjiunlem  42796  voliunsge0lem  42803  volmea  42805  carageniuncllem1  42852  caratheodorylem1  42857  caratheodory  42859  isomenndlem  42861  hoicvr  42879  ovnsubaddlem2  42902  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hspmbllem2  42958  smfaddlem1  43088  smfco  43126  smfsuplem1  43134  f1oresf1o2  43539  2leaddle2  43547  ssfz12  43563  fsumsplitsndif  43582  fsummmodsndifre  43583  fsummmodsnunz  43584  preimafvelsetpreimafv  43597  imaelsetpreimafv  43604  fundcmpsurbijinjpreimafv  43616  iccpartiltu  43631  icceuelpart  43645  ich2exprop  43682  ichnreuop  43683  sprsymrelfolem2  43704  goldbachth  43758  prmdvdsfmtnof1lem1  43795  lighneallem1  43819  lighneallem2  43820  lighneallem4a  43822  lighneallem4  43824  lighneal  43825  oexpnegALTV  43891  oexpnegnz  43892  even3prm2  43933  gbepos  43972  gbegt5  43975  gboge9  43978  sbgoldbwt  43991  nnsum3primesgbe  44006  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  tgblthelfgott  44029  isomgrsym  44050  rngdir  44202  c0snmhm  44235  rngccatidALTV  44309  funcringcsetcALTV2lem6  44361  funcringcsetcALTV2lem9  44364  ringccatidALTV  44372  funcringcsetclem6ALTV  44384  ofaddmndmap  44441  mapprop  44443  nn0sumltlt  44447  domnmsuppn0  44466  scmsuppss  44469  mndpsuppfi  44472  gsumlsscl  44480  ply1ass23l  44485  ply1mulgsumlem1  44489  lincfsuppcl  44517  linccl  44518  lincvalsng  44520  lincvalpr  44522  lincdifsn  44528  ellcoellss  44539  lincext1  44558  lincext2  44559  lincext3  44560  lindslinindimp2lem2  44563  ldepspr  44577  lincresunit3lem1  44583  lincresunit3lem2  44584  islindeps2  44587  logcxp0  44644  elbigo2r  44662  elbigolo1  44666  fllog2  44677  nnolog2flm1  44699  digvalnn0  44708  nn0digval  44709  dignn0fr  44710  dignn0ldlem  44711  dignnld  44712  digexp  44716  dignn0flhalflem1  44724  dignn0flhalflem2  44725  dignn0ehalf  44726  dignn0flhalf  44727  rrx2plord2  44758  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2vlinest  44777  rrxsphere  44784  itscnhlc0yqe  44795  itsclc0yqsol  44800  itsclc0xyqsolr  44805  itsclc0  44807  itsclc0b  44808  itsclquadb  44812  amgmwlem  44952