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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylbi  220  sylib  221  sylbb  222  biimpri  231  mpbi  233  biimtrid  245  imbitrdi  254  syl7bi  258  syl8ib  259  simplbi  502  simprbi  503  birani  509  bilani  510  anc2l  563  sylanb  593  sylanblc  601  sylan2b  606  pm3.37  820  pm2.53  865  orbi2i  926  pm2.32  937  pm2.76  945  pm3.1  1007  pm5.15  1030  pm5.16  1031  4exmid  1067  simp1bi  1163  simp2bi  1164  simp3bi  1165  syl3an1b  1430  syl3an2b  1431  syl3an3b  1432  hadifp  1637  nic-ax  1706  nfnt  1889  19.25  1913  nfimd  1927  19.37imv  1980  alcomimw  2076  sbbii  2113  nsb  2143  excomim  2200  stdpc5  2244  sbequ2  2284  sb9i  2549  mo4  2591  2mo  2673  ax9ALT  2755  eleq2w2  2756  eqeq1d  2762  r19.37v  3188  rmoeq1  3396  elabgt  3626  euind  3682  reuind  3711  sbcimdv  3807  sbcg  3811  ra4v  3832  ra4  3833  csbied  3883  ssrmof  3999  elunnel1  4101  elunnel2  4102  unssd  4138  n0moeu  4307  eqeuel  4313  ss0  4352  iftrueb  4495  elinsn  4671  disjtp2  4677  rabsnif  4684  prprc  4728  elpwdifsn  4752  ssunsn2  4788  preqr1  4808  intss2  5068  disjxiun  5100  unisn2  5269  snexALT  5348  reusv3i  5369  snexOLD  5407  pocl  5571  brrelex12  5707  0nelrel0  5715  elrel  5778  exopxfr2  5824  dmxp  5913  xpssres  6011  elinxp  6012  imadisjlnd  6077  elimasni  6087  inisegn0  6094  xpdifid  6160  xpdifcnvepel  6161  imadifssranOLD  6198  dmsnsnsn  6216  relcnvtrgOLD  6264  xpco  6287  reuop  6291  predprc  6336  sucprc  6436  onunel  6465  iotaint  6511  iotanul  6513  funun  6580  funcnv3  6604  funimass1  6616  funssxp  6732  f0dom0  6760  dffv3  6875  dffv2  6974  fsneq  7028  fndmin  7038  sspreima  7061  iinpreima  7063  fveqressseq  7073  fsn2  7131  f1ounsn  7274  f12dfv  7275  f13dfv  7276  isoselem  7343  oprabidw  7445  oprabid  7446  ovima0  7594  sorpsscmpl  7736  abnex  7757  pwuncl  7770  ordsuci  7808  peano2  7887  1stval  7989  2ndval  7990  1stdm  8038  oprabco  8094  f1o2ndf1  8120  poxp  8127  frxp3  8150  suppval1  8165  fnsuppeq0  8191  frrlem4  8289  tz7.48lemOLD  8433  tz7.49c  8438  ord1eln01  8486  ord2eln012  8487  undifixp  8944  bren2  8992  ensym  9012  en1uniel  9039  domunsn  9128  limenpsi  9153  findcard2  9162  unfi  9168  pwssfi  9174  php4  9207  isinf  9238  en2  9253  fiint  9299  rneqdmfinf1o  9303  elfiun  9403  marypha1lem  9406  supval2  9428  eqinf  9458  brwdom2  9548  zfreg  9571  tcmin  9721  frmin  9734  prwf  9796  r1pw  9830  rankuni2b  9838  rankr1id  9847  djuun  9934  cardval3  9960  ficardom  9969  cardmin2  10007  isinfcard  10098  iscard3  10099  alephval3  10116  dfac9  10142  kmlem6  10161  fin23lem29  10346  fin23lem30  10347  isf32lem11  10368  isfin1-3  10391  fin45  10397  fin1a2lem12  10416  fin1a2lem13  10417  axcc2lem  10441  dominf  10450  axdc4lem  10460  dominfac  10585  pwcfsdom  10595  cfpwsdom  10596  tskuni  10795  wfgru  10828  0nn0m1nnn0  12678  rpregt0  13060  supxrun  13371  elicore  13454  xrge0nre  13509  elfz1end  13612  elfzonlteqm1  13800  modfzo0difsn  14010  fzennn  14035  cardfz  14037  fsuppmapnn0fiub0  14060  ser0  14121  crreczi  14295  faclbnd  14357  bcn1  14380  hashrabsn01  14440  hashge0  14454  prsshashgt1  14478  hashssdif  14480  hashdifpr  14483  hashsn01  14484  hashgt23el  14492  hashpw  14504  hashres  14506  hash3tpexb  14562  ccatw2s1p1  14707  swrdswrd  14777  swrdccatin2  14801  pfxccatpfx1  14808  repsundef  14845  trclublem  15071  reltrclfv  15093  dmtrclfv  15094  cau3lem  15445  harmonic  15951  mertenslem2  15977  prodf1  15983  fprodfac  16063  rpnnen2lem12  16316  sqrt2irr0  16342  sadadd2lem2  16543  saddisjlem  16557  lcmftp  16729  lcmfunsnlem2lem1  16731  lcmfunsnlem2lem2  16732  prmind2  16778  prm2orodd  16784  pceq0  16966  prmreclem6  17016  0ram  17115  ram0  17117  cshwsiun  17194  ressbas2  17333  ressinbas  17340  ressval3d  17341  catpropd  17800  initoid  18093  termoid  18094  initoeu2lem0  18105  arwhoma  18137  joinfval  18462  meetfval  18476  lubun  18606  psssdm  18673  ex-chn1  18728  ex-chn2  18729  ismgmn0  18735  plusfeq  18741  idresefmnd  19011  qsxpid  19303  snsymgefmndeq  19525  fvcosymgeq  19559  pmtrprfv3  19584  pmtr3ncomlem1  19603  ablsubadd23  19943  ablsubsub23  19954  cygabl  20021  gsummptfzsplitl  20063  gsum2dlem1  20100  gsum2dlem2  20101  gsum2d  20102  rng1zrlem  20319  opprnzr  20686  cntzsubrng  20732  ringcinv  20836  opprdomn  20882  drngmcl  20921  staffn  21012  scafeq  21069  lbsexg  21354  rngridlmcl  21408  rnglidl1  21424  df2idl2  21462  2idlss  21467  ssdifidlprm  21552  prmirred  21690  frgpcyg  21789  ipfeq  21866  dsmmbas2  21953  lindsenlbs  22067  zlmassa  22121  ply1bascl2  22432  lply1binom  22538  mamufacex  22621  matsubgcell  22659  matinvgcell  22660  matepmcl  22687  matepm2cl  22688  marrepcl  22789  marepvcl  22794  mulmarep1el  22797  mulmarep1gsum1  22798  mulmarep1gsum2  22799  nfimdetndef  22814  mdetfval1  22815  m1detdiag  22822  mdetdiag  22824  slesolinvbi  22909  pmatcoe1fsupp  22929  mat2pmatbas  22954  mat2pmatmul  22959  m2cpminvid2lem  22982  monmatcollpw  23007  pm2mpf1  23027  pm2mpghm  23044  cayhamlem1  23094  isbasis3g  23177  isopn2  23260  ntrval2  23279  toponmre  23321  innei  23353  restcld  23400  restcldi  23401  neitr  23408  discmp  23626  cmpsublem  23627  cmpsub  23628  ssref  23741  dissnref  23757  ptcnp  23851  imasnopn  23919  imasncld  23920  imasncls  23921  kqf  23976  fbun  24069  opnfbas  24071  supfil  24124  ufprim  24138  acufl  24146  filufint  24149  ufldom  24191  hausflf2  24227  alexsubALTlem4  24279  cnextfval  24291  cnextfun  24293  cnextfres1  24297  efmndtmd  24330  trust  24458  ustuqtop1  24470  metustid  24783  metustbl  24795  restmetu  24799  zlmclm  25343  cphassr  25443  ehleudisval  25650  ovolun  25730  vitalilem2  25840  dvcobr  26176  dvmptfsum  26205  rolle  26220  dvfsumlem2  26257  plyn0mulidp  26514  ulmcaulem  26633  logfac  26841  logno1  26876  logreclem  27002  prmorcht  27417  pclogsum  27454  gausslemma2dlem0i  27603  gausslemma2dlem1a  27604  2lgslem1c  27632  2sqlem10  27667  chto1lb  27717  cutsval  28048  addsproplem2  28238  oncutlt  28532  n0s0suc  28610  tgjustf  28817  tgldimor  28847  cgraer  29259  angmgmlem  29277  axcontlem7  29430  lfgredgge2  29584  edgupgr  29594  lfuhgr2  29609  ausgrusgrb  29628  ausgrumgri  29630  uspgredg2vlem  29686  uspgredg2v  29687  usgredg2vlem2  29689  usgredg2v  29690  ushgredgedg  29692  ushgredgedgloop  29694  griedg0ssusgr  29728  umgrres1lem  29773  upgrres1  29776  nbgrcl  29798  nbgrnvtx0  29802  nbuhgr  29806  nbuhgr2vtx1edgb  29815  edgnbusgreu  29830  nb3grprlem2  29844  nb3grpr2  29846  nb3gr2nb  29847  cplgr2vpr  29896  cplgr3v  29898  vtxdumgrval  29949  umgr2v2evtxel  29985  usgrvd0nedg  29996  finsumvtxdg2ssteplem4  30011  wlk1walk  30101  wlk0prc  30115  wlkp1lem8  30141  wlkp1  30142  spthdep  30202  usgr2pthlem  30231  usgr2pth  30232  crctprop  30261  cyclprop  30262  cyclnumvtx  30270  crctcshwlkn0  30292  wwlknllvtx  30317  wlkiswwlks1  30338  wlkswwlksf1o  30350  wwlksnextproplem3  30382  wwlksnwwlksnon  30386  umgr2wlkon  30421  wwlks2onv  30424  elwspths2on  30433  elwspths2onw  30434  elwwlks2  30440  elwspths2spth  30441  rusgrnumwwlks  30448  clwlkclwwlklem2a4  30470  clwlkclwwlklem2  30473  clwlkclwwlkf  30481  erclwwlkref  30493  erclwwlknref  30542  erclwwlknsym  30543  erclwwlkntr  30544  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  clwlknf1oclwwlknlem1  30554  clwwlknon1  30570  clwwlknon1nloop  30572  clwwlkvbij  30586  0clwlkv  30604  uhgr3cyclex  30665  umgr3cyclex  30666  vdn0conngrumgrv2  30679  eupthi  30686  eucrctshift  30726  frcond1  30749  frcond4  30753  frgr3v  30758  3vfriswmgr  30761  1to2vfriswmgr  30762  1to3vfriswmgr  30763  2pthfrgr  30767  4cycl2v2nb  30772  n4cyclfrgr  30774  frgrnbnb  30776  frgrwopreglem4a  30793  clwlknon2num  30851  numclwwlkqhash  30858  frgrreg  30877  frgrregord013  30878  ex-ceil  30931  grpoidinvlem3  30990  nmlno0lem  31277  blocni  31289  pythi  31334  normpythi  31626  shmodsi  31873  pjchi  31916  chlubii  31956  osumi  32126  nmlnop0iALT  32479  cnlnssadj  32564  nmopcoi  32579  mdbr3  32781  mdbr4  32782  ssmd1  32795  dmdsl3  32799  mdexchi  32819  atssma  32862  atoml2i  32867  chirredlem3  32876  mdsymlem1  32887  dmdbr6ati  32907  dmdbr7ati  32908  cdjreui  32916  cdj3lem2b  32921  addltmulALT  32930  difuncomp  33030  iundifdif  33039  imadifxp  33077  fresf1o  33107  2ndimaxp  33122  acunirnmpt2  33136  suppiniseg  33161  fressupp  33163  fdifsuppconst  33164  ressupprn  33165  disjdsct  33178  1stpreimas  33181  preiman0  33185  resf1o  33204  xrge0addge  33232  xlt2addrd  33233  fz2ssnn0  33259  f1ocnt  33274  elq2  33285  nexple  33306  gsummpt2d  33492  gsumfs2d  33504  gsumwun  33519  psgnfzto1stlem  33543  fzto1st  33546  psgnfzto1st  33548  cycpmco2f1  33567  cycpmco2rn  33568  cycpmco2lem7  33575  elrgspn  33689  elrgspnsubrunlem2  33691  elrlocbasi  33710  ricnzr1  33731  sdrginvcl  33744  nsgqusf1olem2  33846  elrspunidl  33859  ssmxidl  33880  lbsdiflsp0  34139  fldextfld1  34160  fldextfld2  34161  constrconj  34258  constrllcllem  34265  constrlccllem  34266  constrcccllem  34267  submat1n  34318  submatres  34319  locfinreflem  34353  ldlfcntref  34367  zarclsun  34383  zarclsiin  34384  zarclsint  34385  zarcmplem  34394  mndpluscn  34439  pnfneige0  34464  pl1cn  34468  gsumesum  34572  esumcst  34576  esumrnmpt2  34581  esumcvgre  34604  esum2d  34606  pwsiga  34643  ldsysgenld  34674  measxun2  34724  volmeas  34745  ddemeas  34750  aean  34758  mbfmfun  34767  1stmbfm  34774  2ndmbfm  34775  omssubadd  34814  carsgclctunlem1  34831  sibfof  34854  eulerpartlemmf  34889  probun  34933  dstfrvclim1  34992  coinfliprv  34997  ballotlem2  35003  ballotlemic  35021  ballotlem1c  35022  signstres  35086  bnj529  35254  bnj1379  35342  bnj1424  35350  bnj1436  35351  bnj607  35428  bnj908  35443  bnj1097  35493  bnj1118  35496  bnj1128  35502  bnj1145  35505  bnj1154  35511  bnj1174  35515  bnj1189  35521  bnj1417  35553  axprALT2  35620  rankfo  35622  acnum  35641  tz9.1regs  35663  axsepg2  35669  axsepg4  35672  kardcard2b  35694  cusgr3cyclex  35728  cvmliftlem10  35876  satfv1  35945  fmlasuc0  35966  satffunlem2lem1  35986  mrsub0  36098  mrsubccat  36100  mrsubcn  36101  bcprod  36320  socnv  36346  dfon2lem3  36365  dfon2lem7  36369  dfon2lem8  36370  rdgprc0  36373  fvsingle  36500  unisnif  36505  funpartlem  36524  hfun  36761  ss-ax8  36848  trer  36938  clsun  36950  opnregcld  36952  cldregopn  36953  df3nandALT1  37021  lukshef-ax2  37037  nandsym1  37044  weiunfr  37089  dfttc4lem2  37151  knoppndvlem9  37220  bj-mt2bi  37271  bj-gl4  37299  bj-babygodel  37307  bj-babylob  37308  bj-ssbid2ALT  37396  bj-nfext  37450  bj-1upln0  37756  bj-snex  37782  eleq2w2ALT  37794  bj-brrelex12ALT  37814  bj-restsnid  37840  bj-snmooreb  37867  bj-opelrelex  37899  bj-inftyexpitaudisj  37960  bj-inftyexpidisj  37965  bj-elccinfty  37969  finorwe  38139  ctbssinf  38163  fvineqsnf1  38167  pibt2  38174  wl-ifpimpr  38223  wl-ifp4impr  38224  wl-1xor  38239  wl-1mintru1  38245  lindsadd  38370  poimirlem9  38381  poimirlem13  38385  poimirlem14  38386  poimirlem25  38397  poimirlem26  38398  mblfinlem2  38410  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  mbfresfi  38418  ftc1cnnc  38444  dvasin  38456  fnopabco  38476  frinfm  38488  caushft  38514  bndss  38539  notornotel1  38846  tsbi2  38885  rabeq12f  38908  relcnveq3  39078  relcnveq2  39080  cnvref4  39101  ralrnmo  39112  raldmqsmo  39114  disjressuc2  39162  cnvcosseq  39278  symrelcoss3  39306  dfrefrels2  39344  dfrefrel2  39346  dfcnvrefrels2  39359  dfcnvrefrel2  39361  dfsymrels2  39376  elrelscnveq3  39378  dfsymrel2  39384  symrefref2  39398  dftrrels2  39410  dftrrel2  39412  n0elim  39486  disjimeceqim  39555  membpartlem19  39665  axc11n-16  39814  glbconN  40253  paddssat  40690  pclunN  40774  paddunN  40803  poldmj1N  40804  ltrnnid  41012  dibglbN  42042  mndmolinv  42964  primrootsunit1  42966  primrootscoprmpow  42968  primrootscoprbij  42971  aks6d1c2lem4  42996  aks6d1c2  42999  aks6d1c5lem3  43006  deg1gprod  43009  sticksstones3  43017  sticksstones11  43025  sticksstones12a  43026  sticksstones12  43027  sticksstones13  43028  aks6d1c6isolem1  43043  aks6d1c6lem5  43046  grpods  43063  unitscyglem2  43065  unitscyglem3  43066  unitscyglem4  43067  aks5lem7  43069  exbiii  43081  sn-0ne2  43284  sn-0lt1  43366  istopclsd  43548  pellex  43679  monotoddzzfi  43786  jm2.23  43840  expdioph  43867  wopprc  43874  kelac1  43907  dfac21  43910  lsmfgcl  43918  pwssplit4  43933  isnumbasgrp  43951  dgraalem  43989  ordnexbtwnsuc  44111  cantnfresb  44168  dflim5  44173  rp-tfslim  44197  ifpbi1  44320  rp-fakeanorass  44356  rp-isfinite5  44360  iscard4  44376  minregex  44377  pr2cv  44391  superficl  44410  ssuncl  44413  sssymdifcl  44415  relintab  44426  cnvssb  44429  cotrintab  44457  clcnvlem  44466  cnvtrrel  44513  brfvrcld2  44535  relexpxpmin  44560  relexpaddss  44561  unhe1  44628  frege55lem1b  44738  frege58bid  44745  frege92  44798  uneqsn  44868  ntrk2imkb  44880  neik0pk1imk0  44890  gneispace  44977  k0004lem2  44991  k0004val0  44997  ismnushort  45128  pm10.12  45185  pm11.61  45220  sbiota1  45261  bi1imp  45308  bi2imp  45309  bi3impb  45310  bi3impa  45311  bi13impib  45313  bi123impib  45314  bi13impia  45315  bi123impia  45316  bi13imp23  45318  bi13imp2  45319  bi12imp3  45320  tratrb  45362  dfvd1imp  45401  dfvd2imp  45429  e1bi  45455  e2bi  45458  e3bi  45563  3ornot23VD  45672  3impexpbicomVD  45682  3impexpbicomiVD  45683  tratrbVD  45686  ssralv2VD  45691  equncomiVD  45694  truniALTVD  45703  ee33VD  45704  onfrALTlem3VD  45712  onfrALTlem2VD  45714  onfrALTlem1VD  45715  onfrALTVD  45716  relopabVD  45726  2uasbanhVD  45736  vk15.4jVD  45739  unisnALT  45751  chordthmALT  45758  iunconnlem2  45760  wfaxpow  45823  wfaxun  45825  fnchoice  45866  uzwo4  45890  inabs3  45893  rexanuz3  45931  disjrnmpt2  46023  disjinfi  46027  iunmapsn  46050  ssfiunibd  46145  iuneqfzuzlem  46167  iuneqfzuz  46168  xrge0ge0  46180  xrssre  46181  infrpge  46184  allbutfi  46225  supxrunb3  46231  eluzelz2  46234  uz0  46243  allbutfiinf  46251  infxrunb3rnmpt  46259  uzublem  46261  uzub  46262  uzid3  46266  infxrlesupxr  46267  infrpgernmpt  46296  supminfxrrnmpt  46302  rexanuz2nf  46323  eliocre  46342  lbioc  46346  ioonct  46370  uzinico  46392  fsumiunss  46408  fmuldfeq  46416  mccl  46431  climsuse  46441  islptre  46452  lptioo2  46464  lptioo1  46465  islpcn  46470  fnlimfvre  46505  climbddf  46518  limsupubuzlem  46543  limsupmnfuzlem  46557  limsupequzmptlem  46559  limsupre3uzlem  46566  xlimcl  46653  cnrefiisplem  46660  xlimliminflimsup  46693  icccncfext  46718  cncfiooicclem1  46724  cncfiooicc  46725  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnprodlem1  46777  dvnprodlem3  46779  volioc  46803  itgioocnicc  46808  stoweidlem28  46859  stoweidlem57  46888  wallispilem3  46898  wallispilem4  46899  wallispi  46901  wallispi2lem1  46902  wallispi2  46904  stirlinglem12  46916  fourierdlem42  46980  fourierdlem48  46985  fourierdlem50  46987  fourierdlem52  46989  fourierdlem71  47008  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem76  47013  fourierdlem80  47017  fourierdlem93  47030  fourierdlem101  47038  fourierdlem103  47040  fourierdlem104  47041  fourierswlem  47061  fouriersw  47062  etransclem26  47091  etransclem37  47102  rrxsnicc  47131  saluncl  47148  intsaluni  47160  intsal  47161  salgencl  47163  salexct  47165  sssalgen  47166  salgenuni  47168  issalgend  47169  salgencntex  47174  subsaliuncllem  47188  subsaliuncl  47189  sge00  47207  sge0sn  47210  sge0cl  47212  sge0f1o  47213  sge0pnffigt  47227  sge0resplit  47237  sge0split  47240  sge0iunmptlemre  47246  sge0xaddlem2  47265  iundjiun  47291  meadjun  47293  meassle  47294  meadjiunlem  47296  meaiunlelem  47299  volmea  47305  caragenunidm  47339  omeunle  47347  omeiunltfirp  47350  caratheodorylem1  47357  caratheodory  47359  icoresmbl  47374  volicorescl  47384  ovncvrrp  47395  ovnsubaddlem2  47402  hoidmv1le  47425  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem5  47430  hoidmvle  47431  ovnhoilem2  47433  hspdifhsp  47447  hoiqssbllem3  47455  hspmbllem2  47458  ovolval4lem1  47480  ovnovollem3  47489  vonioolem1  47511  pimdecfgtioo  47548  pimincfltioo  47549  mbfresmf  47570  smfaddlem1  47594  smflimlem1  47602  smflimlem2  47603  smflimlem3  47604  smflim  47608  smfresal  47619  smfrec  47620  smfmullem4  47625  smfdiv  47628  smfpimbor1lem2  47630  smflimmpt  47641  smfsuplem1  47642  smfinflem  47648  smflimsuplem3  47653  smflimsuplem5  47655  smflimsuplem6  47656  smflimsuplem7  47657  smflimsupmpt  47660  smfliminflem  47661  smfliminfmpt  47663  simpcntrab  47701  quantgodelALT  47706  chnerlem1  47713  chnerlem2  47714  cos5teq  47747  lambert0  47758  lamberte  47759  aifftbifffaibif  47812  aifftbifffaibifff  47813  abciffcbatnabciffncba  47820  abciffcbatnabciffncbai  47821  nabctnabc  47822  confun4  47833  confun5  47834  plcofph  47835  pldofph  47836  plvcofph  47837  plvcofphax  47838  plvofpos  47839  dandysum2p2e4  47889  fresfo  47939  fcores  47958  3f1oss1  47966  3f1oss2  47967  funfocofob  47969  aiotaint  47982  dfaiota3  47983  ndmaovrcl  48095  tz6.12-afv2  48131  fvmptrabdm  48184  difmodm1lt  48256  uniimafveqt  48284  uniimaelsetpreimafv  48299  iccpartiun  48337  iccpartdisj  48340  ich2exprop  48374  ichnreuop  48375  prpair  48404  fmtnorec2lem  48448  dfodd5  48579  stgoldbwt  48695  sbgoldbb  48701  nnsum3primesle9  48713  nnsum4primeseven  48719  clnbgrcl  48740  clnbgrnvtx0  48746  clnbgredg  48759  grimuhgr  48806  isuspgrim0  48813  isuspgrimlem  48814  gricushgr  48836  grtriclwlk3  48864  isubgr3stgrlem1  48885  isubgr3stgrlem7  48891  uspgrlimlem2  48908  uspgrlimlem4  48910  grlimprclnbgr  48915  gpgusgralem  48975  gpg5order  48979  gpg5nbgrvtx03star  48999  gpg5nbgr3star  49000  gpgvtxdg3  49001  gpg5gricstgr3  49009  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  pgnbgreunbgr  49044  pgn4cyclex  49045  lmod0rng  49147  lidldomnnring  49154  ringcinvALTV  49228  altgsumbcALT  49286  ply1sclrmsm  49317  linccl  49347  lincvalsng  49349  lincvalpr  49351  lincdifsn  49357  linc1  49358  lincsum  49362  lincscm  49363  lindslinindsimp2lem5  49395  lincresunit3lem2  49413  2sphere  49682  resinsnALT  49802  tposideq  49817  clduni  49830  neircl  49834  funcrcl2  50008  funcrcl3  50009  funcf2lem2  50011  uprcl2  50118  uprcl3  50119  swapf2fval  50194  swapf1val  50196  fucofvalne  50254  thincn0eu  50360  isinito3  50429  mndtcobeq  50512  alsralrex  50744