Theorem ralbidv 2861

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 2858	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1872   A.wral 2771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752

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

This theorem is referenced by:  2ralbidv  2866  ralbiiOLD  2939  rexralbidv  2944  raleqbi1dv  3030  raleqbidv  3036  cbvral2v  3062  rspc2  3190  rspc3v  3194  reu6i  3261  reu7  3265  sbcralt  3372  raaan  3907  raaanv  3908  2ralsng  4036  r19.12snOLD  4066  2ralunsn  4208  elintg  4263  elintrabg  4268  eliin  4305  disjprg  4419  disjxun  4421  reusv2lem2  4626  reusv3  4632  poeq1  4777  somo  4808  frirr  4830  fr2nr  4831  frminex  4833  wereu2  4850  posn  4922  frsn  4924  ralxpf  5000  cnvpo  5393  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  7040  wfrlem1  7046  wfrlem3a  7049  wfrlem15  7061  smoeq  7080  tfrlem12  7118  tz7.48lem  7169  elixp2  7537  undifixp  7569  xpf1o  7743  nneneq  7764  ac6sfi  7824  frfi  7825  fipreima  7889  indexfi  7891  marypha1lem  7956  marypha1  7957  supeq1  7968  supeq3  7972  supmo  7975  eqsup  7979  supub  7982  suplub  7983  sup0  7989  supmaxlemOLD  7991  supisoex  7999  eqinf  8009  infval  8011  infmo  8020  oieq1  8036  ordtypecbv  8041  ordtypelem3  8044  ordtypelem6  8047  ordtypelem7  8048  ordtypelem9  8050  wemaplem1  8070  wemaplem2  8071  zfregcl  8118  oemapval  8196  oemapvali  8197  cantnf  8206  wemapwe  8210  rankval3b  8305  unbndrank  8321  rankunb  8329  rankuni2b  8332  tcrank  8363  scottex  8364  scottexs  8366  scott0s  8367  bnd2  8372  dfac8clem  8470  ac5num  8474  acni  8483  acni2  8484  alephval3  8548  dfac4  8560  dfac5lem5  8565  dfac5  8566  dfac2a  8567  dfac2  8568  dfacacn  8578  kmlem2  8588  kmlem13  8599  cflem  8683  cflecard  8690  cfeq0  8693  cfsuc  8694  cfflb  8696  cofsmo  8706  cfsmolem  8707  cfcoflem  8709  coftr  8710  alephsing  8713  fin23lem11  8754  isfin3ds  8766  fin23lem17  8775  fin23lem39  8787  isf33lem  8803  isf34lem6  8817  fin1a2lem13  8849  hsmexlem4  8866  hsmex  8869  axcc2lem  8873  axcc3  8875  dcomex  8884  axdc2lem  8885  axdc3lem2  8888  axdc3lem3  8889  axdc3  8891  axdc4lem  8892  axcclem  8894  zorn2lem2  8934  zorn2lem7  8939  zorn2g  8940  zornn0g  8942  ttukeylem7  8952  axdclem2  8957  brdom3  8963  brdom7disj  8966  brdom6disj  8967  alephval2  9004  inar1  9207  axgroth6  9260  pinq  9359  nqereu  9361  prlem934  9465  supexpr  9486  supsrlem  9542  axpre-sup  9600  dedekind  9804  dedekindle  9805  fimaxre2  10559  fiminre  10562  lbreu  10563  sup2  10572  infm3  10575  supaddc  10581  supadd  10582  supmul1  10583  supmullem2  10585  supmul  10586  infmrclOLD  10600  nnsub  10655  uzwo  11229  nnwof  11232  uzinfmiOLD  11246  ublbneg  11255  lbzbi  11259  zsupss  11260  uzsupss  11263  uzwo3  11266  zmax  11268  rpnnen1lem1  11297  rpnnen1lem2  11298  rpnnen1lem3  11299  rpnnen1lem4  11300  rpnnen1lem5  11301  xrsupsslem  11599  xrinfmsslem  11600  xrsupss  11601  xrinfmss  11602  iccsupr  11734  supicc  11787  supiccub  11788  supicclub  11789  flval2  12055  flval3  12056  fsequb  12194  axdc4uzlem  12201  ssnn0fi  12203  fsuppmapnn0fiubex  12210  faclbnd4lem4  12487  bccl  12513  hashgt12el  12599  hashbc  12620  hashge2el2dif  12641  wrdind  12835  wrd2ind  12836  sqrlem3  13308  rexanre  13409  rexico  13416  cau4  13419  caubnd2  13420  caubnd  13421  clim  13557  rlim  13558  rlim2  13559  rlim2lt  13560  rlim3  13561  clim2  13567  clim2c  13568  clim0c  13570  rlim0  13571  rlim0lt  13572  ello12r  13580  ello1d  13586  lo1bdd2  13587  lo1bddrp  13588  elo12r  13591  rlimconst  13607  rlimresb  13628  rlimcld2  13641  climabs0  13648  rlimcn2  13653  reccn2  13659  cn1lem  13660  rlimo1  13679  o1rlimmul  13681  lo1add  13689  lo1mul  13690  isercoll  13730  caucvgrlem  13735  caucvgrlemOLD  13736  incexclem  13893  climcnds  13908  divrcnv  13909  ruclem12  14292  sqrt2irr  14300  gcdcllem1  14472  gcdcllem2  14473  lcmscllemOLD  14581  lcmsOLD  14583  lcmsledvdsOLD  14584  fissn0dvds  14588  dvdslcmf  14603  lcmfledvds  14604  lcmf  14605  lcmfunsnlem1  14609  lcmfunsnlem2lem1  14610  lcmfunsnlem  14613  lcmfdvds  14614  maxprmfct  14651  reumodprminv  14754  pc2dvds  14827  pcz  14829  prmpwdvds  14847  infpn2  14856  prmreclem1  14859  prmreclem2  14860  prmreclem3  14861  prmreclem5  14863  prmreclem6  14864  vdwlem6  14935  vdwlem8  14937  vdwlem13  14942  vdwnnlem1  14944  vdwnn  14947  ramz  14982  ramcl  14986  prmgaplcmlem1OLD  15011  prmordvdslcmsOLDOLD  15020  cshwrepswhash1  15072  prdsleval  15374  imasval  15410  imasvalOLD  15411  imasaddfnlem  15433  imasvscafn  15442  mrisval  15535  isacs  15556  isacs2  15558  isacs1i  15562  mreacs  15563  acsfn  15564  acsfn2  15568  iscatd  15578  catidex  15579  catideu  15580  cidval  15582  catidd  15585  comfeq  15610  catpropd  15613  ismon  15637  isfunc  15768  isnat  15851  isinito  15894  istermo  15895  isprs  16174  drsdirfi  16182  ispos  16191  lubfval  16223  lubeldm  16226  lubval  16229  lubprop  16231  lublecllem  16233  glbfval  16236  glbeldm  16239  glbval  16242  glbprop  16244  joinval2lem  16253  joinlem  16256  meetval2lem  16267  meetlem  16270  isglbd  16362  lubl  16365  lubun  16368  clatleglb  16371  poslubmo  16391  posglbmo  16392  poslubd  16393  ipodrsima  16410  isdlat  16438  mgm1  16499  mgmidmo  16501  ismgmid  16506  ismgmid2  16509  mgmidsssn0  16511  gsumvalx  16512  gsumress  16518  gsumval2  16522  sgrp1  16533  mndclOLD  16546  mndassOLD  16547  ismndd  16558  mnd1  16576  mnd1OLD  16577  mhmima  16609  mrcmndind  16612  gsumvallem2  16618  gsumwspan  16629  sgrp2rid2  16659  sgrp2rid2ex  16660  sgrp2nmndlem4  16661  isgrpinv  16715  mhmmnd  16807  issubg4  16835  0subg  16841  cycsubgcl  16842  isnsg2  16846  nsgacs  16852  elnmz  16855  ghmrn  16895  ghmnsgima  16905  isga  16944  orbsta  16966  cntzfval  16973  elcntz  16975  resscntz  16984  oppgsubg  17013  symgextfo  17062  gsmsymgreqlem2  17071  gsmsymgreq  17072  pmtrdifel  17120  pmtrdifwrdellem3  17123  pmtrdifwrdel2  17126  psgnunilem2  17135  psgnunilem3  17136  odeq  17198  gexid  17231  gexlem2  17232  gexdvds  17234  gexlem2OLD  17235  isslw  17259  pgpssslw  17265  sylow2alem1  17268  sylow2alem2  17269  efgval  17366  efgrelexlemb  17399  efgcpbllemb  17404  gexex  17490  abl1  17503  dmdprd  17629  dprd2da  17674  pgpfac1lem5  17711  ring1  17829  isabv  18046  islss  18157  lssacs  18189  reslmhm  18274  islbs  18298  pj1lmhm  18322  lbsacsbs  18378  isrrg  18511  opsrval  18697  ply1coe  18888  cply1coe0bi  18893  zringlpir  19056  zringlpirOLD  19057  psgndiflemA  19167  ocvfval  19227  elocv  19229  iunocv  19242  frlmlbs  19353  islindf  19368  islinds2  19369  islindf2  19370  lindfrn  19377  lsslindf  19386  islindf4  19394  mat0dimcrng  19493  mdetunilem1  19635  mdetunilem9  19643  cpmat  19731  cpmatel  19733  1elcpmat  19737  m2cpminvid2lem  19776  chfacffsupp  19878  chfacfscmulfsupp  19881  chfacfpmmulfsupp  19885  basgen2  20003  bastop1  20007  isclo  20101  ordtbaslem  20202  iscn  20249  cnpval  20250  iscnp  20251  iscnp3  20258  lmbr  20272  lmbr2  20273  lmbrf  20274  cnprest  20303  cnprest2  20304  t0sep  20338  isreg  20346  t1sep2  20383  tgcmp  20414  1stcclb  20457  1stcfb  20458  2ndc1stc  20464  1stcrest  20466  2ndcdisj  20469  islly  20481  isnlly  20482  lly1stc  20509  isref  20522  islocfin  20530  elkgen  20549  kgencn  20569  elpt  20585  elptr  20586  ptcnplem  20634  tx1stc  20663  cnmpt21  20684  kqt0lem  20749  isr0  20750  regr1lem2  20753  r0sep  20761  nrmr0reg  20762  flffbas  21008  cnflf  21015  cnflf2  21016  lmflf  21018  txflf  21019  fclsopni  21028  fclsnei  21032  fclsrest  21037  fcfnei  21048  cnfcf  21055  alexsubb  21059  alexsubALTlem3  21062  qustgplem  21133  tsmsfbas  21140  tsmsgsum  21151  tsmsres  21156  tsmsf1o  21157  tsmsxplem1  21165  tsmsxp  21167  ustval  21215  isust  21216  ustincl  21220  ustdiag  21221  ustinvel  21222  ustexhalf  21223  ust0  21232  utopval  21245  ucnval  21290  isucn  21291  isucn2  21292  ucnima  21294  iscfilu  21301  ispsmet  21318  ismet  21336  isxmet  21337  imasdsf1olem  21386  imasf1oxmet  21388  imasf1omet  21389  metss  21521  met1stc  21534  prdsxmslem2  21542  metcnpi3  21559  txmetcnp  21560  metucn  21584  nlmvscn  21688  nrginvrcnlem  21691  nmoval  21718  nmolb  21720  nmovalOLD  21737  nmolbOLD  21739  nghmcn  21764  qtopbaslem  21777  icccmplem2  21839  icccmplem3  21840  reconnlem2  21843  metdscn  21871  metdscnOLD  21886  cncfval  21918  elcncf2  21920  elcncf1di  21925  mulc1cncf  21935  cncfmet  21938  cnllycmp  21982  evth  21985  lebnumlem3  21989  lebnumlem3OLD  21992  lebnum  21993  xlebnum  21994  ishtpy  22001  isphtpy  22010  pi1xfr  22084  pi1coghm  22090  ipcn  22215  lmmbr2  22227  lmmbr3  22228  lmmbrf  22230  cfilfval  22232  iscfil  22233  fmcfil  22240  caufval  22243  iscau  22244  iscau2  22245  iscau3  22246  iscau4  22247  iscauf  22248  caucfil  22251  cfilresi  22263  causs  22266  lmclim  22270  cncmet  22288  cmetcusp1  22318  minveclem4c  22365  minveclem2  22366  minveclem3b  22368  minveclem4  22372  minveclem6  22374  minveclem7  22375  minveclem4cOLD  22377  minveclem2OLD  22378  minveclem3bOLD  22380  minveclem4OLD  22384  minveclem6OLD  22386  minveclem7OLD  22387  ivthlem2  22401  ivthlem3  22402  cniccbdd  22410  ovolunlem1  22448  ovoliunlem1  22453  ovoliun2  22457  ovolicc2lem3  22470  ismbl  22478  ioombl1lem4  22512  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem6  22544  dyadmax  22554  dyadmbllem  22555  dyadmbl  22556  opnmbllem  22557  volcn  22562  ismbf1  22580  ismbf  22584  mbfeqalem  22596  mbfinf  22619  mbfinfOLD  22620  mbflimsup  22621  mbflimsupOLD  22622  itg1climres  22670  mbfi1fseqlem6  22676  mbfi1flimlem  22678  itg2seq  22698  itg2monolem1  22706  itg2i1fseq  22711  itg2i1fseq2  22712  itg2cnlem1  22717  itg2cnlem2  22718  isibl  22721  dveflem  22929  ply1divex  23085  fta1g  23116  plyeq0lem  23162  dgrco  23227  plydivex  23248  fta1  23259  vieta1  23263  aannenlem1  23282  aannenlem2  23283  aalioulem2  23287  aalioulem3  23288  ulmval  23333  ulm2  23338  ulmi  23339  ulmres  23341  ulmshftlem  23342  ulmcaulem  23347  ulmcau  23348  ulmss  23350  ulmbdd  23351  ulmdvlem1  23353  ulmdvlem3  23355  mtestbdd  23358  iblulm  23360  abelthlem8  23392  pilem2  23405  pilem2OLD  23406  pilem3  23407  pilem3OLD  23408  divlogrlim  23578  cxpcn3  23686  dmarea  23881  rlimcnp  23889  cxplim  23895  cxploglim  23901  scvxcvx  23909  emcllem6  23924  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem5  23956  lgambdd  23960  lgamcvglem  23963  ftalem1  23995  ftalem2  23996  ftalem3  23997  isppw2  24040  perfectlem2  24156  2sqlem6  24295  2sqlem10  24300  dchrisumlema  24324  dchrisumlem2  24326  dchrisumlem3  24327  dchrisum0  24356  pntpbnd  24424  pntibndlem3  24428  pntibnd  24429  pntleme  24444  pntlem3  24445  pntlemp  24446  pnt3  24448  istrkgld  24505  axtg5seg  24511  tgcgr4  24574  perpln1  24753  perpln2  24754  isperp  24755  brbtwn2  24933  colinearalg  24938  axsegconlem1  24945  axsegcon  24955  ax5seglem4  24960  ax5seglem5  24961  axlowdim  24989  axeuclidlem  24990  axcontlem1  24992  axcontlem2  24993  axcontlem4  24995  axcontlem5  24996  axcontlem8  24999  axcontlem12  25003  cusgra3v  25190  wlks  25245  wlkcompim  25252  wlkelwrd  25256  wlkntrllem3  25289  constr3trllem2  25377  1conngra  25401  wwlk  25407  clwwlk  25492  isrgrac  25660  rusgra0edg  25681  iseupa  25691  frgrawopreg1  25776  frgrawopreg2  25777  frgrareg  25843  frgraregord013  25844  isgrpo  25922  isgrpo2  25923  isgrpoi  25924  grpoideu  25935  grpoidinv2  25944  isgrp2d  25961  isgrpda  26023  exidu1  26052  cmpidelt  26055  cnid  26077  mulid  26082  ghgrpOLD  26094  isrngod  26105  rngoideu  26110  cnrngo  26129  vci  26165  isvclem  26194  isnvlem  26227  nvi  26231  nmcvcn  26329  lnoval  26391  islno  26392  isblo3i  26440  blo3i  26441  blocnilem  26443  blocni  26444  ajfval  26448  ubthlem1  26510  ubthlem2  26511  ubthlem3  26512  ubth  26513  minvecolem2  26515  minvecolem3  26516  minvecolem4c  26519  minvecolem4  26520  minvecolem5  26521  minvecolem6  26522  minvecolem7  26523  minvecolem2OLD  26525  minvecolem3OLD  26526  minvecolem4cOLD  26529  minvecolem4OLD  26530  minvecolem5OLD  26531  minvecolem6OLD  26532  minvecolem7OLD  26533  htthlem  26568  h2hcau  26630  h2hlm  26631  hilid  26812  hcau  26835  hlimi  26839  hlim2  26843  ocel  26932  adjsym  27484  ellnop  27509  ellnfn  27534  hhcno  27555  hhcnf  27556  0cnop  27630  0cnfn  27631  idcnop  27632  lnopeq  27660  elunop2  27664  lnophm  27670  lnconi  27684  lnopcnbd  27687  lnfncnbd  27708  imaelshi  27709  riesz3i  27713  riesz4i  27714  riesz4  27715  riesz1  27716  cnlnadjlem2  27719  cnlnadjlem5  27722  cnlnadjlem8  27725  cnlnadji  27727  nmopadjlei  27739  cnvbraval  27761  leopg  27773  leoppos  27777  mdbr  27945  dmdbr  27950  cdj3i  28092  rmoeqALT  28121  disjunsn  28206  funcnv5mpt  28274  fgreu  28276  fcnvgreu  28277  xrge0infss  28346  xrge0infssOLD  28347  resspos  28427  isomnd  28471  inftmrel  28504  isinftm  28505  archiabl  28522  rngurd  28559  isarchiofld  28588  crefeq  28680  rge0scvg  28763  qqhcn  28803  esumpcvgval  28907  esum2d  28922  sigaval  28940  issgon  28953  isrnmeas  29030  ismbfm  29082  isanmbfm  29086  mbfmcst  29089  elcarsg  29145  sitgval  29173  oddpwdc  29195  eulerpartlemd  29207  ballotleme  29337  signsw0g  29453  signswmnd  29454  bnj1185  29613  bnj1385  29652  bnj66  29679  bnj106  29687  bnj155  29698  bnj852  29740  bnj893  29747  bnj1228  29828  bnj1234  29830  bnj1463  29872  derangenlem  29902  subfacp1lem3  29913  subfacp1lem5  29915  subfacp1lem6  29916  subfacp1  29917  erdszelem8  29929  kur14  29947  cnpcon  29961  rescon  29977  cvmscbv  29989  iscvm  29990  cvmsi  29996  cvmsval  29997  cvmlift3lem2  30051  snmlval  30062  mclsssvlem  30208  mclsval  30209  mclsax  30215  mclsind  30216  ghomgrpilem1  30311  dfpo2  30402  dfon2lem9  30444  dfrdg2  30449  dfrdg3  30450  poseq  30498  soseq  30499  frrlem1  30521  sltval  30541  nocvxminlem  30584  nobndlem2  30587  nobndlem8  30593  nobndup  30594  nobnddown  30595  fwddifnval  30935  nn0prpwlem  30983  isfne  31000  isfne4  31001  isfne2  31003  isfne3  31004  neibastop3  31023  topmeet  31025  topjoin  31026  filnetlem4  31042  taupilemrplb  31685  csbwrecsg  31692  fin2so  31896  ptrecube  31904  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem28  31932  poimirlem29  31933  poimirlem30  31934  poimirlem32  31936  poimir  31937  heicant  31939  mblfinlem1  31941  mblfinlem2  31942  mblfinlem3  31943  ismblfin  31945  voliunnfl  31948  volsupnfl  31949  mbfresfi  31951  itg2addnc  31960  ftc1anc  31989  f1opr  32015  upixp  32020  indexdom  32025  filbcmb  32031  sdclem2  32035  fdc  32038  lmclim2  32051  caures  32053  istotbnd  32065  istotbnd3  32067  sstotbnd  32071  isbnd  32076  heibor  32117  bfp  32120  rrncmslem  32128  exidres  32140  exidresid  32141  idlval  32210  isidl  32211  0idl  32222  unichnidl  32228  pridl  32234  ismaxidl  32237  smprngopr  32249  igenval2  32263  prnc  32264  ispridlc  32267  scottexf  32375  scott0f  32376  riotasvd  32497  islfl  32595  eqlkr  32634  eqlkr3  32636  glbconN  32911  hlsuprexch  32915  ispsubsp  33279  ldilset  33643  isldil  33644  dilsetN  33688  isdilN  33689  trlset  33696  trlval  33697  cdleme27b  33904  cdleme29b  33911  cdleme31so  33915  cdleme31sn1  33917  cdleme31sn1c  33924  cdleme31fv  33926  cdleme40v  34005  istendo  34296  cdlemkid3N  34469  cdlemkid4  34470  cdlemkid5  34471  dihfval  34768  dihval  34769  islpolN  35020  hdmapffval  35366  hdmapfval  35367  hdmapval  35368  hdmapval2lem  35371  hgmapffval  35425  hgmapfval  35426  hgmapval  35427  hgmapvs  35431  isnacs  35515  isnacs2  35517  nacsfix  35523  mzpclval  35536  elmzpcl  35537  rencldnfilem  35632  infmrgelbi  35694  infmrgelbiOLD  35695  pellfundre  35699  pellfundlb  35702  wepwsolem  35870  fnwe2lem2  35879  aomclem8  35889  dfac11  35890  gicabl  35927  islnr3  35944  hbtlem2  35953  hbtlem5  35957  fiinfi  36147  imo72b2lem0  36578  imo72b2lem2  36580  imo72b2lem1  36584  imo72b2  36589  evth2f  37309  ubelsupr  37314  evthf  37321  fnchoice  37323  uzwo4  37365  wessf1ornlem  37420  disjinfi  37429  dstregt0  37445  upbdrech2  37480  mccl  37618  mullimc  37636  ellimcabssub0  37637  limcdm0  37638  climf  37642  mullimcf  37643  constlimc  37644  idlimc  37646  clim2f  37656  limsupre  37661  limsupreOLD  37662  limcleqr  37665  addlimc  37669  0ellimcdiv  37670  clim2cf  37671  clim0cf  37675  cncfshift  37691  cncfperiod  37696  fperdvper  37730  dvdivbd  37735  dvbdfbdioo  37742  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnprodlem3  37763  stoweidlem5  37805  stoweidlem9  37809  stoweidlem15  37815  stoweidlem16  37816  stoweidlem27  37827  stoweidlem28  37828  stoweidlem31  37832  stoweidlem34  37835  stoweidlem37  37838  stoweidlem46  37847  stoweidlem48  37849  stoweidlem51  37852  stoweidlem52  37853  stoweidlem59  37860  wallispilem3  37869  stirlinglem13  37888  fourierdlem2  37911  fourierdlem3  37912  fourierdlem16  37925  fourierdlem20  37929  fourierdlem21  37930  fourierdlem22  37931  fourierdlem25  37934  fourierdlem39  37949  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem54  37964  fourierdlem64  37974  fourierdlem77  37987  fourierdlem83  37993  fourierdlem87  37997  fourierdlem103  38013  fourierdlem104  38014  issal  38096  sge0supre  38139  sge0rnbnd  38143  ismea  38197  iundjiun  38206  caragenval  38222  isome  38223  caragenel  38224  omessle  38227  ovnlerp  38288  hoidmvlelem1  38321  hoidmvlelem3  38323  hoidmvlelem4  38324  hoidmvle  38326  cbvral2  38464  raaan2  38467  2reu4a  38481  dfdfat2  38503  iccpart  38600  iccpartigtl  38607  perfectALTVlem2  38714  bgoldbachlt  38776  tgoldbachlt  38779  issn  38861  uvtxa01vtx0  39228  uvtxusgr  39234  iscusgredg  39248  mgmhmima  39422  rnghmval  39511  lidlmsgrp  39546  lidlrng  39547  zlidlring  39548  uzlidlring  39549  2zrngamnd  39561  ply1mulgsumlem1  39800  ply1mulgsumlem2  39801  linindslinci  39863  lindslinindsimp1  39872  lindslinindsimp2lem5  39877  lindslinindsimp2  39878  linds0  39880  lindsrng01  39883  snlindsntor  39886  lmod1  39907  ldepsnlinc  39923  bigoval  39982  elbigo2r  39986  nn0sumshdiglem2  40055