Theorem ancoms 461

Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)

Hypothesis

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

Assertion

Ref	Expression
ancoms	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	expcom 416	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 409	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem is referenced by:  pm3.22  462  adantl  484  sylan9bbr  513  syl2anr  598  anim12ci  615  im2anan9r  622  bi2anan9r  638  anabss4  665  anabsi7  669  anabsi8  670  mp3anr1  1454  mp3anr2  1455  mp3anr3  1456  stoic1b  1774  cbvaldvaw  2045  dvelimf  2470  2eu3  2738  eqeqan12rd  2840  sylan9eqr  2878  r19.29r  3255  r19.29vvaOLD  3337  cbvrexdva2  3457  morex  3710  sbcrext  3856  sylan9ssr  3981  pssdifcom1  4435  pssdifcom2  4436  preq12nebg  4793  opthprneg  4795  riinn0  5005  breqan12rd  5083  snopeqop  5396  propeqop  5397  soinxp  5633  frinxp  5634  seinxp  5635  brelrng  5811  dminss  6010  imainss  6011  sossfld  6043  cnvsng  6080  setlikespec  6169  ordelssne  6218  ordtri3or  6223  ordtri2  6226  ordtri4  6228  ordtri2or  6286  funsng  6405  f1co  6585  f1oprswap  6658  funimass4  6730  dffv2  6756  fvmptdf  6774  fndmdifcom  6813  fsn2  6898  fvtp2  6958  fvtp3  6959  fvtp2g  6961  fvtp3g  6962  soisoi  7081  riotaeqimp  7140  oveqan12rd  7176  brrpssg  7451  sorpsscmpl  7460  dfwe2  7496  ordsucelsuc  7537  ordunisuc2  7559  tfindsg  7575  tfindsg2  7576  dfom2  7582  funcnvuni  7636  fiunlem  7643  cofunex2g  7651  curry2  7802  soxp  7823  mpoxopoveqd  7887  tposoprab  7928  wfr3g  7953  wfrlem5  7959  wfrlem10  7964  smores3  7990  smores2  7991  smoel  7997  tfr3  8035  tz7.48-2  8078  tz7.49  8081  oaordi  8172  oaword  8175  oaord1  8177  oaword2  8179  oa00  8185  oalimcl  8186  oaass  8187  oarec  8188  oacomf1o  8191  omord2  8193  omcan  8195  omword  8196  omword1  8199  omword2  8200  odi  8205  omass  8206  oneo  8207  oen0  8212  oecan  8215  oelim2  8221  nnarcl  8242  nnaordi  8244  nnaordr  8246  nnawordi  8247  nnmsucr  8251  nnmcom  8252  nnaword  8253  nnmordi  8257  nnaordex  8264  oaabslem  8270  omabslem  8273  nnneo  8278  omsmo  8281  ersym  8301  elecg  8332  riiner  8370  ecopovsym  8399  ecovcom  8403  mapvalg  8416  pmvalg  8417  elpmg  8422  elmapssres  8431  pmss12g  8433  ixpconstg  8470  ener  8556  domtr  8562  f1imaeng  8569  fundmen  8583  xpcomco  8607  xpsnen2g  8610  xpdom2  8612  xpdom1g  8614  omxpen  8619  omf1o  8620  enen2  8658  domen2  8660  sdomen2  8662  domtriord  8663  sdomel  8664  onsdominel  8666  infensuc  8695  onomeneq  8708  nndomo  8712  pssnn  8736  unbnn  8774  fiint  8795  mapfi  8820  fiin  8886  fiss  8888  infempty  8971  oiiso  9001  unwdomg  9048  suc11reg  9082  inf3lem5  9095  infeq5  9100  cantnfp1lem3  9143  r1tr  9205  r1val1  9215  rankr1ai  9227  rankonidlem  9257  onssr1  9260  djuex  9337  djuunxp  9350  tskwe  9379  carddom2  9406  carden2  9416  domtri2  9418  cardval2  9420  fidomtri  9422  fidomtri2  9423  harval2  9426  dif1card  9436  infxpenlem  9439  ac5num  9462  alephord3  9504  alephdom  9507  aleph11  9510  alephdom2  9513  cardaleph  9515  dfac3  9547  dfac5  9554  onadju  9619  pwsdompw  9626  ackbij1lem11  9652  ackbij2  9665  cfeq0  9678  cfsuc  9679  cff1  9680  cflim2  9685  cfsmolem  9692  coftr  9695  sornom  9699  infpssrlem4  9728  ssfin4  9732  ssfin2  9742  ssfin3ds  9752  fin23lem31  9765  isf32lem9  9783  hsmexlem5  9852  axdc3lem  9872  axdc3lem2  9873  axdc3lem4  9875  zorn2lem6  9923  brdom3  9950  brdom7disj  9953  brdom6disj  9954  alephval2  9994  alephreg  10004  wuncss  10167  gruen  10234  addcompi  10316  mulcompi  10318  ltapi  10325  ltmpi  10326  nqereu  10351  addcompq  10372  addcomnq  10373  mulcompq  10374  mulcomnq  10375  ltsonq  10391  ltanq  10393  ltmnq  10394  genpnnp  10427  addcompr  10443  mulcompr  10445  ltsopr  10454  ltexprlem2  10459  prlem936  10469  suplem2pr  10475  map2psrpr  10532  axpre-ltadd  10589  xrltnle  10708  axlttri  10712  axsup  10716  ltnle  10720  letri3  10726  leloe  10727  eqlelt  10728  letric  10740  mul31  10807  subcl  10885  pncan2  10893  pncan3  10894  npcan  10895  addsubeq4  10901  npncan3  10924  negsubdi2  10945  muladd  11072  subdi  11073  mulneg2  11077  mulsub  11083  ltleadd  11123  ltsubpos  11132  posdif  11133  addge01  11150  lesub0  11157  wloglei  11172  prodgt02  11488  mulsuble0b  11512  ltdivmul  11515  ledivmul  11516  lt2mul2div  11518  lerec  11523  lt2msq  11525  ltdiv23  11531  lediv23  11532  le2msq  11540  msq11  11541  fimaxreOLD  11585  infm3  11600  dfinfre  11622  creur  11632  creui  11633  cju  11634  nnmulcl  11662  nndivtr  11685  avgle1  11878  avgle2  11879  avgle  11880  nn0nnaddcl  11929  ltsubnn0  11949  zrevaddcl  12028  znnsub  12029  znn0sub  12030  zextlt  12057  gtndiv  12060  prime  12064  uztrn2  12263  uztric  12267  uz11  12268  nn0pzuz  12306  uzwo  12312  zmax  12346  zbtwnre  12347  rebtwnz  12348  qrevaddcl  12371  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  difrp  12428  xrltnsym  12531  xrlttri  12533  xrleloe  12538  xrletri  12547  xrletri3  12548  xrmaxeq  12573  xrmineq  12574  xrmaxlt  12575  xrmaxle  12577  lemaxle  12589  z2ge  12592  qbtwnre  12593  qextlt  12597  qextle  12598  xleneg  12612  xaddcom  12634  xmulcom  12660  xmulneg2  12664  xmulgt0  12677  xrsupsslem  12701  xrinfmsslem  12702  supxrunb1  12713  supxrunb2  12714  ixxssixx  12753  ixxin  12756  ioon0  12765  iccid  12784  iooshf  12816  iccsupr  12831  iooneg  12858  iccneg  12859  iccsplit  12872  fzen  12925  fzadd2  12943  fzass4  12946  fzrev  12971  fznn  12976  elfzp1b  12985  elfzm1b  12986  fz0fzdiffz0  13017  difelfznle  13022  fzon  13059  fzo0n  13060  fzonmapblen  13084  elfzoext  13095  eluzgtdifelfzo  13100  ubmelm1fzo  13134  elfzom1elp1fzo1  13138  subfzo0  13160  fllt  13177  flflp1  13178  flbi  13187  flbi2  13188  flzadd  13197  ltdifltdiv  13205  modcyc2  13276  modifeq2int  13302  modaddmodup  13303  modaddmodlo  13304  modfzo0difsn  13312  modsumfzodifsn  13313  om2uzlt2i  13320  om2uzf1oi  13322  fseqsupubi  13347  fsuppmapnn0fiub0  13362  expcllem  13441  mulbinom2  13585  expnngt1  13603  faclbnd5  13659  hashbnd  13697  hasheni  13709  hasheqf1oi  13713  hashdom  13741  hashunsnggt  13756  hashss  13771  hashgt23el  13786  hashfacen  13813  ccatalpha  13947  swrdspsleq  14027  wrd2ind  14085  pfxccatin12lem1  14090  pfxccatin12lem2  14093  pfxccatin12  14095  swrdccat3blem  14101  repswsymballbi  14142  cshwsublen  14158  cshwn  14159  cshwlen  14161  cshwidxmod  14165  cshf1  14172  repswcshw  14174  cshweqdif2  14181  cshweqrep  14183  cshwcsh2id  14190  ccatco  14197  swrdco  14199  lswco  14201  s3iunsndisj  14328  relexprelg  14397  relexpnndm  14400  relexpaddnn  14410  shftlem  14427  shftuz  14428  shftfval  14429  shftval4  14436  shftval5  14437  2shfti  14439  seqshft  14444  mulre  14480  sqrtlt  14621  abs3dif  14691  abs2difabs  14694  uzin2  14704  rexanre  14706  caubnd  14718  climshftlem  14931  rlimcn2  14947  fsumcnv  15128  modfsummods  15148  geo2lim  15231  ntrivcvgfvn0  15255  prodmo  15290  zprod  15291  prodss  15301  fprodcnv  15337  bpolysum  15407  bpoly4  15413  efle  15471  reef11  15472  demoivre  15553  demoivreALT  15554  sqrt2irr  15602  nndivides  15617  0dvds  15630  muldvds1  15634  muldvds2  15635  dvdscmulr  15638  dvdssubr  15655  dvdsadd2b  15656  odd2np1  15690  mulsucdiv2z  15702  ltoddhalfle  15710  divalglem9  15752  gcdcllem1  15848  gcdcom  15862  neggcd  15871  gcdabs2  15879  modgcd  15880  lcmcom  15937  neglcm  15948  lcmgcdeq  15956  coprmdvds  15997  qredeq  16001  divgcdcoprmex  16010  cncongrprm  16069  odzdvds  16132  modprmn0modprm0  16144  coprimeprodsq  16145  pythagtriplem1  16153  pythagtriplem4  16156  pc2dvds  16215  pc11  16216  pcz  16217  pcprod  16231  prmunb  16250  1arithlem3  16261  1arith  16263  cshwshashlem3  16431  ressabs  16563  acsfn2  16934  issect  17023  funcestrcsetclem9  17398  funcsetcestrclem5  17409  funcsetcestrclem9  17413  pospo  17583  latjcom  17669  latmcom  17685  clatglbss  17737  pospropd  17744  pslem  17816  tsrss  17833  issubmnd  17938  submcl  17977  resmhm2b  17987  frmdmnd  18024  frmd0  18025  smndex1mnd  18075  pwmndid  18101  pwmnd  18102  grpinvsub  18181  dfgrp3lem  18197  cycsubm  18345  cyccom  18346  gimco  18408  gictr  18415  cntz2ss  18463  cntzrec  18464  symg2bas  18521  symgextf1  18549  symgfixelsi  18563  pmtrfinv  18589  pmtrdifwrdel2  18614  dfod2  18691  lsmcom2  18780  efgred  18874  qusabl  18985  cygablOLD  19011  eldprd  19126  prmgrpsimpgd  19236  srgmulgass  19281  dfrhm2  19469  isrim0  19475  rmodislmodlem  19701  rmodislmod  19702  mplcoe5lem  20248  psrbagfsupp  20289  cnfldexp  20578  cnsrng  20579  xrsdsreval  20590  dvdsrzring  20630  znf1o  20698  ocvocv  20815  ocvin  20818  frlmip  20922  islindf  20956  lindff  20959  lindfrn  20965  f1lindf  20966  mamudir  21013  matsca2  21029  matlmod  21038  matinvgcell  21044  mat1bas  21058  dmatmul  21106  dmatsgrp  21108  dmatsrng  21110  dmatcrng  21111  scmatsgrp1  21131  scmatsrng1  21132  madulid  21254  gsummatr01lem3  21266  gsummatr01  21268  cpmatacl  21324  0mat2pmat  21344  idmatidpmat  21345  m2cpminv0  21369  pmatcollpw3fi1lem1  21394  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  eltg  21565  eltg2  21566  tgss  21576  tgss2  21595  basgen2  21597  bastop1  21601  cldmre  21686  toponmre  21701  opnneiss  21726  restcldr  21782  restfpw  21787  restcls  21789  restntr  21790  ordtbaslem  21796  ordtrest2lem  21811  leordtvallem2  21819  leordtval  21821  cnrest  21893  t0sep  21932  cmpcov  21997  cmpsublem  22007  cmpsub  22008  bwth  22018  2ndcomap  22066  locfincmp  22134  ptval  22178  xkoval  22195  txss12  22213  ptrescn  22247  xkopt  22263  hmeofval  22366  txswaphmeolem  22412  txswaphmeo  22413  trfbas2  22451  trfbas  22452  uzrest  22505  numufl  22523  ssufl  22526  flimclsi  22586  hauspwpwf1  22595  ghmcnp  22723  blpnfctr  23046  metequiv  23119  metcnp3  23150  elbl4  23173  restmetu  23180  tngngp  23263  qtopbaslem  23367  bl2ioo  23400  ioo2bl  23401  ioo2blex  23402  xrsxmet  23417  divccn  23481  divccncf  23514  isclmi0  23702  iscvsi  23733  causs  23901  lmclim  23906  bcthlem1  23927  ovolfsf  24072  ioombl  24166  iccvolcl  24168  ioovolcl  24171  ioorcl  24178  volcn  24207  itg2itg1  24337  dvexp  24550  dvmptfsum  24572  dvexp3  24575  dvef  24577  dvlip  24590  c1lip1  24594  ftc1a  24634  tdeglem1  24652  tdeglem3  24653  tdeglem4  24654  coe1termlem  24848  plyremlem  24893  ptolemy  25082  cos11  25117  logeftb  25167  logleb  25186  logdivlt  25204  logdivle  25205  angval  25379  isppw2  25692  issqf  25713  vmasum  25792  lgsprme0  25915  gausslemma2dlem1a  25941  lgsquadlem3  25958  2lgsoddprmlem2  25985  ostth  26215  brbtwn2  26691  colinearalglem4  26695  ax5seglem1  26714  ax5seglem2  26715  axcontlem2  26751  axcontlem12  26761  upgrpredgv  26924  uhgr2edg  26990  issubgr  27053  subgrprop  27055  subuhgr  27068  subupgr  27069  subumgr  27070  subusgr  27071  nb3grprlem2  27163  cplgr3v  27217  wlk1walk  27420  upgrwlkvtxedg  27426  pthdivtx  27510  crctcshwlkn0lem3  27590  crctcshwlkn0lem6  27593  crctcshwlkn0lem7  27594  crctcshwlkn0  27599  wlkiswwlks2  27653  wwlksnfiOLD  27685  wwlksnextprop  27691  erclwwlksym  27799  clwwlkn1  27819  clwwlkfo  27829  erclwwlknsym  27849  clwwlknonex2lem2  27887  is0wlk  27896  is0trl  27902  3pthdlem1  27943  frgr3v  28054  frgrncvvdeqlem3  28080  frgrregorufr  28104  clwwnonrepclwwnon  28124  extwwlkfab  28131  numclwwlk1  28140  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  vcz  28352  isvcOLD  28356  isnv  28389  isnvi  28390  nmooge0  28544  nmblolbii  28576  blocnilem  28581  ipblnfi  28632  hvpncan2  28817  hvaddsub4  28855  hire  28871  abshicom  28878  hial2eq2  28884  orthcom  28885  hhssabloi  29039  ocsh  29060  shscli  29094  shscom  29096  shsel2  29099  spanss  29125  shjcom  29135  shmodsi  29166  chpsscon3  29280  spansni  29334  spansnmul  29341  spansncol  29345  spanunsni  29356  cmcm2  29393  cm2j  29397  spansncvi  29429  5oalem2  29432  3oalem2  29440  honegsubdi2  29588  adjsym  29610  cnvadj  29669  brafn  29724  kbpj  29733  riesz3i  29839  cnlnadjlem2  29845  cnlnadjlem9  29852  nmopcoi  29872  cnvbraval  29887  leop  29900  leop3  29902  leopmul2i  29912  leoptri  29913  hstrlem3a  30037  cvcon3  30061  cvnsym  30067  mdbr2  30073  dmdmd  30077  dmdbr2  30080  dmdbr3  30082  dmdbr4  30083  dmdbr5  30085  mdsl0  30087  ssmd2  30089  mdslmd1lem1  30102  mdslmd1lem2  30103  mdslmd3i  30109  mdslmd4i  30110  atcveq0  30125  superpos  30131  atnemeq0  30154  atssma  30155  atexch  30158  atomli  30159  atcvatlem  30162  atcvati  30163  chirredlem1  30167  chirredlem3  30169  chirredi  30171  atcvat3i  30173  atdmd  30175  mdsymlem1  30180  mdsymlem3  30182  mdsymlem4  30183  mdsymlem5  30184  mdsymlem8  30187  dmdsym  30190  atdmd2  30191  sumdmdlem  30195  cdjreui  30209  cdj3lem2b  30214  cdj3i  30218  r19.29ffa  30237  opreu2reuALT  30240  imadifxp  30351  abfmpel  30400  xaddeq0  30477  xrofsup  30492  xnn0gt0  30494  xeqlelt  30499  xdivpnfrp  30609  xrsinvgval  30664  xrsmulgzz  30665  pcmplfin  31124  cnvordtrestixx  31156  ordtrest2NEWlem  31165  indval  31272  esumpfinvallem  31333  sigagenss  31408  ddemeas  31495  brae  31500  dya2iocival  31531  dya2iocnei  31540  dya2iocuni  31541  omsf  31554  oddpwdc  31612  bnj934  32207  spthcycl  32376  derangenlem  32418  subfacval2  32434  kur14  32463  sat1el2xp  32626  fmlasucdisj  32646  satfun  32658  lediv2aALT  32920  dford5  32957  faclim2  32980  funpsstri  33008  dftrpred3g  33072  soseq  33096  wsuclem  33112  fprlem1  33137  fpr1  33139  frrlem15  33142  frr1  33144  elno  33153  nosepon  33172  noextenddif  33175  sltsolem1  33180  nosepne  33185  nolt02o  33199  sltnle  33232  sleloe  33233  sletri3  33234  hfelhf  33642  elicc3  33665  nn0prpwlem  33670  nn0prpw  33671  isfne  33687  onsuct0  33789  nndivsub  33805  bj-nnfbit  34081  bj-restsnss  34377  bj-restsnss2  34378  bj-restuni2  34392  bj-snmoore  34408  topdifinffinlem  34631  iooelexlt  34646  relowlssretop  34647  rdgeqoa  34654  finorwe  34666  nlpineqsn  34692  pibt2  34701  wl-sbcom2d-lem1  34810  wl-sbcom2d  34812  wl-ax11-lem6  34837  curf  34885  finixpnum  34892  ltflcei  34895  leceifl  34896  cos2h  34898  matunitlindflem1  34903  matunitlindflem2  34904  matunitlindf  34905  ptrecube  34907  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem27  34934  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  cnambfre  34955  itg2addnclem2  34959  itg2addnc  34961  itg2gt0cn  34962  ftc1anclem1  34982  ftc1anclem4  34985  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anc  34990  unirep  35003  opelopab3  35007  fvopabf4g  35011  indexa  35023  filbcmb  35030  incsequz2  35039  metf1o  35045  sstotbnd3  35069  isbnd2  35076  bndss  35079  ismtycnv  35095  iccbnd  35133  exidreslem  35170  exidresid  35172  ghomco  35184  isdivrngo  35243  isdrngo2  35251  rngoisocnv  35274  riscer  35281  crngohomfo  35299  unichnidl  35324  maxidlmax  35336  igenmin  35357  exmid2  35392  orel  35395  brcosscnvcoss  35694  brssr  35756  brdmqss  35896  prtlem16  36020  paddss1  36968  paddss2  36969  paddss12  36970  pclfinN  37051  erngmul-rN  37965  mapdordlem2  38788  addsubeq4com  39215  dvdsexpim  39230  renegadd  39251  rersubcl  39257  repncan3  39262  readdsub  39263  reltsub1  39265  renpncan3  39270  resubdi  39275  ismrc  39347  nacsfg  39351  isnacs3  39356  incssnn0  39357  mzpclall  39373  lerabdioph  39451  ltrabdioph  39454  eldioph4b  39457  jm2.17b  39607  congrep  39619  lnr2i  39765  ontric3g  39937  nndomog  39946  brnonrel  39998  enrelmap  40392  enrelmapr  40393  rcompleq  40419  isotone1  40447  isotone2  40448  radcnvrat  40695  expgrowth  40716  bcc0  40721  binomcxplemnn0  40730  2sbc6g  40796  2sbc5g  40797  ordpss  40832  addrcom  40856  3impcombi  41200  sspwimp  41301  sspwimpVD  41302  ax6e2ndeqALT  41314  iunconnlem2  41318  sineq0ALT  41320  nsstr  41410  iunmapsn  41529  ssfiunibd  41625  fmul01  41910  lptre2pt  41970  stoweidlem34  42368  dirkeritg  42436  fourierdlem73  42513  smfsuplem1  43134  smfinflem  43140  sigarac  43158  or2expropbi  43318  euoreqb  43357  2reu3  43358  2reuimp  43363  dfatelrn  43379  afv0nbfvbi  43399  dmfcoafv  43423  dfatcolem  43503  cnambpcma  43543  ltnltne  43548  fzoopth  43576  elmod2  43579  imasetpreimafvbijlemf1  43613  fundcmpsurbijinj  43619  fundcmpsurinjALT  43621  ichreuopeq  43684  sprsymrelfolem2  43704  sprsymrelf1  43707  prproropf1olem4  43717  poprelb  43735  reuopreuprim  43737  fmtnofac2lem  43779  prmdvdsfmtnof1lem2  43796  proththd  43828  opoeALTV  43897  opeoALTV  43898  epoo  43917  evenprm2  43928  gbegt5  43975  sbgoldbaltlem2  43994  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomuspgrlem2d  44045  isomgrsym  44050  isomgrsymb  44051  uspgrsprfo  44072  submgmcl  44110  resmgmhm2b  44116  isassintop  44166  rnghmval  44211  isrngisom  44216  c0snghm  44236  zrrnghm  44237  2zrngamgm  44259  rnghmsubcsetclem2  44296  rhmsubcsetclem2  44342  rhmsubcrngclem1  44347  rhmsubcrngclem2  44348  funcringcsetcALTV2lem9  44364  funcringcsetclem9ALTV  44387  rhmsubclem4  44409  rhmsubcALTVlem4  44427  cbvmpox2  44433  nn0sumltlt  44447  gsumlsscl  44480  ply1mulgsumlem1  44489  lincvalpr  44522  lincdifsn  44528  linc1  44529  lincellss  44530  islinindfiss  44554  islindeps  44557  lincresunit2  44582  islininds2  44588  lmod1zr  44597  ltsubadd2b  44620  zgtp1leeq  44625  logblt1b  44673  blengt1fldiv2p1  44702  nn0sumshdiglemB  44729  line2  44788  itsclc0yqe  44797  itscnhlinecirc02p  44821  setrec2lem2  44846  aacllem  44951