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  499  simprbi  500  birani  506  bilani  507  anc2l  560  sylanb  589  sylanblc  597  sylan2b  602  pm3.37  815  pm2.53  860  orbi2i  921  pm2.32  932  pm2.76  940  pm3.1  1002  pm5.15  1023  pm5.16  1024  4exmid  1060  simp1bi  1154  simp2bi  1155  simp3bi  1156  syl3an1b  1414  syl3an2b  1415  syl3an3b  1416  nic-ax  1683  nfnt  1866  19.25  1890  nfimd  1904  19.37imv  1957  alcomimw  2053  sbbii  2099  nsb  2130  excomim  2187  stdpc5  2233  sb9i  2541  mo4  2583  2mo  2665  ax9ALT  2747  eleq2w2  2748  eqeq1d  2754  r19.37v  3178  rmoeq1  3388  elabgt  3622  euind  3677  reuind  3706  sbcimdv  3803  sbcg  3807  ra4v  3829  ra4  3830  csbied  3879  ssrmof  3995  elunnel1  4098  elunnel2  4099  unssd  4135  n0moeu  4302  eqeuel  4308  ss0  4346  iftrueb  4483  elinsn  4659  disjtp2  4665  rabsnif  4672  prprc  4716  elpwdifsn  4739  ssunsn2  4775  preqr1  4796  intss2  5055  disjxiun  5087  unisn2  5252  snexALT  5330  reusv3i  5351  snexOLD  5389  pocl  5552  brrelex12  5688  0nelrel0  5696  elrel  5759  exopxfr2  5805  dmxp  5894  xpssres  5993  elinxp  5994  imadisjlnd  6056  elimasni  6066  inisegn0  6073  imadifssran  6122  xpdifid  6139  dmsnsnsn  6192  relcnvtrg  6239  xpco  6261  reuop  6265  predprc  6310  sucprc  6409  onunel  6438  iotaint  6484  iotanul  6486  funun  6552  funcnv3  6576  funimass1  6588  funssxp  6705  f0dom0  6733  dffv3  6848  dffv2  6947  fsneq  7001  fndmin  7011  sspreima  7034  iinpreima  7035  fveqressseq  7045  fsn2  7103  f1ounsn  7241  f12dfv  7242  f13dfv  7243  isoselem  7310  oprabidw  7412  oprabid  7413  ovima0  7560  sorpsscmpl  7702  unexgOLD  7717  abnex  7725  pwuncl  7738  ordsuci  7776  peano2  7855  1stval  7957  2ndval  7958  1stdm  8006  oprabco  8059  f1o2ndf1  8085  poxp  8092  frxp3  8115  suppval1  8130  fnsuppeq0  8156  frrlem4  8254  tz7.48lem  8396  tz7.49c  8401  ord1eln01  8449  ord2eln012  8450  undifixp  8901  bren2  8949  ensym  8969  en1uniel  8995  domunsn  9084  limenpsi  9109  findcard2  9118  unfi  9124  pwssfi  9130  php4  9163  isinf  9194  en2  9209  fiint  9256  rneqdmfinf1o  9262  elfiun  9362  marypha1lem  9365  supval2  9387  eqinf  9417  brwdom2  9507  zfreg  9530  tcmin  9680  frmin  9693  prwf  9755  r1pw  9789  rankuni2b  9797  rankr1id  9806  djuun  9870  cardval3  9896  ficardom  9905  cardmin2  9943  isinfcard  10034  iscard3  10035  alephval3  10052  dfac9  10079  kmlem6  10098  fin23lem29  10284  fin23lem30  10285  isf32lem11  10306  isfin1-3  10329  fin45  10335  fin1a2lem12  10354  fin1a2lem13  10355  axcc2lem  10379  dominf  10388  axdc4lem  10398  dominfac  10517  pwcfsdom  10527  cfpwsdom  10528  tskuni  10727  wfgru  10760  rpregt0  12994  supxrun  13305  elicore  13388  xrge0nre  13443  elfz1end  13545  elfzonlteqm1  13733  modfzo0difsn  13942  fzennn  13967  cardfz  13969  fsuppmapnn0fiub0  13992  ser0  14053  crreczi  14227  faclbnd  14289  bcn1  14312  hashrabsn01  14372  hashge0  14386  prsshashgt1  14409  hashssdif  14411  hashdifpr  14414  hashsn01  14415  hashgt23el  14423  hashpw  14435  hashres  14437  hash3tpexb  14493  ccatw2s1p1  14636  swrdswrd  14704  swrdccatin2  14728  pfxccatpfx1  14735  repsundef  14770  trclublem  14994  reltrclfv  15016  dmtrclfv  15017  cau3lem  15354  harmonic  15861  mertenslem2  15887  prodf1  15893  fprodfac  15975  rpnnen2lem12  16229  sqrt2irr0  16255  lcmftp  16642  lcmfunsnlem2lem1  16644  lcmfunsnlem2lem2  16645  prmind2  16691  prm2orodd  16697  pceq0  16879  prmreclem6  16929  0ram  17028  ram0  17030  cshwsiun  17107  ressbas2  17246  ressinbas  17253  ressval3d  17254  catpropd  17713  initoid  18006  termoid  18007  initoeu2lem0  18018  arwhoma  18050  joinfval  18375  meetfval  18389  lubun  18519  psssdm  18586  ex-chn1  18641  ex-chn2  18642  ismgmn0  18648  plusfeq  18654  idresefmnd  18905  snsymgefmndeq  19407  fvcosymgeq  19441  pmtrprfv3  19466  pmtr3ncomlem1  19485  ablsubadd23  19825  ablsubsub23  19836  cygabl  19903  gsummptfzsplitl  19945  gsum2dlem1  19982  gsum2dlem2  19983  gsum2d  19984  srg1zr  20233  opprnzr  20540  cntzsubrng  20585  ringcinv  20689  opprdomn  20736  drngmcl  20768  staffn  20861  scafeq  20918  lbsexg  21203  rngridlmcl  21256  rnglidl1  21271  df2idl2  21296  2idlss  21301  prmirred  21495  frgpcyg  21594  ipfeq  21671  dsmmbas2  21758  zlmassa  21924  ply1bascl2  22235  lply1binom  22342  mamufacex  22425  matsubgcell  22463  matinvgcell  22464  matepmcl  22491  matepm2cl  22492  marrepcl  22593  marepvcl  22598  mulmarep1el  22601  mulmarep1gsum1  22602  mulmarep1gsum2  22603  nfimdetndef  22618  mdetfval1  22619  m1detdiag  22626  mdetdiag  22628  slesolinvbi  22710  pmatcoe1fsupp  22730  mat2pmatbas  22755  mat2pmatmul  22760  m2cpminvid2lem  22783  monmatcollpw  22808  pm2mpf1  22828  pm2mpghm  22845  cayhamlem1  22895  isbasis3g  22978  isopn2  23061  ntrval2  23080  toponmre  23122  innei  23154  restcld  23201  restcldi  23202  neitr  23209  discmp  23427  cmpsublem  23428  cmpsub  23429  ssref  23541  dissnref  23557  ptcnp  23651  imasnopn  23719  imasncld  23720  imasncls  23721  kqf  23776  fbun  23869  opnfbas  23871  supfil  23924  ufprim  23938  acufl  23946  filufint  23949  ufldom  23991  hausflf2  24027  alexsubALTlem4  24079  cnextfval  24091  cnextfun  24093  cnextfres1  24097  efmndtmd  24130  trust  24258  ustuqtop1  24270  metustid  24583  metustbl  24595  restmetu  24599  zlmclm  25143  cphassr  25243  ehleudisval  25450  ovolun  25530  vitalilem2  25640  dvcobr  25977  dvmptfsum  26006  rolle  26021  dvfsumlem2  26058  ulmcaulem  26423  logfac  26632  logno1  26667  logreclem  26793  prmorcht  27208  pclogsum  27245  gausslemma2dlem0i  27394  gausslemma2dlem1a  27395  2lgslem1c  27423  2sqlem10  27458  chto1lb  27508  cutsval  27839  addsproplem2  28029  oncutlt  28323  n0s0suc  28401  tgjustf  28608  tgldimor  28637  axcontlem7  29106  lfgredgge2  29260  edgupgr  29270  ausgrusgrb  29301  ausgrumgri  29303  uspgredg2vlem  29359  uspgredg2v  29360  usgredg2vlem2  29362  usgredg2v  29363  ushgredgedg  29365  ushgredgedgloop  29367  griedg0ssusgr  29401  umgrres1lem  29446  upgrres1  29449  nbgrcl  29471  nbgrnvtx0  29475  nbuhgr  29479  nbuhgr2vtx1edgb  29488  edgnbusgreu  29503  nb3grprlem2  29517  nb3grpr2  29519  nb3gr2nb  29520  cplgr2vpr  29569  cplgr3v  29571  vtxdumgrval  29622  umgr2v2evtxel  29658  usgrvd0nedg  29669  finsumvtxdg2ssteplem4  29684  wlk1walk  29774  wlk0prc  29788  wlkp1lem8  29814  wlkp1  29815  spthdep  29869  usgr2pthlem  29898  usgr2pth  29899  crctprop  29927  cyclprop  29928  cyclnumvtx  29935  crctcshwlkn0  29956  wwlknllvtx  29981  wlkiswwlks1  30002  wlkswwlksf1o  30014  wwlksnextproplem3  30046  wwlksnwwlksnon  30050  umgr2wlkon  30085  wwlks2onv  30088  elwspths2on  30097  elwspths2onw  30098  elwwlks2  30104  elwspths2spth  30105  rusgrnumwwlks  30112  clwlkclwwlklem2a4  30134  clwlkclwwlklem2  30137  clwlkclwwlkf  30145  erclwwlkref  30157  erclwwlknref  30206  erclwwlknsym  30207  erclwwlkntr  30208  hashecclwwlkn1  30214  umgrhashecclwwlk  30215  clwlknf1oclwwlknlem1  30218  clwwlknon1  30234  clwwlknon1nloop  30236  clwwlkvbij  30250  0clwlkv  30268  uhgr3cyclex  30319  umgr3cyclex  30320  vdn0conngrumgrv2  30333  eupthi  30340  eucrctshift  30380  frcond1  30403  frcond4  30407  frgr3v  30412  3vfriswmgr  30415  1to2vfriswmgr  30416  1to3vfriswmgr  30417  2pthfrgr  30421  4cycl2v2nb  30426  n4cyclfrgr  30428  frgrnbnb  30430  frgrwopreglem4a  30447  clwlknon2num  30505  numclwwlkqhash  30512  frgrreg  30531  frgrregord013  30532  ex-ceil  30585  grpoidinvlem3  30644  nmlno0lem  30931  blocni  30943  pythi  30988  normpythi  31280  shmodsi  31527  pjchi  31570  chlubii  31610  osumi  31780  nmlnop0iALT  32133  cnlnssadj  32218  nmopcoi  32233  mdbr3  32435  mdbr4  32436  ssmd1  32449  dmdsl3  32453  mdexchi  32473  atssma  32516  atoml2i  32521  chirredlem3  32530  mdsymlem1  32541  dmdbr6ati  32561  dmdbr7ati  32562  cdjreui  32570  cdj3lem2b  32575  addltmulALT  32584  difuncomp  32691  iundifdif  32700  imadifxp  32739  fresf1o  32772  2ndimaxp  32787  acunirnmpt2  32801  suppiniseg  32827  fressupp  32829  fdifsuppconst  32830  ressupprn  32831  disjdsct  32844  1stpreimas  32847  preiman0  32851  resf1o  32871  xrge0addge  32899  xlt2addrd  32900  fz2ssnn0  32926  f1ocnt  32941  elq2  32953  nexple  32985  s2rnOLD  33072  s3rnOLD  33074  gsummpt2d  33179  gsumfs2d  33191  gsumwun  33206  psgnfzto1stlem  33230  fzto1st  33233  psgnfzto1st  33235  cycpmco2f1  33254  cycpmco2rn  33255  cycpmco2lem7  33262  elrgspn  33376  elrgspnsubrunlem2  33378  elrlocbasi  33396  ricnzr1  33418  sdrginvcl  33433  qsxpid  33494  nsgqusf1olem2  33546  elrspunidl  33560  ssdifidlprm  33590  ssmxidl  33606  selvply1rhmlem2  33762  lbsdiflsp0  33867  fldextfld1  33888  fldextfld2  33889  constrconj  33986  constrllcllem  33993  constrlccllem  33994  constrcccllem  33995  submat1n  34046  submatres  34047  locfinreflem  34081  ldlfcntref  34095  zarclsun  34111  zarclsiin  34112  zarclsint  34113  zarcmplem  34122  mndpluscn  34167  pnfneige0  34192  pl1cn  34196  gsumesum  34300  esumcst  34304  esumrnmpt2  34309  esumcvgre  34332  esum2d  34334  pwsiga  34371  ldsysgenld  34401  measxun2  34451  volmeas  34472  ddemeas  34477  aean  34485  mbfmfun  34494  1stmbfm  34501  2ndmbfm  34502  omssubadd  34541  carsgclctunlem1  34558  sibfof  34581  eulerpartlemmf  34616  probun  34660  dstfrvclim1  34719  coinfliprv  34724  ballotlem2  34730  ballotlemic  34748  ballotlem1c  34749  plymulx0  34788  signstres  34816  bnj529  34984  bnj1379  35072  bnj1424  35080  bnj1436  35081  bnj607  35158  bnj908  35173  bnj1097  35223  bnj1118  35226  bnj1128  35232  bnj1145  35235  bnj1154  35241  bnj1174  35245  bnj1189  35251  bnj1417  35283  axprALT2  35350  tz9.1regs  35375  axsepg2  35381  axsepg4  35384  0nn0m1nnn0  35401  lfuhgr2  35407  cusgr3cyclex  35424  cvmliftlem10  35582  satfv1  35651  fmlasuc0  35672  satffunlem2lem1  35692  mrsub0  35804  mrsubccat  35806  mrsubcn  35807  bcprod  36026  socnv  36052  dfon2lem3  36071  dfon2lem7  36075  dfon2lem8  36076  rdgprc0  36079  fvsingle  36206  unisnif  36211  funpartlem  36230  hfun  36466  ss-ax8  36523  trer  36614  clsun  36626  opnregcld  36628  cldregopn  36629  df3nandALT1  36697  lukshef-ax2  36713  nandsym1  36720  weiunfr  36765  dfttc4lem2  36827  knoppndvlem9  36896  bj-mt2bi  36948  bj-gl4  36976  bj-babygodel  36984  bj-babylob  36985  bj-ssbid2ALT  37073  bj-nfext  37127  bj-1upln0  37432  bj-snex  37458  eleq2w2ALT  37470  bj-brrelex12ALT  37490  bj-restsnid  37515  bj-snmooreb  37542  bj-opelrelex  37574  bj-inftyexpitaudisj  37635  bj-inftyexpidisj  37640  bj-elccinfty  37644  finorwe  37814  ctbssinf  37838  fvineqsnf1  37842  pibt2  37849  wl-ifpimpr  37898  wl-ifp4impr  37899  wl-1xor  37914  wl-1mintru1  37920  lindsadd  38050  lindsenlbs  38052  poimirlem9  38066  poimirlem13  38070  poimirlem14  38071  poimirlem25  38082  poimirlem26  38083  mblfinlem2  38095  mblfinlem3  38096  mblfinlem4  38097  ismblfin  38098  mbfresfi  38103  ftc1cnnc  38129  dvasin  38141  fnopabco  38160  frinfm  38172  caushft  38198  bndss  38223  notornotel1  38532  tsbi2  38571  rabeq12f  38594  relcnveq3  38764  relcnveq2  38766  cnvref4  38787  ralrnmo  38798  raldmqsmo  38800  disjressuc2  38848  cnvcosseq  38964  symrelcoss3  38992  dfrefrels2  39030  dfrefrel2  39032  dfcnvrefrels2  39045  dfcnvrefrel2  39047  dfsymrels2  39062  elrelscnveq3  39064  dfsymrel2  39070  symrefref2  39084  dftrrels2  39096  dftrrel2  39098  n0elim  39172  disjimeceqim  39241  membpartlem19  39351  axc11n-16  39500  glbconN  39939  paddssat  40376  pclunN  40460  paddunN  40489  poldmj1N  40490  ltrnnid  40698  dibglbN  41728  mndmolinv  42650  primrootsunit1  42652  primrootscoprmpow  42654  primrootscoprbij  42657  aks6d1c2lem4  42682  aks6d1c2  42685  aks6d1c5lem3  42692  deg1gprod  42695  sticksstones3  42703  sticksstones11  42711  sticksstones12a  42712  sticksstones12  42713  sticksstones13  42714  aks6d1c6isolem1  42729  aks6d1c6lem5  42732  grpods  42749  unitscyglem2  42751  unitscyglem3  42752  unitscyglem4  42753  aks5lem7  42755  exbiii  42765  sn-0ne2  42953  sn-0lt1  43035  istopclsd  43219  pellex  43350  monotoddzzfi  43457  jm2.23  43511  expdioph  43538  wopprc  43545  kelac1  43578  dfac21  43581  lsmfgcl  43589  pwssplit4  43604  isnumbasgrp  43622  dgraalem  43660  ordnexbtwnsuc  43782  cantnfresb  43839  dflim5  43844  rp-tfslim  43868  ifpbi1  43991  rp-fakeanorass  44027  rp-isfinite5  44031  iscard4  44047  minregex  44048  pr2cv  44062  superficl  44081  ssuncl  44084  sssymdifcl  44086  relintab  44097  cnvssb  44100  cotrintab  44128  clcnvlem  44137  cnvtrrel  44184  brfvrcld2  44206  relexpxpmin  44231  relexpaddss  44232  unhe1  44299  frege55lem1b  44409  frege58bid  44416  frege92  44469  uneqsn  44539  ntrk2imkb  44551  neik0pk1imk0  44561  gneispace  44648  k0004lem2  44662  k0004val0  44668  ismnushort  44815  pm10.12  44872  pm11.61  44907  sbiota1  44948  bi1imp  44996  bi2imp  44997  bi3impb  44998  bi3impa  44999  bi13impib  45001  bi123impib  45002  bi13impia  45003  bi123impia  45004  bi13imp23  45006  bi13imp2  45007  bi12imp3  45008  tratrb  45050  dfvd1imp  45089  dfvd2imp  45117  e1bi  45143  e2bi  45146  e3bi  45251  3ornot23VD  45360  3impexpbicomVD  45370  3impexpbicomiVD  45371  tratrbVD  45374  ssralv2VD  45379  equncomiVD  45382  truniALTVD  45391  ee33VD  45392  onfrALTlem3VD  45400  onfrALTlem2VD  45402  onfrALTlem1VD  45403  onfrALTVD  45404  relopabVD  45414  2uasbanhVD  45424  vk15.4jVD  45427  unisnALT  45439  chordthmALT  45446  iunconnlem2  45448  wfaxpow  45511  wfaxun  45513  fnchoice  45547  uzwo4  45571  inabs3  45574  rexanuz3  45612  disjrnmpt2  45704  disjinfi  45708  iunmapsn  45731  ssfiunibd  45826  iuneqfzuzlem  45848  iuneqfzuz  45849  xrge0ge0  45861  xrssre  45862  infrpge  45865  allbutfi  45906  supxrunb3  45912  eluzelz2  45915  uz0  45924  allbutfiinf  45932  infxrunb3rnmpt  45940  uzublem  45942  uzub  45943  uzid3  45947  infxrlesupxr  45948  infrpgernmpt  45977  supminfxrrnmpt  45983  rexanuz2nf  46004  eliocre  46023  lbioc  46027  ioonct  46051  uzinico  46073  fsumiunss  46089  fmuldfeq  46097  mccl  46112  climsuse  46122  islptre  46133  lptioo2  46145  lptioo1  46146  islpcn  46151  fnlimfvre  46186  climbddf  46199  limsupvaluz  46220  limsupubuzlem  46224  limsupmnfuzlem  46238  limsupequzmptlem  46240  limsupre3uzlem  46247  xlimcl  46334  cnrefiisplem  46341  xlimliminflimsup  46374  icccncfext  46399  cncfiooicclem1  46405  cncfiooicc  46406  ioodvbdlimc1lem2  46444  ioodvbdlimc2lem  46446  dvnprodlem1  46458  dvnprodlem3  46460  volioc  46484  itgioocnicc  46489  stoweidlem28  46540  stoweidlem57  46569  wallispilem3  46579  wallispilem4  46580  wallispi  46582  wallispi2lem1  46583  wallispi2  46585  stirlinglem12  46597  fourierdlem42  46661  fourierdlem48  46666  fourierdlem50  46668  fourierdlem52  46670  fourierdlem71  46689  fourierdlem73  46691  fourierdlem74  46692  fourierdlem75  46693  fourierdlem76  46694  fourierdlem80  46698  fourierdlem93  46711  fourierdlem101  46719  fourierdlem103  46721  fourierdlem104  46722  fourierswlem  46742  fouriersw  46743  etransclem26  46772  etransclem37  46783  rrxsnicc  46812  saluncl  46829  intsaluni  46841  intsal  46842  salgencl  46844  salexct  46846  sssalgen  46847  salgenuni  46849  issalgend  46850  salgencntex  46855  subsaliuncllem  46869  subsaliuncl  46870  sge00  46888  sge0sn  46891  sge0cl  46893  sge0f1o  46894  sge0pnffigt  46908  sge0resplit  46918  sge0split  46921  sge0iunmptlemre  46927  sge0xaddlem2  46946  iundjiun  46972  meadjun  46974  meassle  46975  meadjiunlem  46977  meaiunlelem  46980  volmea  46986  caragenunidm  47020  omeunle  47028  omeiunltfirp  47031  caratheodorylem1  47038  caratheodory  47040  icoresmbl  47055  volicorescl  47065  ovncvrrp  47076  ovnsubaddlem2  47083  hoidmv1le  47106  hoidmvlelem1  47107  hoidmvlelem2  47108  hoidmvlelem5  47111  hoidmvle  47112  ovnhoilem2  47114  hspdifhsp  47128  hoiqssbllem3  47136  hspmbllem2  47139  ovolval4lem1  47161  ovnovollem3  47170  vonioolem1  47192  pimdecfgtioo  47229  pimincfltioo  47230  sssmf  47250  mbfresmf  47251  smfaddlem1  47275  smflimlem1  47283  smflimlem2  47284  smflimlem3  47285  smflim  47289  smfresal  47300  smfrec  47301  smfmullem4  47306  smfdiv  47309  smfpimbor1lem2  47311  smflimmpt  47322  smfsuplem1  47323  smfinflem  47329  smflimsuplem3  47334  smflimsuplem5  47336  smflimsuplem6  47337  smflimsuplem7  47338  smflimsupmpt  47341  smfliminflem  47342  smfliminfmpt  47344  simpcntrab  47382  quantgodelALT  47387  chnerlem1  47396  chnerlem2  47397  cos5teq  47412  lambert0  47419  lamberte  47420  aifftbifffaibif  47453  aifftbifffaibifff  47454  abciffcbatnabciffncba  47461  abciffcbatnabciffncbai  47462  nabctnabc  47463  confun4  47474  confun5  47475  plcofph  47476  pldofph  47477  plvcofph  47478  plvcofphax  47479  plvofpos  47480  dandysum2p2e4  47530  fresfo  47580  fcores  47599  3f1oss1  47607  3f1oss2  47608  funfocofob  47610  aiotaint  47623  dfaiota3  47624  ndmaovrcl  47736  tz6.12-afv2  47772  fvmptrabdm  47825  difmodm1lt  47897  uniimafveqt  47925  uniimaelsetpreimafv  47940  iccpartiun  47978  iccpartdisj  47981  ich2exprop  48015  ichnreuop  48016  prpair  48045  fmtnorec2lem  48089  dfodd5  48220  stgoldbwt  48336  sbgoldbb  48342  nnsum3primesle9  48354  nnsum4primeseven  48360  clnbgrcl  48381  clnbgrnvtx0  48387  clnbgredg  48400  grimuhgr  48447  isuspgrim0  48454  isuspgrimlem  48455  gricushgr  48477  grtriclwlk3  48505  isubgr3stgrlem1  48526  isubgr3stgrlem7  48532  uspgrlimlem2  48549  uspgrlimlem4  48551  grlimprclnbgr  48556  gpgusgralem  48616  gpg5order  48620  gpg5nbgrvtx03star  48640  gpg5nbgr3star  48641  gpgvtxdg3  48642  gpg5gricstgr3  48650  pgnbgreunbgrlem3  48678  pgnbgreunbgrlem6  48684  pgnbgreunbgr  48685  pgn4cyclex  48686  lmod0rng  48789  lidldomnnring  48796  ringcinvALTV  48870  altgsumbcALT  48913  ply1sclrmsm  48944  linccl  48974  lincvalsng  48976  lincvalpr  48978  lincdifsn  48984  linc1  48985  lincsum  48989  lincscm  48990  lindslinindsimp2lem5  49022  lincresunit3lem2  49040  2sphere  49309  resinsnALT  49432  tposideq  49447  clduni  49460  neircl  49464  funcrcl2  49638  funcrcl3  49639  funcf2lem2  49641  uprcl2  49748  uprcl3  49749  swapf2fval  49824  swapf1val  49826  fucofvalne  49884  thincn0eu  49990  isinito3  50059  mndtcbas2  50142