Theorem biimpi 218

Description: Infer an implication from a logical equivalence. Inference associated with biimp 217. (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 217	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208

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

This theorem is referenced by:  sylbi  219  sylib  220  sylbb  221  biimpri  230  mpbi  232  biimtrid  244  imbitrdi  253  syl7bi  257  syl8ib  258  simplbi  500  simprbi  501  birani  507  bilani  508  anc2l  561  sylanb  590  sylanblc  598  sylan2b  603  pm3.37  817  pm2.53  862  orbi2i  923  pm2.32  934  pm2.76  942  pm3.1  1005  pm5.15  1026  pm5.16  1027  4exmid  1063  simp1bi  1159  simp2bi  1160  simp3bi  1161  syl3an1b  1423  syl3an2b  1424  syl3an3b  1425  nic-ax  1694  nfnt  1877  19.25  1901  nfimd  1915  19.37imv  1968  alcomimw  2064  sbbii  2110  nsb  2141  excomim  2198  stdpc5  2244  sb9i  2552  mo4  2594  2mo  2676  ax9ALT  2758  eleq2w2  2759  eqeq1d  2765  r19.37v  3189  rmoeq1  3399  elabgt  3632  euind  3688  reuind  3717  sbcimdv  3813  sbcg  3817  ra4v  3839  ra4  3840  csbied  3889  ssrmof  4005  elunnel1  4108  elunnel2  4109  unssd  4145  n0moeu  4313  eqeuel  4319  ss0  4357  iftrueb  4494  elinsn  4670  disjtp2  4676  rabsnif  4683  prprc  4727  elpwdifsn  4750  ssunsn2  4786  preqr1  4807  intss2  5066  disjxiun  5098  unisn2  5263  snexALT  5341  reusv3i  5362  snexOLD  5400  pocl  5564  brrelex12  5700  0nelrel0  5708  elrel  5771  exopxfr2  5817  dmxp  5906  xpssres  6005  elinxp  6006  imadisjlnd  6071  elimasni  6081  inisegn0  6088  imadifssran  6137  xpdifid  6154  xpdifcnvepel  6155  dmsnsnsn  6208  relcnvtrg  6255  xpco  6277  reuop  6281  predprc  6326  sucprc  6425  onunel  6454  iotaint  6500  iotanul  6502  funun  6568  funcnv3  6592  funimass1  6604  funssxp  6721  f0dom0  6749  dffv3  6864  dffv2  6963  fsneq  7017  fndmin  7027  sspreima  7050  iinpreima  7051  fveqressseq  7061  fsn2  7119  f1ounsn  7257  f12dfv  7258  f13dfv  7259  isoselem  7326  oprabidw  7428  oprabid  7429  ovima0  7576  sorpsscmpl  7718  unexgOLD  7733  abnex  7741  pwuncl  7754  ordsuci  7792  peano2  7871  1stval  7973  2ndval  7974  1stdm  8022  oprabco  8076  f1o2ndf1  8102  poxp  8109  frxp3  8132  suppval1  8147  fnsuppeq0  8173  frrlem4  8271  tz7.48lem  8413  tz7.49c  8418  ord1eln01  8466  ord2eln012  8467  undifixp  8917  bren2  8965  ensym  8985  en1uniel  9011  domunsn  9100  limenpsi  9125  findcard2  9134  unfi  9140  pwssfi  9146  php4  9179  isinf  9210  en2  9225  fiint  9272  rneqdmfinf1o  9277  elfiun  9377  marypha1lem  9380  supval2  9402  eqinf  9432  brwdom2  9522  zfreg  9545  tcmin  9695  frmin  9708  prwf  9770  r1pw  9804  rankuni2b  9812  rankr1id  9821  djuun  9885  cardval3  9911  ficardom  9920  cardmin2  9958  isinfcard  10049  iscard3  10050  alephval3  10067  dfac9  10094  kmlem6  10113  fin23lem29  10299  fin23lem30  10300  isf32lem11  10321  isfin1-3  10344  fin45  10350  fin1a2lem12  10369  fin1a2lem13  10370  axcc2lem  10394  dominf  10403  axdc4lem  10413  dominfac  10532  pwcfsdom  10542  cfpwsdom  10543  tskuni  10742  wfgru  10775  rpregt0  13009  supxrun  13320  elicore  13403  xrge0nre  13458  elfz1end  13560  elfzonlteqm1  13748  modfzo0difsn  13957  fzennn  13982  cardfz  13984  fsuppmapnn0fiub0  14007  ser0  14068  crreczi  14242  faclbnd  14304  bcn1  14327  hashrabsn01  14387  hashge0  14401  prsshashgt1  14424  hashssdif  14426  hashdifpr  14429  hashsn01  14430  hashgt23el  14438  hashpw  14450  hashres  14452  hash3tpexb  14508  ccatw2s1p1  14651  swrdswrd  14719  swrdccatin2  14743  pfxccatpfx1  14750  repsundef  14785  trclublem  15009  reltrclfv  15031  dmtrclfv  15032  cau3lem  15383  harmonic  15890  mertenslem2  15916  prodf1  15922  fprodfac  16004  rpnnen2lem12  16258  sqrt2irr0  16284  lcmftp  16671  lcmfunsnlem2lem1  16673  lcmfunsnlem2lem2  16674  prmind2  16720  prm2orodd  16726  pceq0  16908  prmreclem6  16958  0ram  17057  ram0  17059  cshwsiun  17136  ressbas2  17275  ressinbas  17282  ressval3d  17283  catpropd  17742  initoid  18035  termoid  18036  initoeu2lem0  18047  arwhoma  18079  joinfval  18404  meetfval  18418  lubun  18548  psssdm  18615  ex-chn1  18670  ex-chn2  18671  ismgmn0  18677  plusfeq  18683  idresefmnd  18934  snsymgefmndeq  19436  fvcosymgeq  19470  pmtrprfv3  19495  pmtr3ncomlem1  19514  ablsubadd23  19854  ablsubsub23  19865  cygabl  19932  gsummptfzsplitl  19974  gsum2dlem1  20011  gsum2dlem2  20012  gsum2d  20013  rng1zrlem  20228  opprnzr  20573  cntzsubrng  20618  ringcinv  20722  opprdomn  20769  drngmcl  20801  staffn  20893  scafeq  20950  lbsexg  21235  rngridlmcl  21288  rnglidl1  21303  df2idl2  21328  2idlss  21333  prmirred  21527  frgpcyg  21626  ipfeq  21703  dsmmbas2  21790  zlmassa  21956  ply1bascl2  22267  lply1binom  22374  mamufacex  22457  matsubgcell  22495  matinvgcell  22496  matepmcl  22523  matepm2cl  22524  marrepcl  22625  marepvcl  22630  mulmarep1el  22633  mulmarep1gsum1  22634  mulmarep1gsum2  22635  nfimdetndef  22650  mdetfval1  22651  m1detdiag  22658  mdetdiag  22660  slesolinvbi  22742  pmatcoe1fsupp  22762  mat2pmatbas  22787  mat2pmatmul  22792  m2cpminvid2lem  22815  monmatcollpw  22840  pm2mpf1  22860  pm2mpghm  22877  cayhamlem1  22927  isbasis3g  23010  isopn2  23093  ntrval2  23112  toponmre  23154  innei  23186  restcld  23233  restcldi  23234  neitr  23241  discmp  23459  cmpsublem  23460  cmpsub  23461  ssref  23573  dissnref  23589  ptcnp  23683  imasnopn  23751  imasncld  23752  imasncls  23753  kqf  23808  fbun  23901  opnfbas  23903  supfil  23956  ufprim  23970  acufl  23978  filufint  23981  ufldom  24023  hausflf2  24059  alexsubALTlem4  24111  cnextfval  24123  cnextfun  24125  cnextfres1  24129  efmndtmd  24162  trust  24290  ustuqtop1  24302  metustid  24615  metustbl  24627  restmetu  24631  zlmclm  25175  cphassr  25275  ehleudisval  25482  ovolun  25562  vitalilem2  25672  dvcobr  26009  dvmptfsum  26038  rolle  26053  dvfsumlem2  26090  plyn0mulidp  26346  ulmcaulem  26458  logfac  26667  logno1  26702  logreclem  26828  prmorcht  27243  pclogsum  27280  gausslemma2dlem0i  27429  gausslemma2dlem1a  27430  2lgslem1c  27458  2sqlem10  27493  chto1lb  27543  cutsval  27874  addsproplem2  28064  oncutlt  28358  n0s0suc  28436  tgjustf  28643  tgldimor  28672  axcontlem7  29172  lfgredgge2  29326  edgupgr  29336  ausgrusgrb  29367  ausgrumgri  29369  uspgredg2vlem  29425  uspgredg2v  29426  usgredg2vlem2  29428  usgredg2v  29429  ushgredgedg  29431  ushgredgedgloop  29433  griedg0ssusgr  29467  umgrres1lem  29512  upgrres1  29515  nbgrcl  29537  nbgrnvtx0  29541  nbuhgr  29545  nbuhgr2vtx1edgb  29554  edgnbusgreu  29569  nb3grprlem2  29583  nb3grpr2  29585  nb3gr2nb  29586  cplgr2vpr  29635  cplgr3v  29637  vtxdumgrval  29688  umgr2v2evtxel  29724  usgrvd0nedg  29735  finsumvtxdg2ssteplem4  29750  wlk1walk  29840  wlk0prc  29854  wlkp1lem8  29880  wlkp1  29881  spthdep  29935  usgr2pthlem  29964  usgr2pth  29965  crctprop  29993  cyclprop  29994  cyclnumvtx  30001  crctcshwlkn0  30022  wwlknllvtx  30047  wlkiswwlks1  30068  wlkswwlksf1o  30080  wwlksnextproplem3  30112  wwlksnwwlksnon  30116  umgr2wlkon  30151  wwlks2onv  30154  elwspths2on  30163  elwspths2onw  30164  elwwlks2  30170  elwspths2spth  30171  rusgrnumwwlks  30178  clwlkclwwlklem2a4  30200  clwlkclwwlklem2  30203  clwlkclwwlkf  30211  erclwwlkref  30223  erclwwlknref  30272  erclwwlknsym  30273  erclwwlkntr  30274  hashecclwwlkn1  30280  umgrhashecclwwlk  30281  clwlknf1oclwwlknlem1  30284  clwwlknon1  30300  clwwlknon1nloop  30302  clwwlkvbij  30316  0clwlkv  30334  uhgr3cyclex  30385  umgr3cyclex  30386  vdn0conngrumgrv2  30399  eupthi  30406  eucrctshift  30446  frcond1  30469  frcond4  30473  frgr3v  30478  3vfriswmgr  30481  1to2vfriswmgr  30482  1to3vfriswmgr  30483  2pthfrgr  30487  4cycl2v2nb  30492  n4cyclfrgr  30494  frgrnbnb  30496  frgrwopreglem4a  30513  clwlknon2num  30571  numclwwlkqhash  30578  frgrreg  30597  frgrregord013  30598  ex-ceil  30651  grpoidinvlem3  30710  nmlno0lem  30997  blocni  31009  pythi  31054  normpythi  31346  shmodsi  31593  pjchi  31636  chlubii  31676  osumi  31846  nmlnop0iALT  32199  cnlnssadj  32284  nmopcoi  32299  mdbr3  32501  mdbr4  32502  ssmd1  32515  dmdsl3  32519  mdexchi  32539  atssma  32582  atoml2i  32587  chirredlem3  32596  mdsymlem1  32607  dmdbr6ati  32627  dmdbr7ati  32628  cdjreui  32636  cdj3lem2b  32641  addltmulALT  32650  difuncomp  32754  iundifdif  32763  imadifxp  32802  fresf1o  32834  2ndimaxp  32849  acunirnmpt2  32863  suppiniseg  32889  fressupp  32891  fdifsuppconst  32892  ressupprn  32893  disjdsct  32906  1stpreimas  32909  preiman0  32913  resf1o  32933  xrge0addge  32961  xlt2addrd  32962  fz2ssnn0  32988  f1ocnt  33003  elq2  33015  nexple  33036  s2rnOLD  33123  s3rnOLD  33125  gsummpt2d  33230  gsumfs2d  33242  gsumwun  33257  psgnfzto1stlem  33281  fzto1st  33284  psgnfzto1st  33286  cycpmco2f1  33305  cycpmco2rn  33306  cycpmco2lem7  33313  elrgspn  33428  elrgspnsubrunlem2  33430  elrlocbasi  33449  ricnzr1  33473  sdrginvcl  33488  qsxpid  33549  nsgqusf1olem2  33601  elrspunidl  33615  ssdifidlprm  33646  ssmxidl  33663  selvply1rhmlem2  33819  lbsdiflsp0  33924  fldextfld1  33945  fldextfld2  33946  constrconj  34043  constrllcllem  34050  constrlccllem  34051  constrcccllem  34052  submat1n  34103  submatres  34104  locfinreflem  34138  ldlfcntref  34152  zarclsun  34168  zarclsiin  34169  zarclsint  34170  zarcmplem  34179  mndpluscn  34224  pnfneige0  34249  pl1cn  34253  gsumesum  34357  esumcst  34361  esumrnmpt2  34366  esumcvgre  34389  esum2d  34391  pwsiga  34428  ldsysgenld  34458  measxun2  34508  volmeas  34529  ddemeas  34534  aean  34542  mbfmfun  34551  1stmbfm  34558  2ndmbfm  34559  omssubadd  34598  carsgclctunlem1  34615  sibfof  34638  eulerpartlemmf  34673  probun  34717  dstfrvclim1  34776  coinfliprv  34781  ballotlem2  34787  ballotlemic  34805  ballotlem1c  34806  signstres  34870  bnj529  35038  bnj1379  35126  bnj1424  35134  bnj1436  35135  bnj607  35212  bnj908  35227  bnj1097  35277  bnj1118  35280  bnj1128  35286  bnj1145  35289  bnj1154  35295  bnj1174  35299  bnj1189  35305  bnj1417  35337  axprALT2  35406  tz9.1regs  35431  axsepg2  35437  axsepg4  35440  0nn0m1nnn0  35464  lfuhgr2  35470  cusgr3cyclex  35487  cvmliftlem10  35645  satfv1  35714  fmlasuc0  35735  satffunlem2lem1  35755  mrsub0  35867  mrsubccat  35869  mrsubcn  35870  bcprod  36089  socnv  36115  dfon2lem3  36134  dfon2lem7  36138  dfon2lem8  36139  rdgprc0  36142  fvsingle  36269  unisnif  36274  funpartlem  36293  hfun  36529  ss-ax8  36586  trer  36677  clsun  36689  opnregcld  36691  cldregopn  36692  df3nandALT1  36760  lukshef-ax2  36776  nandsym1  36783  weiunfr  36828  dfttc4lem2  36890  knoppndvlem9  36959  bj-mt2bi  37011  bj-gl4  37039  bj-babygodel  37047  bj-babylob  37048  bj-ssbid2ALT  37136  bj-nfext  37190  bj-1upln0  37495  bj-snex  37521  eleq2w2ALT  37533  bj-brrelex12ALT  37553  bj-restsnid  37578  bj-snmooreb  37605  bj-opelrelex  37637  bj-inftyexpitaudisj  37698  bj-inftyexpidisj  37703  bj-elccinfty  37707  finorwe  37877  ctbssinf  37901  fvineqsnf1  37905  pibt2  37912  wl-ifpimpr  37961  wl-ifp4impr  37962  wl-1xor  37977  wl-1mintru1  37983  lindsadd  38113  lindsenlbs  38115  poimirlem9  38129  poimirlem13  38133  poimirlem14  38134  poimirlem25  38145  poimirlem26  38146  mblfinlem2  38158  mblfinlem3  38159  mblfinlem4  38160  ismblfin  38161  mbfresfi  38166  ftc1cnnc  38192  dvasin  38204  fnopabco  38223  frinfm  38235  caushft  38261  bndss  38286  notornotel1  38595  tsbi2  38634  rabeq12f  38657  relcnveq3  38827  relcnveq2  38829  cnvref4  38850  ralrnmo  38861  raldmqsmo  38863  disjressuc2  38911  cnvcosseq  39027  symrelcoss3  39055  dfrefrels2  39093  dfrefrel2  39095  dfcnvrefrels2  39108  dfcnvrefrel2  39110  dfsymrels2  39125  elrelscnveq3  39127  dfsymrel2  39133  symrefref2  39147  dftrrels2  39159  dftrrel2  39161  n0elim  39235  disjimeceqim  39304  membpartlem19  39414  axc11n-16  39563  glbconN  40002  paddssat  40439  pclunN  40523  paddunN  40552  poldmj1N  40553  ltrnnid  40761  dibglbN  41791  mndmolinv  42713  primrootsunit1  42715  primrootscoprmpow  42717  primrootscoprbij  42720  aks6d1c2lem4  42745  aks6d1c2  42748  aks6d1c5lem3  42755  deg1gprod  42758  sticksstones3  42766  sticksstones11  42774  sticksstones12a  42775  sticksstones12  42776  sticksstones13  42777  aks6d1c6isolem1  42792  aks6d1c6lem5  42795  grpods  42812  unitscyglem2  42814  unitscyglem3  42815  unitscyglem4  42816  aks5lem7  42818  exbiii  42828  sn-0ne2  43016  sn-0lt1  43098  istopclsd  43282  pellex  43413  monotoddzzfi  43520  jm2.23  43574  expdioph  43601  wopprc  43608  kelac1  43641  dfac21  43644  lsmfgcl  43652  pwssplit4  43667  isnumbasgrp  43685  dgraalem  43723  ordnexbtwnsuc  43845  cantnfresb  43902  dflim5  43907  rp-tfslim  43931  ifpbi1  44054  rp-fakeanorass  44090  rp-isfinite5  44094  iscard4  44110  minregex  44111  pr2cv  44125  superficl  44144  ssuncl  44147  sssymdifcl  44149  relintab  44160  cnvssb  44163  cotrintab  44191  clcnvlem  44200  cnvtrrel  44247  brfvrcld2  44269  relexpxpmin  44294  relexpaddss  44295  unhe1  44362  frege55lem1b  44472  frege58bid  44479  frege92  44532  uneqsn  44602  ntrk2imkb  44614  neik0pk1imk0  44624  gneispace  44711  k0004lem2  44725  k0004val0  44731  ismnushort  44878  pm10.12  44935  pm11.61  44970  sbiota1  45011  bi1imp  45059  bi2imp  45060  bi3impb  45061  bi3impa  45062  bi13impib  45064  bi123impib  45065  bi13impia  45066  bi123impia  45067  bi13imp23  45069  bi13imp2  45070  bi12imp3  45071  tratrb  45113  dfvd1imp  45152  dfvd2imp  45180  e1bi  45206  e2bi  45209  e3bi  45314  3ornot23VD  45423  3impexpbicomVD  45433  3impexpbicomiVD  45434  tratrbVD  45437  ssralv2VD  45442  equncomiVD  45445  truniALTVD  45454  ee33VD  45455  onfrALTlem3VD  45463  onfrALTlem2VD  45465  onfrALTlem1VD  45466  onfrALTVD  45467  relopabVD  45477  2uasbanhVD  45487  vk15.4jVD  45490  unisnALT  45502  chordthmALT  45509  iunconnlem2  45511  wfaxpow  45574  wfaxun  45576  fnchoice  45610  uzwo4  45634  inabs3  45637  rexanuz3  45675  disjrnmpt2  45767  disjinfi  45771  iunmapsn  45794  ssfiunibd  45889  iuneqfzuzlem  45911  iuneqfzuz  45912  xrge0ge0  45924  xrssre  45925  infrpge  45928  allbutfi  45969  supxrunb3  45975  eluzelz2  45978  uz0  45987  allbutfiinf  45995  infxrunb3rnmpt  46003  uzublem  46005  uzub  46006  uzid3  46010  infxrlesupxr  46011  infrpgernmpt  46040  supminfxrrnmpt  46046  rexanuz2nf  46067  eliocre  46086  lbioc  46090  ioonct  46114  uzinico  46136  fsumiunss  46152  fmuldfeq  46160  mccl  46175  climsuse  46185  islptre  46196  lptioo2  46208  lptioo1  46209  islpcn  46214  fnlimfvre  46249  climbddf  46262  limsupubuzlem  46287  limsupmnfuzlem  46301  limsupequzmptlem  46303  limsupre3uzlem  46310  xlimcl  46397  cnrefiisplem  46404  xlimliminflimsup  46437  icccncfext  46462  cncfiooicclem1  46468  cncfiooicc  46469  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  dvnprodlem1  46521  dvnprodlem3  46523  volioc  46547  itgioocnicc  46552  stoweidlem28  46603  stoweidlem57  46632  wallispilem3  46642  wallispilem4  46643  wallispi  46645  wallispi2lem1  46646  wallispi2  46648  stirlinglem12  46660  fourierdlem42  46724  fourierdlem48  46729  fourierdlem50  46731  fourierdlem52  46733  fourierdlem71  46752  fourierdlem73  46754  fourierdlem74  46755  fourierdlem75  46756  fourierdlem76  46757  fourierdlem80  46761  fourierdlem93  46774  fourierdlem101  46782  fourierdlem103  46784  fourierdlem104  46785  fourierswlem  46805  fouriersw  46806  etransclem26  46835  etransclem37  46846  rrxsnicc  46875  saluncl  46892  intsaluni  46904  intsal  46905  salgencl  46907  salexct  46909  sssalgen  46910  salgenuni  46912  issalgend  46913  salgencntex  46918  subsaliuncllem  46932  subsaliuncl  46933  sge00  46951  sge0sn  46954  sge0cl  46956  sge0f1o  46957  sge0pnffigt  46971  sge0resplit  46981  sge0split  46984  sge0iunmptlemre  46990  sge0xaddlem2  47009  iundjiun  47035  meadjun  47037  meassle  47038  meadjiunlem  47040  meaiunlelem  47043  volmea  47049  caragenunidm  47083  omeunle  47091  omeiunltfirp  47094  caratheodorylem1  47101  caratheodory  47103  icoresmbl  47118  volicorescl  47128  ovncvrrp  47139  ovnsubaddlem2  47146  hoidmv1le  47169  hoidmvlelem1  47170  hoidmvlelem2  47171  hoidmvlelem5  47174  hoidmvle  47175  ovnhoilem2  47177  hspdifhsp  47191  hoiqssbllem3  47199  hspmbllem2  47202  ovolval4lem1  47224  ovnovollem3  47233  vonioolem1  47255  pimdecfgtioo  47292  pimincfltioo  47293  mbfresmf  47314  smfaddlem1  47338  smflimlem1  47346  smflimlem2  47347  smflimlem3  47348  smflim  47352  smfresal  47363  smfrec  47364  smfmullem4  47369  smfdiv  47372  smfpimbor1lem2  47374  smflimmpt  47385  smfsuplem1  47386  smfinflem  47392  smflimsuplem3  47397  smflimsuplem5  47399  smflimsuplem6  47400  smflimsuplem7  47401  smflimsupmpt  47404  smfliminflem  47405  smfliminfmpt  47407  simpcntrab  47445  quantgodelALT  47450  chnerlem1  47459  chnerlem2  47460  cos5teq  47475  lambert0  47482  lamberte  47483  aifftbifffaibif  47516  aifftbifffaibifff  47517  abciffcbatnabciffncba  47524  abciffcbatnabciffncbai  47525  nabctnabc  47526  confun4  47537  confun5  47538  plcofph  47539  pldofph  47540  plvcofph  47541  plvcofphax  47542  plvofpos  47543  dandysum2p2e4  47593  fresfo  47643  fcores  47662  3f1oss1  47670  3f1oss2  47671  funfocofob  47673  aiotaint  47686  dfaiota3  47687  ndmaovrcl  47799  tz6.12-afv2  47835  fvmptrabdm  47888  difmodm1lt  47960  uniimafveqt  47988  uniimaelsetpreimafv  48003  iccpartiun  48041  iccpartdisj  48044  ich2exprop  48078  ichnreuop  48079  prpair  48108  fmtnorec2lem  48152  dfodd5  48283  stgoldbwt  48399  sbgoldbb  48405  nnsum3primesle9  48417  nnsum4primeseven  48423  clnbgrcl  48444  clnbgrnvtx0  48450  clnbgredg  48463  grimuhgr  48510  isuspgrim0  48517  isuspgrimlem  48518  gricushgr  48540  grtriclwlk3  48568  isubgr3stgrlem1  48589  isubgr3stgrlem7  48595  uspgrlimlem2  48612  uspgrlimlem4  48614  grlimprclnbgr  48619  gpgusgralem  48679  gpg5order  48683  gpg5nbgrvtx03star  48703  gpg5nbgr3star  48704  gpgvtxdg3  48705  gpg5gricstgr3  48713  pgnbgreunbgrlem3  48741  pgnbgreunbgrlem6  48747  pgnbgreunbgr  48748  pgn4cyclex  48749  lmod0rng  48852  lidldomnnring  48859  ringcinvALTV  48933  altgsumbcALT  48976  ply1sclrmsm  49007  linccl  49037  lincvalsng  49039  lincvalpr  49041  lincdifsn  49047  linc1  49048  lincsum  49052  lincscm  49053  lindslinindsimp2lem5  49085  lincresunit3lem2  49103  2sphere  49372  resinsnALT  49495  tposideq  49510  clduni  49523  neircl  49527  funcrcl2  49701  funcrcl3  49702  funcf2lem2  49704  uprcl2  49811  uprcl3  49812  swapf2fval  49887  swapf1val  49889  fucofvalne  49947  thincn0eu  50053  isinito3  50122  mndtcbas2  50205