Theorem ralbidv 2871

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
ralbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 466	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ralbidva 2868	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1870   A.wral 2782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2787

This theorem is referenced by:  2ralbidv  2876  ralbiiOLD  2949  rexralbidv  2954  raleqbi1dv  3040  raleqbidv  3046  cbvral2v  3070  rspc2  3196  rspc3v  3200  reu6i  3268  reu7  3272  sbcralt  3378  raaan  3911  raaanv  3912  2ralsng  4039  r19.12snOLD  4069  2ralunsn  4211  elintg  4266  elintrabg  4271  eliin  4308  disjprg  4422  disjxun  4424  reusv2lem2  4627  reusv3  4633  poeq1  4778  somo  4809  frirr  4831  fr2nr  4832  frminex  4834  wereu2  4851  posn  4923  frsn  4925  ralxpf  5001  cnvpo  5394  fnmptfvd  6000  iinpreima  6025  dff4  6051  dff13f  6175  eusvobj2  6298  ofreq  6548  sorpssuni  6594  sorpssint  6595  fr3nr  6620  onssmin  6638  funcnvuni  6760  f1oweALT  6791  frxp  6917  wrecseq123  7037  wfrlem1  7043  wfrlem3a  7046  wfrlem15  7058  smoeq  7077  tfrlem12  7115  tz7.48lem  7166  elixp2  7534  undifixp  7566  xpf1o  7740  nneneq  7761  ac6sfi  7821  frfi  7822  fipreima  7886  indexfi  7888  marypha1lem  7953  marypha1  7954  supeq1  7965  supeq3  7969  supmo  7972  eqsup  7976  supub  7979  suplub  7980  sup0  7986  supmaxlemOLD  7988  supisoex  7996  eqinf  8006  infval  8008  oieq1  8027  ordtypecbv  8032  ordtypelem3  8035  ordtypelem6  8038  ordtypelem7  8039  ordtypelem9  8041  wemaplem1  8061  wemaplem2  8062  zfregcl  8109  oemapval  8187  oemapvali  8188  cantnf  8197  wemapwe  8201  rankval3b  8296  unbndrank  8312  rankunb  8320  rankuni2b  8323  tcrank  8354  scottex  8355  scottexs  8357  scott0s  8358  bnd2  8363  dfac8clem  8461  ac5num  8465  acni  8474  acni2  8475  alephval3  8539  dfac4  8551  dfac5lem5  8556  dfac5  8557  dfac2a  8558  dfac2  8559  dfacacn  8569  kmlem2  8579  kmlem13  8590  cflem  8674  cflecard  8681  cfeq0  8684  cfsuc  8685  cfflb  8687  cofsmo  8697  cfsmolem  8698  cfcoflem  8700  coftr  8701  alephsing  8704  fin23lem11  8745  isfin3ds  8757  fin23lem17  8766  fin23lem39  8778  isf33lem  8794  isf34lem6  8808  fin1a2lem13  8840  hsmexlem4  8857  hsmex  8860  axcc2lem  8864  axcc3  8866  dcomex  8875  axdc2lem  8876  axdc3lem2  8879  axdc3lem3  8880  axdc3  8882  axdc4lem  8883  axcclem  8885  zorn2lem2  8925  zorn2lem7  8930  zorn2g  8931  zornn0g  8933  ttukeylem7  8943  axdclem2  8948  brdom3  8954  brdom7disj  8957  brdom6disj  8958  alephval2  8995  inar1  9199  axgroth6  9252  pinq  9351  nqereu  9353  prlem934  9457  supexpr  9478  supsrlem  9534  axpre-sup  9592  dedekind  9796  dedekindle  9797  fimaxre2  10552  fiminre  10555  lbreu  10556  sup2  10565  infm3  10568  supaddc  10574  supadd  10575  supmul1  10576  supmullem2  10578  supmul  10579  infmrclOLD  10593  nnsub  10648  uzwo  11222  nnwof  11225  uzinfmiOLD  11239  ublbneg  11248  lbzbi  11252  zsupss  11253  uzsupss  11256  uzwo3  11259  zmax  11261  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem4  11293  rpnnen1lem5  11294  xrsupsslem  11592  xrinfmsslem  11593  xrsupss  11594  xrinfmss  11595  iccsupr  11727  supicc  11778  supiccub  11779  supicclub  11780  flval2  12046  flval3  12047  fsequb  12185  axdc4uzlem  12192  ssnn0fi  12194  fsuppmapnn0fiubex  12201  faclbnd4lem4  12478  bccl  12504  hashgt12el  12590  hashbc  12611  hashge2el2dif  12630  wrdind  12818  wrd2ind  12819  sqrlem3  13287  rexanre  13388  rexico  13395  cau4  13398  caubnd2  13399  caubnd  13400  clim  13536  rlim  13537  rlim2  13538  rlim2lt  13539  rlim3  13540  clim2  13546  clim2c  13547  clim0c  13549  rlim0  13550  rlim0lt  13551  ello12r  13559  ello1d  13565  lo1bdd2  13566  lo1bddrp  13567  elo12r  13570  rlimconst  13586  rlimresb  13607  rlimcld2  13620  climabs0  13627  rlimcn2  13632  reccn2  13638  cn1lem  13639  rlimo1  13658  o1rlimmul  13660  lo1add  13668  lo1mul  13669  isercoll  13709  caucvgrlem  13714  caucvgrlemOLD  13715  incexclem  13872  climcnds  13887  divrcnv  13888  ruclem12  14271  sqrt2irr  14279  gcdcllem1  14447  gcdcllem2  14448  lcmscllemOLD  14547  lcmsOLD  14549  lcmsledvdsOLD  14550  fissn0dvds  14554  dvdslcmf  14566  lcmfledvds  14567  lcmf  14568  lcmfunsnlem1  14572  lcmfunsnlem2lem1  14573  lcmfunsnlem  14576  lcmfdvds  14577  maxprmfct  14614  reumodprminv  14709  pc2dvds  14782  pcz  14784  prmpwdvds  14802  infpn2  14811  prmreclem1  14814  prmreclem2  14815  prmreclem3  14816  prmreclem5  14818  prmreclem6  14819  vdwlem6  14890  vdwlem8  14892  vdwlem13  14897  vdwnnlem1  14899  vdwnn  14902  ramz  14937  ramcl  14941  prmgaplcmlem1OLD  14966  prmordvdslcmsOLDOLD  14975  cshwrepswhash1  15027  prdsleval  15325  imasval  15359  imasaddfnlem  15376  imasvscafn  15385  mrisval  15478  isacs  15499  isacs2  15501  isacs1i  15505  mreacs  15506  acsfn  15507  acsfn2  15511  iscatd  15521  catidex  15522  catideu  15523  cidval  15525  catidd  15528  comfeq  15553  catpropd  15556  ismon  15580  isfunc  15711  isnat  15794  isinito  15837  istermo  15838  isprs  16117  drsdirfi  16125  ispos  16134  lubfval  16166  lubeldm  16169  lubval  16172  lubprop  16174  lublecllem  16176  glbfval  16179  glbeldm  16182  glbval  16185  glbprop  16187  joinval2lem  16196  joinlem  16199  meetval2lem  16210  meetlem  16213  isglbd  16305  lubl  16308  lubun  16311  clatleglb  16314  poslubmo  16334  posglbmo  16335  poslubd  16336  ipodrsima  16353  isdlat  16381  mgm1  16442  mgmidmo  16444  ismgmid  16449  ismgmid2  16452  mgmidsssn0  16454  gsumvalx  16455  gsumress  16461  gsumval2  16465  sgrp1  16476  mndclOLD  16489  mndassOLD  16490  ismndd  16501  mnd1  16519  mnd1OLD  16520  mhmima  16552  mrcmndind  16555  gsumvallem2  16561  gsumwspan  16572  sgrp2rid2  16602  sgrp2rid2ex  16603  sgrp2nmndlem4  16604  isgrpinv  16658  mhmmnd  16750  issubg4  16778  0subg  16784  cycsubgcl  16785  isnsg2  16789  nsgacs  16795  elnmz  16798  ghmrn  16838  ghmnsgima  16848  isga  16887  orbsta  16909  cntzfval  16916  elcntz  16918  resscntz  16927  oppgsubg  16956  symgextfo  17005  gsmsymgreqlem2  17014  gsmsymgreq  17015  pmtrdifel  17063  pmtrdifwrdellem3  17066  pmtrdifwrdel2  17069  psgnunilem2  17078  psgnunilem3  17079  odeq  17132  gexid  17159  gexlem2  17160  gexdvds  17162  isslw  17186  pgpssslw  17192  sylow2alem1  17195  sylow2alem2  17196  efgval  17293  efgrelexlemb  17326  efgcpbllemb  17331  gexex  17417  abl1  17430  dmdprd  17556  dprd2da  17601  pgpfac1lem5  17638  ring1  17756  isabv  17973  islss  18084  lssacs  18116  reslmhm  18201  islbs  18225  pj1lmhm  18249  lbsacsbs  18305  isrrg  18438  opsrval  18624  ply1coe  18815  cply1coe0bi  18820  zringlpir  18981  psgndiflemA  19091  ocvfval  19151  elocv  19153  iunocv  19166  frlmlbs  19277  islindf  19292  islinds2  19293  islindf2  19294  lindfrn  19301  lsslindf  19310  islindf4  19318  mat0dimcrng  19417  mdetunilem1  19559  mdetunilem9  19567  cpmat  19655  cpmatel  19657  1elcpmat  19661  m2cpminvid2lem  19700  chfacffsupp  19802  chfacfscmulfsupp  19805  chfacfpmmulfsupp  19809  basgen2  19927  bastop1  19931  isclo  20025  ordtbaslem  20126  iscn  20173  cnpval  20174  iscnp  20175  iscnp3  20182  lmbr  20196  lmbr2  20197  lmbrf  20198  cnprest  20227  cnprest2  20228  t0sep  20262  isreg  20270  t1sep2  20307  tgcmp  20338  1stcclb  20381  1stcfb  20382  2ndc1stc  20388  1stcrest  20390  2ndcdisj  20393  islly  20405  isnlly  20406  lly1stc  20433  isref  20446  islocfin  20454  elkgen  20473  kgencn  20493  elpt  20509  elptr  20510  ptcnplem  20558  tx1stc  20587  cnmpt21  20608  kqt0lem  20673  isr0  20674  regr1lem2  20677  r0sep  20685  nrmr0reg  20686  flffbas  20932  cnflf  20939  cnflf2  20940  lmflf  20942  txflf  20943  fclsopni  20952  fclsnei  20956  fclsrest  20961  fcfnei  20972  cnfcf  20979  alexsubb  20983  alexsubALTlem3  20986  qustgplem  21057  tsmsfbas  21064  tsmsgsum  21075  tsmsres  21080  tsmsf1o  21081  tsmsxplem1  21089  tsmsxp  21091  ustval  21139  isust  21140  ustincl  21144  ustdiag  21145  ustinvel  21146  ustexhalf  21147  ust0  21156  utopval  21169  ucnval  21214  isucn  21215  isucn2  21216  ucnima  21218  iscfilu  21225  ispsmet  21242  ismet  21260  isxmet  21261  imasdsf1olem  21310  imasf1oxmet  21312  imasf1omet  21313  metss  21445  met1stc  21458  prdsxmslem2  21466  metcnpi3  21483  txmetcnp  21484  metucn  21508  nlmvscn  21612  nrginvrcnlem  21615  nmoval  21638  nmolb  21640  nghmcn  21668  qtopbaslem  21681  icccmplem2  21743  icccmplem3  21744  reconnlem2  21747  metdscn  21775  cncfval  21807  elcncf2  21809  elcncf1di  21814  mulc1cncf  21824  cncfmet  21827  cnllycmp  21871  evth  21874  lebnumlem3  21878  lebnum  21879  xlebnum  21880  ishtpy  21887  isphtpy  21896  pi1xfr  21970  pi1coghm  21976  ipcn  22101  lmmbr2  22113  lmmbr3  22114  lmmbrf  22116  cfilfval  22118  iscfil  22119  fmcfil  22126  caufval  22129  iscau  22130  iscau2  22131  iscau3  22132  iscau4  22133  iscauf  22134  caucfil  22137  cfilresi  22149  causs  22152  lmclim  22156  cncmet  22174  cmetcusp1  22204  minveclem4c  22251  minveclem2  22252  minveclem3b  22254  minveclem4  22258  minveclem6  22260  minveclem7  22261  ivthlem2  22275  ivthlem3  22276  cniccbdd  22284  ovolunlem1  22319  ovoliunlem1  22324  ovoliun2  22328  ovolicc2lem3  22341  ismbl  22348  ioombl1lem4  22382  uniioombllem2  22408  uniioombllem2OLD  22409  uniioombllem6  22414  dyadmax  22424  dyadmbllem  22425  dyadmbl  22426  opnmbllem  22427  volcn  22432  ismbf1  22450  ismbf  22454  mbfeqalem  22466  mbfinf  22489  mbfinfOLD  22490  mbflimsup  22491  mbflimsupOLD  22492  itg1climres  22540  mbfi1fseqlem6  22546  mbfi1flimlem  22548  itg2seq  22568  itg2monolem1  22576  itg2i1fseq  22581  itg2i1fseq2  22582  itg2cnlem1  22587  itg2cnlem2  22588  isibl  22591  dveflem  22799  ply1divex  22953  fta1g  22984  plyeq0lem  23023  dgrco  23088  plydivex  23109  fta1  23120  vieta1  23124  aannenlem1  23140  aannenlem2  23141  aalioulem2  23145  aalioulem3  23146  ulmval  23191  ulm2  23196  ulmi  23197  ulmres  23199  ulmshftlem  23200  ulmcaulem  23205  ulmcau  23206  ulmss  23208  ulmbdd  23209  ulmdvlem1  23211  ulmdvlem3  23213  mtestbdd  23216  iblulm  23218  abelthlem8  23250  pilem2  23263  pilem2OLD  23264  pilem3  23265  pilem3OLD  23266  divlogrlim  23436  cxpcn3  23544  dmarea  23739  rlimcnp  23747  cxplim  23753  cxploglim  23759  scvxcvx  23767  emcllem6  23782  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem5  23814  lgambdd  23818  lgamcvglem  23821  ftalem1  23853  ftalem2  23854  ftalem3  23855  isppw2  23896  perfectlem2  24012  2sqlem6  24151  2sqlem10  24156  dchrisumlema  24180  dchrisumlem2  24182  dchrisumlem3  24183  dchrisum0  24212  pntpbnd  24280  pntibndlem3  24284  pntibnd  24285  pntleme  24300  pntlem3  24301  pntlemp  24302  pnt3  24304  istrkgld  24361  axtg5seg  24367  perpln1  24603  perpln2  24604  isperp  24605  brbtwn2  24772  colinearalg  24777  axsegconlem1  24784  axsegcon  24794  ax5seglem4  24799  ax5seglem5  24800  axlowdim  24828  axeuclidlem  24829  axcontlem1  24831  axcontlem2  24832  axcontlem4  24834  axcontlem5  24835  axcontlem8  24838  axcontlem12  24842  cusgra3v  25028  wlks  25083  wlkcompim  25090  wlkelwrd  25094  wlkntrllem3  25127  constr3trllem2  25215  1conngra  25239  wwlk  25245  clwwlk  25330  isrgrac  25498  rusgra0edg  25519  iseupa  25529  frgrawopreg1  25614  frgrawopreg2  25615  frgrareg  25681  frgraregord013  25682  isgrpo  25760  isgrpo2  25761  isgrpoi  25762  grpoideu  25773  grpoidinv2  25782  isgrp2d  25799  isgrpda  25861  exidu1  25890  cmpidelt  25893  cnid  25915  mulid  25920  ghgrpOLD  25932  isrngod  25943  rngoideu  25948  cnrngo  25967  vci  26003  isvclem  26032  isnvlem  26065  nvi  26069  nmcvcn  26167  lnoval  26229  islno  26230  isblo3i  26278  blo3i  26279  blocnilem  26281  blocni  26282  ajfval  26286  ubthlem1  26348  ubthlem2  26349  ubthlem3  26350  ubth  26351  minvecolem2  26353  minvecolem3  26354  minvecolem4c  26357  minvecolem4  26358  minvecolem5  26359  minvecolem6  26360  minvecolem7  26361  htthlem  26396  h2hcau  26458  h2hlm  26459  hilid  26640  hcau  26663  hlimi  26667  hlim2  26671  ocel  26760  adjsym  27312  ellnop  27337  ellnfn  27362  hhcno  27383  hhcnf  27384  0cnop  27458  0cnfn  27459  idcnop  27460  lnopeq  27488  elunop2  27492  lnophm  27498  lnconi  27512  lnopcnbd  27515  lnfncnbd  27536  imaelshi  27537  riesz3i  27541  riesz4i  27542  riesz4  27543  riesz1  27544  cnlnadjlem2  27547  cnlnadjlem5  27550  cnlnadjlem8  27553  cnlnadji  27555  nmopadjlei  27567  cnvbraval  27589  leopg  27601  leoppos  27605  mdbr  27773  dmdbr  27778  cdj3i  27920  rmoeq  27949  disjunsn  28034  funcnv5mpt  28103  fgreu  28105  fcnvgreu  28106  xrge0infss  28172  resspos  28249  isomnd  28293  inftmrel  28326  isinftm  28327  archiabl  28344  rngurd  28381  isarchiofld  28410  crefeq  28502  rge0scvg  28585  qqhcn  28625  esumpcvgval  28729  esum2d  28744  sigaval  28762  issgon  28775  isrnmeas  28852  ismbfm  28904  isanmbfm  28908  mbfmcst  28911  elcarsg  28957  sitgval  28984  oddpwdc  29004  eulerpartlemd  29016  ballotleme  29146  signsw0g  29224  signswmnd  29225  bnj1185  29384  bnj1385  29423  bnj66  29450  bnj106  29458  bnj155  29469  bnj852  29511  bnj893  29518  bnj1228  29599  bnj1234  29601  bnj1463  29643  derangenlem  29673  subfacp1lem3  29684  subfacp1lem5  29686  subfacp1lem6  29687  subfacp1  29688  erdszelem8  29700  kur14  29718  cnpcon  29732  rescon  29748  cvmscbv  29760  iscvm  29761  cvmsi  29767  cvmsval  29768  cvmlift3lem2  29822  snmlval  29833  mclsssvlem  29979  mclsval  29980  mclsax  29986  mclsind  29987  ghomgrpilem1  30082  dfpo2  30173  dfon2lem9  30215  dfrdg2  30220  dfrdg3  30221  poseq  30269  soseq  30270  frrlem1  30292  sltval  30312  nocvxminlem  30355  nobndlem2  30358  nobndlem8  30364  nobndup  30365  nobnddown  30366  fwddifnval  30706  nn0prpwlem  30754  isfne  30771  isfne4  30772  isfne2  30774  isfne3  30775  neibastop3  30794  topmeet  30796  topjoin  30797  filnetlem4  30813  taupilemrplb  31457  fin2so  31626  ptrecube  31634  poimirlem2  31636  poimirlem3  31637  poimirlem4  31638  poimirlem24  31658  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  poimirlem29  31663  poimirlem30  31664  poimirlem32  31666  poimir  31667  heicant  31669  mblfinlem1  31671  mblfinlem2  31672  mblfinlem3  31673  ismblfin  31675  voliunnfl  31678  volsupnfl  31679  mbfresfi  31681  itg2addnc  31690  ftc1anc  31719  f1opr  31745  upixp  31750  indexdom  31755  filbcmb  31761  sdclem2  31765  fdc  31768  lmclim2  31781  caures  31783  istotbnd  31795  istotbnd3  31797  sstotbnd  31801  isbnd  31806  heibor  31847  bfp  31850  rrncmslem  31858  exidres  31870  exidresid  31871  idlval  31940  isidl  31941  0idl  31952  unichnidl  31958  pridl  31964  ismaxidl  31967  smprngopr  31979  igenval2  31993  prnc  31994  ispridlc  31997  scottexf  32105  scott0f  32106  riotasvd  32227  islfl  32325  eqlkr  32364  eqlkr3  32366  glbconN  32641  hlsuprexch  32645  ispsubsp  33009  ldilset  33373  isldil  33374  dilsetN  33418  isdilN  33419  trlset  33426  trlval  33427  cdleme27b  33634  cdleme29b  33641  cdleme31so  33645  cdleme31sn1  33647  cdleme31sn1c  33654  cdleme31fv  33656  cdleme40v  33735  istendo  34026  cdlemkid3N  34199  cdlemkid4  34200  cdlemkid5  34201  dihfval  34498  dihval  34499  islpolN  34750  hdmapffval  35096  hdmapfval  35097  hdmapval  35098  hdmapval2lem  35101  hgmapffval  35155  hgmapfval  35156  hgmapval  35157  hgmapvs  35161  isnacs  35245  isnacs2  35247  nacsfix  35253  mzpclval  35266  elmzpcl  35267  rencldnfilem  35362  infmrgelbi  35422  pellfundre  35425  pellfundlb  35428  wepwsolem  35596  fnwe2lem2  35605  aomclem8  35615  dfac11  35616  gicabl  35653  islnr3  35670  hbtlem2  35679  hbtlem5  35683  fiinfi  35866  imo72b2lem0  36235  imo72b2lem2  36237  imo72b2lem1  36241  imo72b2  36246  evth2f  36966  ubelsupr  36971  evthf  36978  fnchoice  36980  uzwo4  37023  wessf1ornlem  37072  disjinfi  37081  dstregt0  37090  upbdrech2  37125  mccl  37240  mullimc  37258  ellimcabssub0  37259  limcdm0  37260  climf  37264  mullimcf  37265  constlimc  37266  idlimc  37268  clim2f  37278  limsupre  37283  limsupreOLD  37284  limcleqr  37287  addlimc  37291  0ellimcdiv  37292  clim2cf  37293  clim0cf  37297  cncfshift  37313  cncfperiod  37318  fperdvper  37352  dvdivbd  37357  dvbdfbdioo  37364  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvnprodlem3  37382  stoweidlem5  37424  stoweidlem9  37428  stoweidlem15  37434  stoweidlem16  37435  stoweidlem27  37446  stoweidlem28  37447  stoweidlem31  37451  stoweidlem34  37454  stoweidlem37  37457  stoweidlem46  37466  stoweidlem48  37468  stoweidlem51  37471  stoweidlem52  37472  stoweidlem59  37479  wallispilem3  37488  stirlinglem13  37507  fourierdlem2  37530  fourierdlem3  37531  fourierdlem16  37544  fourierdlem20  37548  fourierdlem21  37549  fourierdlem22  37550  fourierdlem25  37553  fourierdlem39  37567  fourierdlem42  37570  fourierdlem54  37582  fourierdlem64  37592  fourierdlem77  37605  fourierdlem83  37611  fourierdlem87  37615  fourierdlem103  37631  fourierdlem104  37632  issal  37712  sge0supre  37755  sge0rnbnd  37759  ismea  37788  iundjiun  37797  caragenval  37813  isome  37814  caragenel  37815  omessle  37818  cbvral2  37974  raaan2  37977  2reu4a  37991  dfdfat2  38013  iccpart  38110  iccpartigtl  38117  perfectALTVlem2  38224  bgoldbachlt  38286  tgoldbachlt  38289  mgmhmima  38550  rnghmval  38639  lidlmsgrp  38674  lidlrng  38675  zlidlring  38676  uzlidlring  38677  2zrngamnd  38689  ply1mulgsumlem1  38928  ply1mulgsumlem2  38929  linindslinci  38991  lindslinindsimp1  39000  lindslinindsimp2lem5  39005  lindslinindsimp2  39006  linds0  39008  lindsrng01  39011  snlindsntor  39014  lmod1  39035  ldepsnlinc  39051  bigoval  39111  elbigo2r  39115  nn0sumshdiglem2  39184