Theorem biimpi 219

Description: Infer an implication from a logical equivalence. Inference associated with biimp 218. (Contributed by NM, 29-Dec-1992.)

Hypothesis

Ref	Expression
biimpi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpi	⊢ (𝜑 → 𝜓)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		biimp 218	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sylbi  220  sylib  221  sylbb  222  biimpri  231  mpbi  233  biimtrid  245  imbitrdi  254  syl7bi  258  syl8ib  259  simplbi  501  simprbi  502  birani  508  bilani  509  anc2l  562  sylanb  592  sylanblc  600  sylan2b  605  pm3.37  819  pm2.53  864  orbi2i  925  pm2.32  936  pm2.76  944  pm3.1  1007  pm5.15  1028  pm5.16  1029  4exmid  1065  simp1bi  1161  simp2bi  1162  simp3bi  1163  syl3an1b  1428  syl3an2b  1429  syl3an3b  1430  nic-ax  1700  nfnt  1883  19.25  1907  nfimd  1921  19.37imv  1974  alcomimw  2070  sbbii  2116  nsb  2147  excomim  2204  stdpc5  2250  sb9i  2558  mo4  2600  2mo  2682  ax9ALT  2764  eleq2w2  2765  eqeq1d  2771  r19.37v  3197  rmoeq1  3407  elabgt  3640  euind  3696  reuind  3725  sbcimdv  3821  sbcg  3825  ra4v  3847  ra4  3848  csbied  3897  ssrmof  4013  elunnel1  4116  elunnel2  4117  unssd  4153  n0moeu  4322  eqeuel  4328  ss0  4366  iftrueb  4505  elinsn  4681  disjtp2  4687  rabsnif  4694  prprc  4738  elpwdifsn  4761  ssunsn2  4797  preqr1  4817  intss2  5078  disjxiun  5110  unisn2  5277  snexALT  5355  reusv3i  5376  snexOLD  5414  pocl  5578  brrelex12  5714  0nelrel0  5722  elrel  5785  exopxfr2  5831  dmxp  5920  xpssres  6018  elinxp  6019  imadisjlnd  6084  elimasni  6094  inisegn0  6101  xpdifid  6166  xpdifcnvepel  6167  imadifssranOLD  6204  dmsnsnsn  6222  relcnvtrg  6269  xpco  6291  reuop  6295  predprc  6340  sucprc  6440  onunel  6469  iotaint  6515  iotanul  6517  funun  6583  funcnv3  6607  funimass1  6619  funssxp  6735  f0dom0  6763  dffv3  6878  dffv2  6977  fsneq  7031  fndmin  7041  sspreima  7064  iinpreima  7065  fveqressseq  7075  fsn2  7133  f1ounsn  7271  f12dfv  7272  f13dfv  7273  isoselem  7340  oprabidw  7442  oprabid  7443  ovima0  7590  sorpsscmpl  7732  unexgOLD  7748  abnex  7756  pwuncl  7769  ordsuci  7807  peano2  7886  1stval  7988  2ndval  7989  1stdm  8037  oprabco  8091  f1o2ndf1  8117  poxp  8124  frxp3  8147  suppval1  8162  fnsuppeq0  8188  frrlem4  8286  tz7.48lem  8428  tz7.49c  8433  ord1eln01  8481  ord2eln012  8482  undifixp  8932  bren2  8980  ensym  9000  en1uniel  9026  domunsn  9115  limenpsi  9140  findcard2  9149  unfi  9155  pwssfi  9161  php4  9194  isinf  9225  en2  9240  fiint  9286  rneqdmfinf1o  9290  elfiun  9390  marypha1lem  9393  supval2  9415  eqinf  9445  brwdom2  9535  zfreg  9558  tcmin  9708  frmin  9721  prwf  9783  r1pw  9817  rankuni2b  9825  rankr1id  9834  djuun  9912  cardval3  9938  ficardom  9947  cardmin2  9985  isinfcard  10076  iscard3  10077  alephval3  10094  dfac9  10120  kmlem6  10139  fin23lem29  10325  fin23lem30  10326  isf32lem11  10347  isfin1-3  10370  fin45  10376  fin1a2lem12  10395  fin1a2lem13  10396  axcc2lem  10420  dominf  10429  axdc4lem  10439  dominfac  10558  pwcfsdom  10568  cfpwsdom  10569  tskuni  10768  wfgru  10801  rpregt0  13031  supxrun  13342  elicore  13425  xrge0nre  13480  elfz1end  13582  elfzonlteqm1  13770  modfzo0difsn  13979  fzennn  14004  cardfz  14006  fsuppmapnn0fiub0  14029  ser0  14090  crreczi  14264  faclbnd  14326  bcn1  14349  hashrabsn01  14409  hashge0  14423  prsshashgt1  14447  hashssdif  14449  hashdifpr  14452  hashsn01  14453  hashgt23el  14461  hashpw  14473  hashres  14475  hash3tpexb  14531  ccatw2s1p1  14674  swrdswrd  14742  swrdccatin2  14766  pfxccatpfx1  14773  repsundef  14808  trclublem  15032  reltrclfv  15054  dmtrclfv  15055  cau3lem  15406  harmonic  15913  mertenslem2  15939  prodf1  15945  fprodfac  16027  rpnnen2lem12  16281  sqrt2irr0  16307  lcmftp  16694  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  prmind2  16743  prm2orodd  16749  pceq0  16931  prmreclem6  16981  0ram  17080  ram0  17082  cshwsiun  17159  ressbas2  17298  ressinbas  17305  ressval3d  17306  catpropd  17765  initoid  18058  termoid  18059  initoeu2lem0  18070  arwhoma  18102  joinfval  18427  meetfval  18441  lubun  18571  psssdm  18638  ex-chn1  18693  ex-chn2  18694  ismgmn0  18700  plusfeq  18706  idresefmnd  18958  qsxpid  19243  snsymgefmndeq  19465  fvcosymgeq  19499  pmtrprfv3  19524  pmtr3ncomlem1  19543  ablsubadd23  19883  ablsubsub23  19894  cygabl  19961  gsummptfzsplitl  20003  gsum2dlem1  20040  gsum2dlem2  20041  gsum2d  20042  rng1zrlem  20259  opprnzr  20606  cntzsubrng  20652  ringcinv  20756  opprdomn  20802  drngmcl  20834  staffn  20924  scafeq  20981  lbsexg  21266  rngridlmcl  21320  rnglidl1  21336  df2idl2  21367  2idlss  21372  ssdifidlprm  21455  prmirred  21593  frgpcyg  21692  ipfeq  21769  dsmmbas2  21856  zlmassa  22022  ply1bascl2  22333  lply1binom  22439  mamufacex  22522  matsubgcell  22560  matinvgcell  22561  matepmcl  22588  matepm2cl  22589  marrepcl  22690  marepvcl  22695  mulmarep1el  22698  mulmarep1gsum1  22699  mulmarep1gsum2  22700  nfimdetndef  22715  mdetfval1  22716  m1detdiag  22723  mdetdiag  22725  slesolinvbi  22807  pmatcoe1fsupp  22827  mat2pmatbas  22852  mat2pmatmul  22857  m2cpminvid2lem  22880  monmatcollpw  22905  pm2mpf1  22925  pm2mpghm  22942  cayhamlem1  22992  isbasis3g  23075  isopn2  23158  ntrval2  23177  toponmre  23219  innei  23251  restcld  23298  restcldi  23299  neitr  23306  discmp  23524  cmpsublem  23525  cmpsub  23526  ssref  23638  dissnref  23654  ptcnp  23748  imasnopn  23816  imasncld  23817  imasncls  23818  kqf  23873  fbun  23966  opnfbas  23968  supfil  24021  ufprim  24035  acufl  24043  filufint  24046  ufldom  24088  hausflf2  24124  alexsubALTlem4  24176  cnextfval  24188  cnextfun  24190  cnextfres1  24194  efmndtmd  24227  trust  24355  ustuqtop1  24367  metustid  24680  metustbl  24692  restmetu  24696  zlmclm  25240  cphassr  25340  ehleudisval  25547  ovolun  25627  vitalilem2  25737  dvcobr  26074  dvmptfsum  26103  rolle  26118  dvfsumlem2  26155  plyn0mulidp  26411  ulmcaulem  26523  logfac  26732  logno1  26767  logreclem  26893  prmorcht  27308  pclogsum  27345  gausslemma2dlem0i  27494  gausslemma2dlem1a  27495  2lgslem1c  27523  2sqlem10  27558  chto1lb  27608  cutsval  27939  addsproplem2  28129  oncutlt  28423  n0s0suc  28501  tgjustf  28708  tgldimor  28737  axcontlem7  29261  lfgredgge2  29415  edgupgr  29425  ausgrusgrb  29456  ausgrumgri  29458  uspgredg2vlem  29514  uspgredg2v  29515  usgredg2vlem2  29517  usgredg2v  29518  ushgredgedg  29520  ushgredgedgloop  29522  griedg0ssusgr  29556  umgrres1lem  29601  upgrres1  29604  nbgrcl  29626  nbgrnvtx0  29630  nbuhgr  29634  nbuhgr2vtx1edgb  29643  edgnbusgreu  29658  nb3grprlem2  29672  nb3grpr2  29674  nb3gr2nb  29675  cplgr2vpr  29724  cplgr3v  29726  vtxdumgrval  29777  umgr2v2evtxel  29813  usgrvd0nedg  29824  finsumvtxdg2ssteplem4  29839  wlk1walk  29929  wlk0prc  29943  wlkp1lem8  29969  wlkp1  29970  spthdep  30024  usgr2pthlem  30053  usgr2pth  30054  crctprop  30082  cyclprop  30083  cyclnumvtx  30090  crctcshwlkn0  30111  wwlknllvtx  30136  wlkiswwlks1  30157  wlkswwlksf1o  30169  wwlksnextproplem3  30201  wwlksnwwlksnon  30205  umgr2wlkon  30240  wwlks2onv  30243  elwspths2on  30252  elwspths2onw  30253  elwwlks2  30259  elwspths2spth  30260  rusgrnumwwlks  30267  clwlkclwwlklem2a4  30289  clwlkclwwlklem2  30292  clwlkclwwlkf  30300  erclwwlkref  30312  erclwwlknref  30361  erclwwlknsym  30362  erclwwlkntr  30363  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  clwlknf1oclwwlknlem1  30373  clwwlknon1  30389  clwwlknon1nloop  30391  clwwlkvbij  30405  0clwlkv  30423  uhgr3cyclex  30474  umgr3cyclex  30475  vdn0conngrumgrv2  30488  eupthi  30495  eucrctshift  30535  frcond1  30558  frcond4  30562  frgr3v  30567  3vfriswmgr  30570  1to2vfriswmgr  30571  1to3vfriswmgr  30572  2pthfrgr  30576  4cycl2v2nb  30581  n4cyclfrgr  30583  frgrnbnb  30585  frgrwopreglem4a  30602  clwlknon2num  30660  numclwwlkqhash  30667  frgrreg  30686  frgrregord013  30687  ex-ceil  30740  grpoidinvlem3  30799  nmlno0lem  31086  blocni  31098  pythi  31143  normpythi  31435  shmodsi  31682  pjchi  31725  chlubii  31765  osumi  31935  nmlnop0iALT  32288  cnlnssadj  32373  nmopcoi  32388  mdbr3  32590  mdbr4  32591  ssmd1  32604  dmdsl3  32608  mdexchi  32628  atssma  32671  atoml2i  32676  chirredlem3  32685  mdsymlem1  32696  dmdbr6ati  32716  dmdbr7ati  32717  cdjreui  32725  cdj3lem2b  32730  addltmulALT  32739  difuncomp  32839  iundifdif  32848  imadifxp  32887  fresf1o  32917  2ndimaxp  32932  acunirnmpt2  32946  suppiniseg  32972  fressupp  32974  fdifsuppconst  32975  ressupprn  32976  disjdsct  32989  1stpreimas  32992  preiman0  32996  resf1o  33016  xrge0addge  33044  xlt2addrd  33045  fz2ssnn0  33071  f1ocnt  33086  elq2  33097  nexple  33118  s2rnOLD  33205  s3rnOLD  33207  gsummpt2d  33310  gsumfs2d  33322  gsumwun  33337  psgnfzto1stlem  33361  fzto1st  33364  psgnfzto1st  33366  cycpmco2f1  33385  cycpmco2rn  33386  cycpmco2lem7  33393  elrgspn  33507  elrgspnsubrunlem2  33509  elrlocbasi  33528  ricnzr1  33549  sdrginvcl  33564  nsgqusf1olem2  33667  elrspunidl  33680  ssmxidl  33702  selvply1rhmlem2  33856  lbsdiflsp0  33961  fldextfld1  33982  fldextfld2  33983  constrconj  34080  constrllcllem  34087  constrlccllem  34088  constrcccllem  34089  submat1n  34140  submatres  34141  locfinreflem  34175  ldlfcntref  34189  zarclsun  34205  zarclsiin  34206  zarclsint  34207  zarcmplem  34216  mndpluscn  34261  pnfneige0  34286  pl1cn  34290  gsumesum  34394  esumcst  34398  esumrnmpt2  34403  esumcvgre  34426  esum2d  34428  pwsiga  34465  ldsysgenld  34495  measxun2  34545  volmeas  34566  ddemeas  34571  aean  34579  mbfmfun  34588  1stmbfm  34595  2ndmbfm  34596  omssubadd  34635  carsgclctunlem1  34652  sibfof  34675  eulerpartlemmf  34710  probun  34754  dstfrvclim1  34813  coinfliprv  34818  ballotlem2  34824  ballotlemic  34842  ballotlem1c  34843  signstres  34907  bnj529  35075  bnj1379  35163  bnj1424  35171  bnj1436  35172  bnj607  35249  bnj908  35264  bnj1097  35314  bnj1118  35317  bnj1128  35323  bnj1145  35326  bnj1154  35332  bnj1174  35336  bnj1189  35342  bnj1417  35374  axprALT2  35446  acnum  35458  tz9.1regs  35480  axsepg2  35486  axsepg4  35489  kardcard2b  35511  0nn0m1nnn0  35537  lfuhgr2  35544  cusgr3cyclex  35561  cvmliftlem10  35719  satfv1  35788  fmlasuc0  35809  satffunlem2lem1  35829  mrsub0  35941  mrsubccat  35943  mrsubcn  35944  bcprod  36163  socnv  36189  dfon2lem3  36208  dfon2lem7  36212  dfon2lem8  36213  rdgprc0  36216  fvsingle  36343  unisnif  36348  funpartlem  36367  hfun  36603  ss-ax8  36660  trer  36750  clsun  36762  opnregcld  36764  cldregopn  36765  df3nandALT1  36833  lukshef-ax2  36849  nandsym1  36856  weiunfr  36901  dfttc4lem2  36963  knoppndvlem9  37032  bj-mt2bi  37083  bj-gl4  37111  bj-babygodel  37119  bj-babylob  37120  bj-ssbid2ALT  37208  bj-nfext  37262  bj-1upln0  37567  bj-snex  37593  eleq2w2ALT  37605  bj-brrelex12ALT  37625  bj-restsnid  37651  bj-snmooreb  37678  bj-opelrelex  37710  bj-inftyexpitaudisj  37771  bj-inftyexpidisj  37776  bj-elccinfty  37780  finorwe  37950  ctbssinf  37974  fvineqsnf1  37978  pibt2  37985  wl-ifpimpr  38034  wl-ifp4impr  38035  wl-1xor  38050  wl-1mintru1  38056  lindsadd  38186  lindsenlbs  38188  poimirlem9  38202  poimirlem13  38206  poimirlem14  38207  poimirlem25  38218  poimirlem26  38219  mblfinlem2  38231  mblfinlem3  38232  mblfinlem4  38233  ismblfin  38234  mbfresfi  38239  ftc1cnnc  38265  dvasin  38277  fnopabco  38296  frinfm  38308  caushft  38334  bndss  38359  notornotel1  38668  tsbi2  38707  rabeq12f  38730  relcnveq3  38900  relcnveq2  38902  cnvref4  38923  ralrnmo  38934  raldmqsmo  38936  disjressuc2  38984  cnvcosseq  39100  symrelcoss3  39128  dfrefrels2  39166  dfrefrel2  39168  dfcnvrefrels2  39181  dfcnvrefrel2  39183  dfsymrels2  39198  elrelscnveq3  39200  dfsymrel2  39206  symrefref2  39220  dftrrels2  39232  dftrrel2  39234  n0elim  39308  disjimeceqim  39377  membpartlem19  39487  axc11n-16  39636  glbconN  40075  paddssat  40512  pclunN  40596  paddunN  40625  poldmj1N  40626  ltrnnid  40834  dibglbN  41864  mndmolinv  42786  primrootsunit1  42788  primrootscoprmpow  42790  primrootscoprbij  42793  aks6d1c2lem4  42818  aks6d1c2  42821  aks6d1c5lem3  42828  deg1gprod  42831  sticksstones3  42839  sticksstones11  42847  sticksstones12a  42848  sticksstones12  42849  sticksstones13  42850  aks6d1c6isolem1  42865  aks6d1c6lem5  42868  grpods  42885  unitscyglem2  42887  unitscyglem3  42888  unitscyglem4  42889  aks5lem7  42891  exbiii  42903  sn-0ne2  43091  sn-0lt1  43173  istopclsd  43357  pellex  43488  monotoddzzfi  43595  jm2.23  43649  expdioph  43676  wopprc  43683  kelac1  43716  dfac21  43719  lsmfgcl  43727  pwssplit4  43742  isnumbasgrp  43760  dgraalem  43798  ordnexbtwnsuc  43920  cantnfresb  43977  dflim5  43982  rp-tfslim  44006  ifpbi1  44129  rp-fakeanorass  44165  rp-isfinite5  44169  iscard4  44185  minregex  44186  pr2cv  44200  superficl  44219  ssuncl  44222  sssymdifcl  44224  relintab  44235  cnvssb  44238  cotrintab  44266  clcnvlem  44275  cnvtrrel  44322  brfvrcld2  44344  relexpxpmin  44369  relexpaddss  44370  unhe1  44437  frege55lem1b  44547  frege58bid  44554  frege92  44607  uneqsn  44677  ntrk2imkb  44689  neik0pk1imk0  44699  gneispace  44786  k0004lem2  44800  k0004val0  44806  ismnushort  44937  pm10.12  44994  pm11.61  45029  sbiota1  45070  bi1imp  45117  bi2imp  45118  bi3impb  45119  bi3impa  45120  bi13impib  45122  bi123impib  45123  bi13impia  45124  bi123impia  45125  bi13imp23  45127  bi13imp2  45128  bi12imp3  45129  tratrb  45171  dfvd1imp  45210  dfvd2imp  45238  e1bi  45264  e2bi  45267  e3bi  45372  3ornot23VD  45481  3impexpbicomVD  45491  3impexpbicomiVD  45492  tratrbVD  45495  ssralv2VD  45500  equncomiVD  45503  truniALTVD  45512  ee33VD  45513  onfrALTlem3VD  45521  onfrALTlem2VD  45523  onfrALTlem1VD  45524  onfrALTVD  45525  relopabVD  45535  2uasbanhVD  45545  vk15.4jVD  45548  unisnALT  45560  chordthmALT  45567  iunconnlem2  45569  wfaxpow  45632  wfaxun  45634  fnchoice  45675  uzwo4  45699  inabs3  45702  rexanuz3  45740  disjrnmpt2  45832  disjinfi  45836  iunmapsn  45859  ssfiunibd  45954  iuneqfzuzlem  45976  iuneqfzuz  45977  xrge0ge0  45989  xrssre  45990  infrpge  45993  allbutfi  46034  supxrunb3  46040  eluzelz2  46043  uz0  46052  allbutfiinf  46060  infxrunb3rnmpt  46068  uzublem  46070  uzub  46071  uzid3  46075  infxrlesupxr  46076  infrpgernmpt  46105  supminfxrrnmpt  46111  rexanuz2nf  46132  eliocre  46151  lbioc  46155  ioonct  46179  uzinico  46201  fsumiunss  46217  fmuldfeq  46225  mccl  46240  climsuse  46250  islptre  46261  lptioo2  46273  lptioo1  46274  islpcn  46279  fnlimfvre  46314  climbddf  46327  limsupubuzlem  46352  limsupmnfuzlem  46366  limsupequzmptlem  46368  limsupre3uzlem  46375  xlimcl  46462  cnrefiisplem  46469  xlimliminflimsup  46502  icccncfext  46527  cncfiooicclem1  46533  cncfiooicc  46534  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnprodlem1  46586  dvnprodlem3  46588  volioc  46612  itgioocnicc  46617  stoweidlem28  46668  stoweidlem57  46697  wallispilem3  46707  wallispilem4  46708  wallispi  46710  wallispi2lem1  46711  wallispi2  46713  stirlinglem12  46725  fourierdlem42  46789  fourierdlem48  46794  fourierdlem50  46796  fourierdlem52  46798  fourierdlem71  46817  fourierdlem73  46819  fourierdlem74  46820  fourierdlem75  46821  fourierdlem76  46822  fourierdlem80  46826  fourierdlem93  46839  fourierdlem101  46847  fourierdlem103  46849  fourierdlem104  46850  fourierswlem  46870  fouriersw  46871  etransclem26  46900  etransclem37  46911  rrxsnicc  46940  saluncl  46957  intsaluni  46969  intsal  46970  salgencl  46972  salexct  46974  sssalgen  46975  salgenuni  46977  issalgend  46978  salgencntex  46983  subsaliuncllem  46997  subsaliuncl  46998  sge00  47016  sge0sn  47019  sge0cl  47021  sge0f1o  47022  sge0pnffigt  47036  sge0resplit  47046  sge0split  47049  sge0iunmptlemre  47055  sge0xaddlem2  47074  iundjiun  47100  meadjun  47102  meassle  47103  meadjiunlem  47105  meaiunlelem  47108  volmea  47114  caragenunidm  47148  omeunle  47156  omeiunltfirp  47159  caratheodorylem1  47166  caratheodory  47168  icoresmbl  47183  volicorescl  47193  ovncvrrp  47204  ovnsubaddlem2  47211  hoidmv1le  47234  hoidmvlelem1  47235  hoidmvlelem2  47236  hoidmvlelem5  47239  hoidmvle  47240  ovnhoilem2  47242  hspdifhsp  47256  hoiqssbllem3  47264  hspmbllem2  47267  ovolval4lem1  47289  ovnovollem3  47298  vonioolem1  47320  pimdecfgtioo  47357  pimincfltioo  47358  mbfresmf  47379  smfaddlem1  47403  smflimlem1  47411  smflimlem2  47412  smflimlem3  47413  smflim  47417  smfresal  47428  smfrec  47429  smfmullem4  47434  smfdiv  47437  smfpimbor1lem2  47439  smflimmpt  47450  smfsuplem1  47451  smfinflem  47457  smflimsuplem3  47462  smflimsuplem5  47464  smflimsuplem6  47465  smflimsuplem7  47466  smflimsupmpt  47469  smfliminflem  47470  smfliminfmpt  47472  simpcntrab  47510  quantgodelALT  47515  chnerlem1  47524  chnerlem2  47525  cos5teq  47540  lambert0  47547  lamberte  47548  aifftbifffaibif  47581  aifftbifffaibifff  47582  abciffcbatnabciffncba  47589  abciffcbatnabciffncbai  47590  nabctnabc  47591  confun4  47602  confun5  47603  plcofph  47604  pldofph  47605  plvcofph  47606  plvcofphax  47607  plvofpos  47608  dandysum2p2e4  47658  fresfo  47708  fcores  47727  3f1oss1  47735  3f1oss2  47736  funfocofob  47738  aiotaint  47751  dfaiota3  47752  ndmaovrcl  47864  tz6.12-afv2  47900  fvmptrabdm  47953  difmodm1lt  48025  uniimafveqt  48053  uniimaelsetpreimafv  48068  iccpartiun  48106  iccpartdisj  48109  ich2exprop  48143  ichnreuop  48144  prpair  48173  fmtnorec2lem  48217  dfodd5  48348  stgoldbwt  48464  sbgoldbb  48470  nnsum3primesle9  48482  nnsum4primeseven  48488  clnbgrcl  48509  clnbgrnvtx0  48515  clnbgredg  48528  grimuhgr  48575  isuspgrim0  48582  isuspgrimlem  48583  gricushgr  48605  grtriclwlk3  48633  isubgr3stgrlem1  48654  isubgr3stgrlem7  48660  uspgrlimlem2  48677  uspgrlimlem4  48679  grlimprclnbgr  48684  gpgusgralem  48744  gpg5order  48748  gpg5nbgrvtx03star  48768  gpg5nbgr3star  48769  gpgvtxdg3  48770  gpg5gricstgr3  48778  pgnbgreunbgrlem3  48806  pgnbgreunbgrlem6  48812  pgnbgreunbgr  48813  pgn4cyclex  48814  lmod0rng  48917  lidldomnnring  48924  ringcinvALTV  48998  altgsumbcALT  49052  ply1sclrmsm  49083  linccl  49113  lincvalsng  49115  lincvalpr  49117  lincdifsn  49123  linc1  49124  lincsum  49128  lincscm  49129  lindslinindsimp2lem5  49161  lincresunit3lem2  49179  2sphere  49448  resinsnALT  49570  tposideq  49585  clduni  49598  neircl  49602  funcrcl2  49776  funcrcl3  49777  funcf2lem2  49779  uprcl2  49886  uprcl3  49887  swapf2fval  49962  swapf1val  49964  fucofvalne  50022  thincn0eu  50128  isinito3  50197  mndtcbas2  50280