Theorem 3ad2ant2 1083

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant1 1079	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simp2l  1087  simp2r  1088  simp21  1094  simp22  1095  simp23  1096  simp2ll  1128  simp2lr  1129  simp2rl  1130  simp2rr  1131  simp2l1  1160  simp2l2  1161  simp2l3  1162  simp2r1  1163  simp2r2  1164  simp2r3  1165  simp21l  1178  simp21r  1179  simp22l  1180  simp22r  1181  simp23l  1182  simp23r  1183  simp211  1199  simp212  1200  simp213  1201  simp221  1202  simp222  1203  simp223  1204  simp231  1205  simp232  1206  simp233  1207  3anim123i  1247  3jaao  1396  ceqsalt  3228  vtoclgftOLD  3255  vtoclegft  3280  sofld  5581  funtpgOLD  5943  fnprg  5947  fntpg  5948  fnco  5999  fvun1  6269  fvcofneq  6367  fsnunf2  6452  oprssov  6803  ovmpt3rab1  6891  sorpssuni  6946  sorpssint  6947  epne3  6980  suppsnop  7309  funsssuppss  7321  fnsuppres  7322  wrecseq123  7408  onfununi  7438  onoviun  7440  smogt  7464  omass  7660  f1dom2g  7973  domunfican  8233  rneqdmfinf1o  8242  mapfien2  8314  inelfi  8324  dffi2  8329  ordiso2  8420  wemapso  8456  unwdomg  8489  wdomima2g  8491  ixpiunwdom  8496  cantnfres  8574  dif1card  8833  ackbij1lem9  9050  ackbij1lem16  9057  cfflb  9081  coflim  9083  cfsmolem  9092  fincssdom  9145  isf32lem11  9185  domtriomlem  9264  axdc4lem  9277  ac6num  9301  axacndlem4  9432  axacndlem5  9433  axacnd  9434  elwina  9508  elina  9509  winaon  9510  inawina  9512  winacard  9514  winainflem  9515  tsksuc  9584  tskuni  9605  grupr  9619  nqereu  9751  enqeq  9756  nqereq  9757  adderpqlem  9776  mulerpqlem  9777  addassnq  9780  mulassnq  9781  distrnq  9783  ltsonq  9791  ltanq  9793  ltmnq  9794  div2neg  10748  lediv2  10913  nndivtr  11062  difgtsumgt  11346  zdivmul  11449  gtndiv  11454  fzind  11475  eluzuzle  11696  eluzp1p1  11713  peano2uz  11741  nn01to3  11781  ledivge1le  11901  xrre2  12001  xaddass  12079  xlt2add  12090  xmulasslem3  12116  xmulass  12117  supxrun  12146  icc0  12223  ubioc1  12227  ubicc2  12289  iccsplit  12305  zltaddlt1le  12324  uzsubsubfz  12363  ssfzunsnext  12386  ssfzunsn  12387  elfz1b  12409  fzp1nel  12424  fz0fzdiffz0  12448  difelfzle  12452  elfzo0  12508  elfzonlteqm1  12543  fzonn0p1p1  12546  fzosplitprm1  12578  fzoshftral  12585  subfzo0  12590  ltdifltdiv  12635  modabs  12703  modcyc  12705  modaddabs  12708  addmodid  12718  modadd2mod  12720  moddi  12738  modsubdir  12739  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  expneg2  12869  expnbnd  12993  digit2  12997  mulsubdivbinom2  13046  muldivbinom2  13047  hashnnn0genn0  13131  hashgadd  13166  hashinfxadd  13174  hashprdifel  13186  hashgt12el2  13211  hashfun  13224  hashres  13225  hashreshashfun  13226  brfi1indlem  13278  ccatval1  13361  ccatass  13371  lswccatn0lsw  13373  ccats1val2  13404  swrd00  13418  swrdval2  13420  swrdlen  13423  swrdn0  13430  swrdnd  13432  swrd0len0  13436  swrd0fv  13439  swrdeq  13444  swrdlen2  13445  swrdfv2  13446  swrdsbslen  13448  swrdspsleq  13449  swrd0swrd0  13463  ccats1swrdeq  13469  ccatopth  13470  ccatopth2  13471  wrd2ind  13477  ccats1swrdeqrex  13478  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat  13493  swrdccat3a  13494  repswswrd  13531  cshwidxmod  13549  cshwidx0  13552  cshwidxm1  13553  cshwidxm  13554  repswcshw  13558  cshimadifsn  13575  cshimadifsn0  13576  ccatco  13581  swrdco  13583  f1oun2prg  13662  swrds2  13685  eqwrds3  13704  trclfvss  13747  relexpaddnn  13791  rediv  13871  imdiv  13878  resqrex  13991  resqrtcl  13994  limsupgle  14208  climuni  14283  mulcn2  14326  iseraltlem3  14414  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  modfsummods  14525  prodfn0  14626  prodfrec  14627  rpnnen2lem7  14949  summodnegmod  15012  divalglem8  15123  modremain  15132  ndvdssub  15133  bitsfzo  15157  nndvdslegcd  15227  dfgcd2  15263  mulgcd  15265  mulgcdr  15267  gcddiv  15268  rplpwr  15276  rppwr  15277  lcmftp  15349  lcmfunsnlem2lem2  15352  qredeq  15371  coprmprod  15375  divgcdcoprmex  15380  cncongr1  15381  cncongr2  15382  ncoprmlnprm  15436  hashgcdlem  15493  vfermltlALT  15507  modprm0  15510  modprmn0modprm0  15512  pythagtriplem1  15521  pythagtriplem3  15523  pythagtriplem10  15525  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem11  15530  pythagtriplem12  15531  pythagtriplem13  15532  pythagtriplem14  15533  pythagtriplem16  15535  pythagtriplem19  15538  pythagtrip  15539  dvdsprmpweqnn  15589  difsqpwdvds  15591  pcfaclem  15602  pcbc  15604  vdwapun  15678  vdwapid1  15679  fvprmselgcd1  15749  prmgaplem6  15760  cshwshashlem2  15803  cshwrepswhash1  15809  setsstruct  15898  setsstructOLD  15899  imasaddvallem  16189  ismre  16250  mreincl  16259  submre  16265  mrcss  16276  comfeq  16366  cofurid  16551  initoeu2lem0  16663  funcestrcsetclem9  16788  funcsetcestrclem9  16803  xpcpropd  16848  issubmnd  17318  frmdup3lem  17403  frmdup3  17404  mulginvcom  17565  mulgassr  17580  mulgmodid  17581  cycsubg2cl  17632  ghmnsgima  17684  pgrpsubgsymg  17828  pmtrprfv3  17874  pmtr3ncomlem1  17893  mndodcongi  17962  oddvdsnn0  17963  oddvds  17966  odeq  17969  odmulg2  17972  odmulg  17973  odhash2  17990  odhash3  17991  gexnnod  18003  gexcl2  18004  isslw  18023  subgslw  18031  oppglsm  18057  lsmsubm  18068  lsmless1  18074  lsmless2  18075  lsmass  18083  efgsval2  18146  efgsrel  18147  efgsfo  18152  ghmplusg  18249  odadd1  18251  odadd2  18252  gsumconst  18334  ablfac1eu  18472  pgpfac1lem5  18478  ablfaclem3  18486  ringidss  18577  irredrmul  18707  abvres  18839  srngadd  18857  srngmul  18858  rmodislmodlem  18930  rmodislmod  18931  lssincl  18965  lsslsp  19015  reslmhm2b  19054  lsmsp  19086  sralmod  19187  assa2ass  19322  aspid  19330  asclmul1  19339  asclmul2  19340  evlsval2  19520  coe1add  19634  coe1addfv  19635  coe1subfv  19636  zrhpsgninv  19931  zrhpsgnevpm  19937  zrhpsgnodpm  19938  psgndiflemB  19946  regsumsupp  19968  uvcval  20124  uvcresum  20132  lindsind2  20158  f1lindf  20161  lindsss  20163  f1linds  20164  lsslindf  20169  lsslinds  20170  islindf4  20177  lbslcic  20180  mndvcl  20197  mndvass  20198  mhmvlin  20203  matsubgcell  20240  matinvgcell  20241  matvscacell  20242  matmulcell  20251  mattposm  20265  madetsmelbas  20270  madetsmelbas2  20271  scmatf1  20337  mavmuldm  20356  marrepcl  20370  marepvcl  20375  ma1repveval  20377  mulmarep1el  20378  mulmarep1gsum1  20379  mulmarep1gsum2  20380  1marepvsma1  20389  m1detdiag  20403  mdetdiag  20405  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  mdetmul  20429  m2detleiblem3  20435  m2detleiblem4  20436  gsummatr01lem3  20463  smadiadetglem2  20478  matinv  20483  slesolinv  20486  slesolinvbi  20487  slesolex  20488  cramerimplem1  20489  cramerimplem2  20490  cramerlem1  20493  mat2pmatbas  20531  d1mat2pmat  20544  m2pmfzgsumcl  20553  decpmatcl  20572  decpmatid  20575  decpmatmul  20577  pmatcollpw1  20581  pmatcollpw2lem  20582  pmatcollpw2  20583  pmatcollpwlem  20585  pmatcollpw  20586  pmatcollpwfi  20587  mply1topmatcllem  20608  mply1topmatcl  20610  mp2pm2mplem2  20612  mp2pm2mplem4  20614  chmatcl  20633  chmatval  20634  chpmatply1  20637  chpmat1dlem  20640  chpmat1d  20641  chpdmatlem2  20644  chpdmatlem3  20645  chpdmat  20646  chfacfscmulcl  20662  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadurid  20672  cpmidpmatlem2  20676  cpmidpmatlem3  20677  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  cpmadumatpolylem1  20686  cpmadumatpoly  20688  chcoeffeqlem  20690  cayhamlem4  20693  cayleyhamilton1  20697  ntrin  20865  elnei  20915  restco  20968  restcldi  20977  sslm  21103  cnt1  21154  cmpsublem  21202  cmpcld  21205  kgen2ss  21358  upxp  21426  xkopjcn  21459  xkococnlem  21462  xkococn  21463  qtopval2  21499  qtoptop2  21502  ordthmeolem  21604  isfil2  21660  fgss  21677  fbasrn  21688  ufilmax  21711  filufint  21724  fmval  21747  elfm2  21752  elfm3  21754  rnelfmlem  21756  rnelfm  21757  flimrest  21787  flfnei  21795  isflf  21797  flffbas  21799  fclsrest  21828  cnpfcfi  21844  alexsubALTlem4  21854  subgntr  21910  opnsubg  21911  tgpconncompss  21917  qustgpopn  21923  qustgphaus  21926  utopsnnei  22053  blres  22236  metcnp3  22345  blval2  22367  xmsusp  22374  nmmtri  22426  nmrtri  22428  tngngp3  22460  nrmtngnrm  22462  nminvr  22473  nmotri  22543  nghmplusg  22544  tgqioo  22603  iccpnfhmeo  22744  isclmp  22897  ncvsi  22951  ncvsge0  22953  caun0  23079  cmetcusp1  23149  rrxmvallem  23187  pjth  23210  volss  23301  volsup2  23373  itg2le  23506  dvn2bss  23693  mdegldg  23826  mdegnn0cl  23831  deg1ldgdomn  23854  deg1mul3  23875  drnguc1p  23930  ig1peu  23931  ig1pdvds  23936  coeid3  23996  coe11  24009  dgradd2  24024  facth  24061  dvtaylp  24124  pserdvlem2  24182  ptolemy  24248  tanord1  24283  cxple2  24443  cxpeq  24498  logbchbase  24509  relogbcl  24511  relogbreexp  24513  isosctrlem2  24549  muval1  24859  dvdssqf  24864  chpwordi  24883  efchtdvds  24885  logfacbnd3  24948  bcmono  25002  efexple  25006  lgslem1  25022  lgsneg  25046  lgssq2  25063  lgsdirnn0  25069  gausslemma2dlem1a  25090  2lgslem1a1  25114  dchrmusumlema  25182  selberglem3  25236  pntrmax  25253  padicabv  25319  brbtwn2  25785  ax5seglem2  25809  ax5seglem3  25811  axlowdim  25841  axcontlem7  25850  axcontlem8  25851  incistruhgr  25974  numedglnl  26039  uhgr2edg  26100  issubgr2  26164  0uhgrsubgr  26171  subgrfun  26173  subgreldmiedg  26175  subumgredg2  26177  fusgrfisbase  26220  fusgrfisstep  26221  fusgrfis  26222  nbupgrres  26266  nbusgrfi  26276  nb3grprlem1  26282  cplgr3v  26331  umgr2v2evd2  26423  finsumvtxdg2size  26446  vtxdgoddnumeven  26449  frusgrnn0  26467  upgrewlkle2  26502  iedginwlk  26533  uspgr2wlkeq2  26543  pthdivtx  26625  upgrwlkdvde  26633  upgrwlkdvspth  26635  uhgrwkspth  26651  usgr2wlkspthlem2  26654  usgr2pth  26660  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  wwlknp  26734  wwlkswwlksn  26750  wlkiswwlks1  26753  wlkiswwlks2lem4  26758  wwlksm1edg  26767  wwlksnred  26787  wwlksnextbi  26789  wwlksnredwwlkn  26790  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextbij0  26796  2pthon3v  26839  elwwlks2ons3  26848  umgrwwlks2on  26850  wpthswwlks2on  26854  elwspths2spth  26862  rusgrnumwwlks  26869  rusgrnumwlkg  26872  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwlkclwwlk  26903  umgrclwwlksge2  26912  clwwlksf  26915  clwwlksext2edg  26923  wwlksext2clwwlk  26924  clwwisshclwwslemlem  26926  clwwisshclwwslem  26927  clwwisshclwws  26928  clwwnisshclwwsn  26930  erclwwlksref  26934  umgr2cwwk2dif  26941  umgr2cwwkdifex  26942  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  3wlkdlem9  27028  uhgr3cyclex  27042  eucrctshift  27103  eucrct2eupth  27105  nfrgr2v  27136  3vfriswmgr  27142  3cyclfrgrrn2  27151  n4cyclfrgr  27155  4cyclusnfrgr  27156  frgr2wwlkeqm  27195  frrusgrord0lem  27203  frrusgrord0  27204  numclwwlkovfel2  27216  numclwwlkovf2ex  27219  numclwwlk2lem1  27235  numclwwlk3OLD  27242  numclwwlk3  27243  numclwwlk5  27246  l2p  27331  n0lpligALT  27336  nvsge0  27519  nmoub2i  27629  isblo3i  27656  dipassr2  27702  bcs2  28039  elspansn2  28426  fh2  28478  pjoi0  28576  homco2  28836  leopmul  28993  cdj3lem2  29294  fnunres1  29417  rexdiv  29634  archiexdiv  29744  symgfcoeu  29845  locfinreflem  29907  pstmfval  29939  unitdivcld  29947  pl1cn  30001  nmmulg  30012  nexple  30071  sigaclcuni  30181  inelpisys  30217  volfiniune  30293  dya2iocnrect  30343  omsfval  30356  sitmcl  30413  eulerpartlemn  30443  probun  30481  cndprobtot  30498  ballotlemsgt1  30572  ballotlemieq  30578  ballotlemfrcn0  30591  signstfvp  30648  bnj240  30765  bnj836  30830  bnj545  30965  bnj600  30989  bnj966  31014  bnj967  31015  bnj1097  31049  bnj1118  31052  bnj1128  31058  bnj1204  31080  bnj1321  31095  bnj1408  31104  bnj1514  31131  cnpconn  31212  cvmsf1o  31254  cvmscld  31255  cvmlift2lem6  31290  eqfunresadj  31659  dfrdg2  31701  frrlem5e  31788  noseponlem  31817  nosepon  31818  nolesgn2o  31824  nolesgn2ores  31825  nosepssdm  31836  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem2  31855  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  fvtransport  32139  nn0prpwlem  32317  nn0prpw  32318  ivthALT  32330  fness  32344  topmeet  32359  fnejoin1  32363  nndivsub  32456  bj-ceqsalt0  32873  bj-ceqsalt1  32874  topdifinffinlem  33195  ptrecube  33409  mblfinlem2  33447  itg2addnclem  33461  f1ocan1fv  33521  f1ocan2fv  33522  upixp  33524  filbcmb  33535  mettrifi  33553  ghomidOLD  33688  rngohom0  33771  rngohomsub  33772  rngokerinj  33774  intidl  33828  keridl  33831  lsmsat  34295  lcv1  34328  atcmp  34598  atnle  34604  cvlatcvr2  34629  hlsupr2  34673  cvrval3  34699  atcvr0eq  34712  2atlt  34725  llnnleat  34799  llnle  34804  llncmp  34808  2llnmat  34810  lplnle  34826  2lplnmN  34845  2llnmj  34846  lplncmp  34848  lvolcmp  34903  2lplnmj  34908  pmapmeet  35059  2lnat  35070  elpadd2at  35092  pclssN  35180  lhp0lt  35289  lhpj1  35308  lhpmcvr5N  35313  lhpmcvr6N  35314  ltrneq  35435  cdleme0aa  35497  cdleme10  35541  cdleme27a  35655  cdleme32fva  35725  cdleme42b  35766  cdlemf1  35849  cdlemg35  36001  tendovalco  36053  tendoidcl  36057  tendo0co2  36076  cdleml7  36270  dvhopvadd  36382  dvhopellsm  36406  dihmeetcN  36591  dihmeet  36632  mapdrvallem2  36934  mapdpglem32  36994  nacsfix  37275  mapco2g  37277  mapfzcons  37279  mzpexpmpt  37308  mzpsubst  37311  mzpresrename  37313  coeq0i  37316  eldioph2lem1  37323  lzunuz  37331  diophren  37377  pellexlem1  37393  pell14qrexpclnn0  37430  pellqrexplicit  37441  reglogcl  37454  reglogmul  37457  reglogexp  37458  rmxycomplete  37482  monotuz  37506  zindbi  37511  rmxypos  37514  jm2.17a  37527  congtr  37532  congmul  37534  congabseq  37541  acongsym  37543  acongrep  37547  fzneg  37549  acongeq  37550  jm2.19  37560  jm2.20nn  37564  jm2.15nn0  37570  rmydioph  37581  rmxdiophlem  37582  jm3.1  37587  rpnnen3lem  37598  aomclem2  37625  islssfgi  37642  pwssplit4  37659  hbtlem1  37693  hbtlem2  37694  hbtlem5  37698  cnsrexpcl  37735  ioounsn  37795  iocinico  37797  iunrelexp0  37994  relexpss1d  37997  relexpxpmin  38009  tratrb  38746  chordthmALT  39169  fnchoice  39188  suprnmpt  39355  mapsnd  39388  iunmapsn  39409  iuneqfzuzlem  39550  suplesup  39555  infrpge  39567  ioomidp  39740  fmul01lt1lem1  39816  climsuselem1  39839  climsuse  39840  mullimc  39848  islptre  39851  mullimcf  39855  limcrecl  39861  addlimc  39880  limclner  39883  fnlimfvre  39906  limsupmnfuzlem  39958  limsupre3uzlem  39967  climuzlem  39975  limsupresxr  39998  liminfresxr  39999  cosknegpi  40080  icccncfext  40100  dvdsn1add  40154  dvnmptconst  40156  dvnprodlem1  40161  volioc  40188  itgspltprt  40195  volico  40200  stoweidlem10  40227  stoweidlem14  40231  stoweidlem16  40233  stoweidlem17  40234  stoweidlem20  40237  stoweidlem44  40261  stoweidlem57  40274  stoweidlem60  40277  wallispilem3  40284  fourierdlem41  40365  fourierdlem42  40366  fourierdlem52  40375  fourierdlem79  40402  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  elaa2  40451  etransclem48  40499  rrxtopnfi  40506  ioorrnopnlem  40524  saldifcl2  40546  salexct  40552  subsaliuncl  40576  sge0tsms  40597  sge0sup  40608  sge0gerp  40612  sge0pnffigt  40613  sge0resplit  40623  sge0rpcpnf  40638  sge0xaddlem2  40651  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  nnfoctbdj  40673  meaiuninclem  40697  meaiininc2  40702  ovnhoilem2  40816  opnvonmbllem2  40847  ovolval5lem3  40868  smfaddlem1  40971  smfinflem  41023  smflimsupmpt  41035  smfliminfmpt  41038  elfzelfzlble  41331  subsubelfzo0  41336  fzoopth  41337  fsummmodsndifre  41344  fsummmodsnunz  41345  iccpartiltu  41358  iccpartigtl  41359  icceuelpart  41372  iccpartnel  41374  pfxnd  41395  pfxlen0  41396  pfxfv  41399  pfxeq  41404  ccatpfx  41409  pfxpfx  41415  ccats1pfxeq  41421  pfxccat3  41426  pfxccat3a  41429  pfxco  41438  goldbachthlem2  41458  fmtnoprmfac1  41477  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  pwdif  41501  2pwp1prmfmtno  41504  lighneallem2  41523  lighneallem3  41524  lighneallem4b  41526  lighneallem4  41527  even3prm2  41628  mogoldbblem  41629  gbowgt5  41650  evengpop3  41686  evengpoap3  41687  bgoldbtbndlem2  41694  uspgropssxp  41752  ringrng  41879  c0snmhm  41915  lidldomn1  41921  rngccatidALTV  41989  funcringcsetcALTV2lem9  42044  ringccatidALTV  42052  mapsnop  42123  nn0sumltlt  42128  gsumpr  42139  scmsuppss  42153  rmfsupp  42155  mndpfsupp  42157  mptcfsupp  42161  ply1ass23l  42170  ply1sclrmsm  42171  ply1mulgsumlem1  42174  lincfsuppcl  42202  linccl  42203  lincvalsng  42205  lincvalpr  42207  lincdifsn  42213  linc1  42214  lincsum  42218  lincscm  42219  ellcoellss  42224  lincext2  42244  lincext3  42245  lincresunitlem1  42264  lincresunitlem2  42265  lincresunit2  42267  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  lincreslvec3  42271  islindeps2  42272  difmodm1lt  42317  fdivmpt  42334  fdivmptf  42335  refdivmptf  42336  fdivpm  42337  refdivpm  42338  elbigolo1  42351  rege1logbzge0  42353  fllog2  42362  nnolog2flm1  42384  digvalnn0  42393  nn0digval  42394  dignn0fr  42395  dignn0ldlem  42396  dignnld  42397  digexp  42401  dignn0ehalf  42411  dignn0flhalf  42412  setrec2fun  42439