Theorem biimpi 217

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sylbi  218  sylib  219  sylbb  220  biimpri  229  mpbi  231  biimtrid  243  imbitrdi  252  syl7bi  256  syl8ib  257  simplbi  497  simprbi  498  birani  504  bilani  505  anc2l  558  sylanb  587  sylanblc  595  sylan2b  600  pm3.37  813  pm2.53  857  orbi2i  918  pm2.32  929  pm2.76  937  pm3.1  999  pm5.15  1020  pm5.16  1021  4exmid  1057  simp1bi  1151  simp2bi  1152  simp3bi  1153  syl3an1b  1411  syl3an2b  1412  syl3an3b  1413  nic-ax  1680  nfnt  1863  19.25  1887  nfimd  1901  19.37imv  1954  alcomimw  2050  sbbii  2087  nsb  2117  excomim  2174  stdpc5  2220  sbequ2  2261  sb9i  2528  mo4  2570  2mo  2652  ax9ALT  2734  eleq2w2  2735  eqeq1d  2741  r19.37v  3165  rmoeq1  3375  elabgt  3610  euind  3665  reuind  3694  sbcimdv  3791  sbcg  3795  ra4v  3817  ra4  3818  csbied  3867  ssrmof  3983  elunnel1  4085  elunnel2  4086  unssd  4122  n0moeu  4288  eqeuel  4294  ss0  4331  iftrueb  4468  elinsn  4643  disjtp2  4649  rabsnif  4656  prprc  4700  elpwdifsn  4723  ssunsn2  4759  preqr1  4780  intss2  5038  disjxiun  5070  unisn2  5235  snexALT  5313  reusv3i  5334  snexOLD  5372  pocl  5535  brrelex12  5671  0nelrel0  5679  elrel  5742  exopxfr2  5787  dmxp  5872  xpssres  5971  elinxp  5972  imadisjlnd  6034  elimasni  6044  inisegn0  6051  imadifssran  6103  xpdifid  6120  dmsnsnsn  6172  relcnvtrg  6219  xpco  6241  reuop  6245  predprc  6290  sucprc  6389  onunel  6418  iotaint  6464  iotanul  6466  funun  6532  funcnv3  6556  funimass1  6568  funssxp  6684  f0dom0  6712  dffv3  6824  dffv2  6923  fsneq  6977  fndmin  6987  sspreima  7010  iinpreima  7011  fveqressseq  7021  fsn2  7079  f1ounsn  7217  f12dfv  7218  f13dfv  7219  isoselem  7286  oprabidw  7388  oprabid  7389  ovima0  7536  sorpsscmpl  7678  unexgOLD  7693  abnex  7701  pwuncl  7714  ordsuci  7752  peano2  7831  1stval  7934  2ndval  7935  1stdm  7983  oprabco  8036  f1o2ndf1  8062  poxp  8069  frxp3  8092  suppval1  8107  fnsuppeq0  8133  frrlem4  8230  tz7.48lem  8371  tz7.49c  8376  ord1eln01  8422  ord2eln012  8423  undifixp  8873  bren2  8921  ensym  8941  en1uniel  8967  domunsn  9056  limenpsi  9081  findcard2  9090  unfi  9096  pwssfi  9102  php4  9135  isinf  9166  en2  9181  fiint  9228  rneqdmfinf1o  9234  elfiun  9334  marypha1lem  9337  supval2  9359  eqinf  9389  brwdom2  9479  zfreg  9502  tcmin  9652  frmin  9665  prwf  9727  r1pw  9761  rankuni2b  9769  rankr1id  9778  djuun  9842  cardval3  9868  ficardom  9877  cardmin2  9915  isinfcard  10006  iscard3  10007  alephval3  10024  dfac9  10051  kmlem6  10070  fin23lem29  10255  fin23lem30  10256  isf32lem11  10277  isfin1-3  10300  fin45  10306  fin1a2lem12  10325  fin1a2lem13  10326  axcc2lem  10350  dominf  10359  axdc4lem  10369  dominfac  10488  pwcfsdom  10498  cfpwsdom  10499  tskuni  10698  wfgru  10731  rpregt0  12949  supxrun  13260  elicore  13343  xrge0nre  13398  elfz1end  13500  elfzonlteqm1  13688  modfzo0difsn  13897  fzennn  13922  cardfz  13924  fsuppmapnn0fiub0  13947  ser0  14008  crreczi  14182  faclbnd  14244  bcn1  14267  hashrabsn01  14327  hashge0  14341  prsshashgt1  14364  hashssdif  14366  hashdifpr  14369  hashsn01  14370  hashgt23el  14378  hashpw  14390  hashres  14392  hash3tpexb  14448  ccatw2s1p1  14591  swrdswrd  14659  swrdccatin2  14683  pfxccatpfx1  14690  repsundef  14725  trclublem  14949  reltrclfv  14971  dmtrclfv  14972  cau3lem  15309  harmonic  15816  mertenslem2  15842  prodf1  15848  fprodfac  15930  rpnnen2lem12  16184  sqrt2irr0  16210  lcmftp  16597  lcmfunsnlem2lem1  16599  lcmfunsnlem2lem2  16600  prmind2  16646  prm2orodd  16652  pceq0  16834  prmreclem6  16884  0ram  16983  ram0  16985  cshwsiun  17062  ressbas2  17200  ressinbas  17207  ressval3d  17208  catpropd  17667  initoid  17960  termoid  17961  initoeu2lem0  17972  arwhoma  18004  joinfval  18329  meetfval  18343  lubun  18473  psssdm  18540  ex-chn1  18595  ex-chn2  18596  ismgmn0  18602  plusfeq  18608  idresefmnd  18859  snsymgefmndeq  19362  fvcosymgeq  19396  pmtrprfv3  19421  pmtr3ncomlem1  19440  ablsubadd23  19780  ablsubsub23  19791  cygabl  19858  gsummptfzsplitl  19900  gsum2dlem1  19937  gsum2dlem2  19938  gsum2d  19939  srg1zr  20188  opprnzr  20495  cntzsubrng  20540  ringcinv  20644  opprdomn  20691  drngmcl  20723  staffn  20816  scafeq  20873  lbsexg  21158  rngridlmcl  21211  rnglidl1  21226  df2idl2  21251  2idlss  21256  prmirred  21450  frgpcyg  21549  ipfeq  21626  dsmmbas2  21713  zlmassa  21879  ply1bascl2  22190  lply1binom  22297  mamufacex  22380  matsubgcell  22418  matinvgcell  22419  matepmcl  22446  matepm2cl  22447  marrepcl  22548  marepvcl  22553  mulmarep1el  22556  mulmarep1gsum1  22557  mulmarep1gsum2  22558  nfimdetndef  22573  mdetfval1  22574  m1detdiag  22581  mdetdiag  22583  slesolinvbi  22665  pmatcoe1fsupp  22685  mat2pmatbas  22710  mat2pmatmul  22715  m2cpminvid2lem  22738  monmatcollpw  22763  pm2mpf1  22783  pm2mpghm  22800  cayhamlem1  22850  isbasis3g  22933  isopn2  23016  ntrval2  23035  toponmre  23077  innei  23109  restcld  23156  restcldi  23157  neitr  23164  discmp  23382  cmpsublem  23383  cmpsub  23384  ssref  23496  dissnref  23512  ptcnp  23606  imasnopn  23674  imasncld  23675  imasncls  23676  kqf  23731  fbun  23824  opnfbas  23826  supfil  23879  ufprim  23893  acufl  23901  filufint  23904  ufldom  23946  hausflf2  23982  alexsubALTlem4  24034  cnextfval  24046  cnextfun  24048  cnextfres1  24052  efmndtmd  24085  trust  24213  ustuqtop1  24225  metustid  24538  metustbl  24550  restmetu  24554  zlmclm  25098  cphassr  25198  ehleudisval  25405  ovolun  25485  vitalilem2  25595  dvcobr  25932  dvmptfsum  25961  rolle  25976  dvfsumlem2  26013  ulmcaulem  26378  logfac  26584  logno1  26619  logreclem  26745  prmorcht  27160  pclogsum  27197  gausslemma2dlem0i  27346  gausslemma2dlem1a  27347  2lgslem1c  27375  2sqlem10  27410  chto1lb  27460  cutsval  27791  addsproplem2  27981  oncutlt  28275  n0s0suc  28353  tgjustf  28560  tgldimor  28589  axcontlem7  29058  lfgredgge2  29212  edgupgr  29222  ausgrusgrb  29253  ausgrumgri  29255  uspgredg2vlem  29311  uspgredg2v  29312  usgredg2vlem2  29314  usgredg2v  29315  ushgredgedg  29317  ushgredgedgloop  29319  griedg0ssusgr  29353  umgrres1lem  29398  upgrres1  29401  nbgrcl  29423  nbgrnvtx0  29427  nbuhgr  29431  nbuhgr2vtx1edgb  29440  edgnbusgreu  29455  nb3grprlem2  29469  nb3grpr2  29471  nb3gr2nb  29472  cplgr2vpr  29521  cplgr3v  29523  vtxdumgrval  29574  umgr2v2evtxel  29610  usgrvd0nedg  29621  finsumvtxdg2ssteplem4  29636  wlk1walk  29726  wlk0prc  29740  wlkp1lem8  29766  wlkp1  29767  spthdep  29821  usgr2pthlem  29850  usgr2pth  29851  crctprop  29879  cyclprop  29880  cyclnumvtx  29887  crctcshwlkn0  29908  wwlknllvtx  29933  wlkiswwlks1  29954  wlkswwlksf1o  29966  wwlksnextproplem3  29998  wwlksnwwlksnon  30002  umgr2wlkon  30037  wwlks2onv  30040  elwspths2on  30049  elwspths2onw  30050  elwwlks2  30056  elwspths2spth  30057  rusgrnumwwlks  30064  clwlkclwwlklem2a4  30086  clwlkclwwlklem2  30089  clwlkclwwlkf  30097  erclwwlkref  30109  erclwwlknref  30158  erclwwlknsym  30159  erclwwlkntr  30160  hashecclwwlkn1  30166  umgrhashecclwwlk  30167  clwlknf1oclwwlknlem1  30170  clwwlknon1  30186  clwwlknon1nloop  30188  clwwlkvbij  30202  0clwlkv  30220  uhgr3cyclex  30271  umgr3cyclex  30272  vdn0conngrumgrv2  30285  eupthi  30292  eucrctshift  30332  frcond1  30355  frcond4  30359  frgr3v  30364  3vfriswmgr  30367  1to2vfriswmgr  30368  1to3vfriswmgr  30369  2pthfrgr  30373  4cycl2v2nb  30378  n4cyclfrgr  30380  frgrnbnb  30382  frgrwopreglem4a  30399  clwlknon2num  30457  numclwwlkqhash  30464  frgrreg  30483  frgrregord013  30484  ex-ceil  30537  grpoidinvlem3  30596  nmlno0lem  30883  blocni  30895  pythi  30940  normpythi  31232  shmodsi  31479  pjchi  31522  chlubii  31562  osumi  31732  nmlnop0iALT  32085  cnlnssadj  32170  nmopcoi  32185  mdbr3  32387  mdbr4  32388  ssmd1  32401  dmdsl3  32405  mdexchi  32425  atssma  32468  atoml2i  32473  chirredlem3  32482  mdsymlem1  32493  dmdbr6ati  32513  dmdbr7ati  32514  cdjreui  32522  cdj3lem2b  32527  addltmulALT  32536  difuncomp  32643  iundifdif  32652  imadifxp  32691  fresf1o  32724  2ndimaxp  32739  acunirnmpt2  32753  suppiniseg  32779  fressupp  32781  fdifsuppconst  32782  ressupprn  32783  disjdsct  32796  1stpreimas  32799  preiman0  32803  resf1o  32823  xrge0addge  32851  xlt2addrd  32852  fz2ssnn0  32878  f1ocnt  32893  elq2  32905  nexple  32937  s2rnOLD  33024  s3rnOLD  33026  gsummpt2d  33131  gsumfs2d  33143  gsumwun  33158  psgnfzto1stlem  33182  fzto1st  33185  psgnfzto1st  33187  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem7  33214  elrgspn  33328  elrgspnsubrunlem2  33330  elrlocbasi  33348  ricnzr1  33370  sdrginvcl  33385  qsxpid  33446  nsgqusf1olem2  33498  elrspunidl  33512  ssdifidlprm  33542  ssmxidl  33558  selvply1rhmlem2  33714  lbsdiflsp0  33819  fldextfld1  33840  fldextfld2  33841  constrconj  33938  constrllcllem  33945  constrlccllem  33946  constrcccllem  33947  submat1n  33998  submatres  33999  locfinreflem  34033  ldlfcntref  34047  zarclsun  34063  zarclsiin  34064  zarclsint  34065  zarcmplem  34074  mndpluscn  34119  pnfneige0  34144  pl1cn  34148  gsumesum  34252  esumcst  34256  esumrnmpt2  34261  esumcvgre  34284  esum2d  34286  pwsiga  34323  ldsysgenld  34353  measxun2  34403  volmeas  34424  ddemeas  34429  aean  34437  mbfmfun  34446  1stmbfm  34453  2ndmbfm  34454  omssubadd  34493  carsgclctunlem1  34510  sibfof  34533  eulerpartlemmf  34568  probun  34612  dstfrvclim1  34671  coinfliprv  34676  ballotlem2  34682  ballotlemic  34700  ballotlem1c  34701  plymulx0  34740  signstres  34768  bnj529  34933  bnj1379  35021  bnj1424  35029  bnj1436  35030  bnj607  35107  bnj908  35122  bnj1097  35172  bnj1118  35175  bnj1128  35181  bnj1145  35184  bnj1154  35190  bnj1174  35194  bnj1189  35200  bnj1417  35232  axprALT2  35299  tz9.1regs  35324  axsepg2  35330  axsepg4  35333  0nn0m1nnn0  35350  lfuhgr2  35356  cusgr3cyclex  35373  cvmliftlem10  35531  satfv1  35600  fmlasuc0  35621  satffunlem2lem1  35641  mrsub0  35753  mrsubccat  35755  mrsubcn  35756  bcprod  35975  socnv  36001  dfon2lem3  36020  dfon2lem7  36024  dfon2lem8  36025  rdgprc0  36028  fvsingle  36155  unisnif  36160  funpartlem  36179  hfun  36415  ss-ax8  36462  trer  36553  clsun  36565  opnregcld  36567  cldregopn  36568  df3nandALT1  36636  lukshef-ax2  36652  nandsym1  36659  weiunfr  36704  dfttc4lem2  36766  knoppndvlem9  36835  bj-mt2bi  36887  bj-gl4  36915  bj-babygodel  36923  bj-babylob  36924  bj-ssbid2ALT  37012  bj-nfext  37066  bj-1upln0  37371  bj-snex  37397  eleq2w2ALT  37409  bj-brrelex12ALT  37429  bj-restsnid  37454  bj-snmooreb  37481  bj-opelrelex  37513  bj-inftyexpitaudisj  37574  bj-inftyexpidisj  37579  bj-elccinfty  37583  finorwe  37753  ctbssinf  37777  fvineqsnf1  37781  pibt2  37788  wl-ifpimpr  37837  wl-ifp4impr  37838  wl-1xor  37853  wl-1mintru1  37859  lindsadd  37989  lindsenlbs  37991  poimirlem9  38005  poimirlem13  38009  poimirlem14  38010  poimirlem25  38021  poimirlem26  38022  mblfinlem2  38034  mblfinlem3  38035  mblfinlem4  38036  ismblfin  38037  mbfresfi  38042  ftc1cnnc  38068  dvasin  38080  fnopabco  38099  frinfm  38111  caushft  38137  bndss  38162  notornotel1  38471  tsbi2  38510  rabeq12f  38533  relcnveq3  38703  relcnveq2  38705  cnvref4  38726  ralrnmo  38737  raldmqsmo  38739  disjressuc2  38787  cnvcosseq  38903  symrelcoss3  38931  dfrefrels2  38969  dfrefrel2  38971  dfcnvrefrels2  38984  dfcnvrefrel2  38986  dfsymrels2  39001  elrelscnveq3  39003  dfsymrel2  39009  symrefref2  39023  dftrrels2  39035  dftrrel2  39037  n0elim  39111  disjimeceqim  39180  membpartlem19  39290  axc11n-16  39439  glbconN  39878  paddssat  40315  pclunN  40399  paddunN  40428  poldmj1N  40429  ltrnnid  40637  dibglbN  41667  mndmolinv  42589  primrootsunit1  42591  primrootscoprmpow  42593  primrootscoprbij  42596  aks6d1c2lem4  42621  aks6d1c2  42624  aks6d1c5lem3  42631  deg1gprod  42634  sticksstones3  42642  sticksstones11  42650  sticksstones12a  42651  sticksstones12  42652  sticksstones13  42653  aks6d1c6isolem1  42668  aks6d1c6lem5  42671  grpods  42688  unitscyglem2  42690  unitscyglem3  42691  unitscyglem4  42692  aks5lem7  42694  exbiii  42704  sn-0ne2  42892  sn-0lt1  42974  istopclsd  43158  pellex  43289  monotoddzzfi  43396  jm2.23  43450  expdioph  43477  wopprc  43484  kelac1  43517  dfac21  43520  lsmfgcl  43528  pwssplit4  43543  isnumbasgrp  43561  dgraalem  43599  ordnexbtwnsuc  43721  cantnfresb  43778  dflim5  43783  rp-tfslim  43807  ifpbi1  43930  rp-fakeanorass  43966  rp-isfinite5  43970  iscard4  43986  minregex  43987  pr2cv  44001  superficl  44020  ssuncl  44023  sssymdifcl  44025  relintab  44036  cnvssb  44039  cotrintab  44067  clcnvlem  44076  cnvtrrel  44123  brfvrcld2  44145  relexpxpmin  44170  relexpaddss  44171  unhe1  44238  frege55lem1b  44348  frege58bid  44355  frege92  44408  uneqsn  44478  ntrk2imkb  44490  neik0pk1imk0  44500  gneispace  44587  k0004lem2  44601  k0004val0  44607  ismnushort  44754  pm10.12  44811  pm11.61  44846  sbiota1  44887  bi1imp  44935  bi2imp  44936  bi3impb  44937  bi3impa  44938  bi13impib  44940  bi123impib  44941  bi13impia  44942  bi123impia  44943  bi13imp23  44945  bi13imp2  44946  bi12imp3  44947  tratrb  44989  dfvd1imp  45028  dfvd2imp  45056  e1bi  45082  e2bi  45085  e3bi  45190  3ornot23VD  45299  3impexpbicomVD  45309  3impexpbicomiVD  45310  tratrbVD  45313  ssralv2VD  45318  equncomiVD  45321  truniALTVD  45330  ee33VD  45331  onfrALTlem3VD  45339  onfrALTlem2VD  45341  onfrALTlem1VD  45342  onfrALTVD  45343  relopabVD  45353  2uasbanhVD  45363  vk15.4jVD  45366  unisnALT  45378  chordthmALT  45385  iunconnlem2  45387  wfaxpow  45450  wfaxun  45452  fnchoice  45486  uzwo4  45510  inabs3  45513  rexanuz3  45551  disjrnmpt2  45643  disjinfi  45647  iunmapsn  45670  ssfiunibd  45765  iuneqfzuzlem  45787  iuneqfzuz  45788  xrge0ge0  45800  xrssre  45801  infrpge  45804  allbutfi  45845  supxrunb3  45851  eluzelz2  45854  uz0  45863  allbutfiinf  45871  infxrunb3rnmpt  45879  uzublem  45881  uzub  45882  uzid3  45886  infxrlesupxr  45887  infrpgernmpt  45916  supminfxrrnmpt  45922  rexanuz2nf  45943  eliocre  45962  lbioc  45966  ioonct  45990  uzinico  46012  fsumiunss  46028  fmuldfeq  46036  mccl  46051  climsuse  46061  islptre  46072  lptioo2  46084  lptioo1  46085  islpcn  46090  fnlimfvre  46125  climbddf  46138  limsupvaluz  46159  limsupubuzlem  46163  limsupmnfuzlem  46177  limsupequzmptlem  46179  limsupre3uzlem  46186  xlimcl  46273  cnrefiisplem  46280  xlimliminflimsup  46313  icccncfext  46338  cncfiooicclem1  46344  cncfiooicc  46345  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvnprodlem1  46397  dvnprodlem3  46399  volioc  46423  itgioocnicc  46428  stoweidlem28  46479  stoweidlem57  46508  wallispilem3  46518  wallispilem4  46519  wallispi  46521  wallispi2lem1  46522  wallispi2  46524  stirlinglem12  46536  fourierdlem42  46600  fourierdlem48  46605  fourierdlem50  46607  fourierdlem52  46609  fourierdlem71  46628  fourierdlem73  46630  fourierdlem74  46631  fourierdlem75  46632  fourierdlem76  46633  fourierdlem80  46637  fourierdlem93  46650  fourierdlem101  46658  fourierdlem103  46660  fourierdlem104  46661  fourierswlem  46681  fouriersw  46682  etransclem26  46711  etransclem37  46722  rrxsnicc  46751  saluncl  46768  intsaluni  46780  intsal  46781  salgencl  46783  salexct  46785  sssalgen  46786  salgenuni  46788  issalgend  46789  salgencntex  46794  subsaliuncllem  46808  subsaliuncl  46809  sge00  46827  sge0sn  46830  sge0cl  46832  sge0f1o  46833  sge0pnffigt  46847  sge0resplit  46857  sge0split  46860  sge0iunmptlemre  46866  sge0xaddlem2  46885  iundjiun  46911  meadjun  46913  meassle  46914  meadjiunlem  46916  meaiunlelem  46919  volmea  46925  caragenunidm  46959  omeunle  46967  omeiunltfirp  46970  caratheodorylem1  46977  caratheodory  46979  icoresmbl  46994  volicorescl  47004  ovncvrrp  47015  ovnsubaddlem2  47022  hoidmv1le  47045  hoidmvlelem1  47046  hoidmvlelem2  47047  hoidmvlelem5  47050  hoidmvle  47051  ovnhoilem2  47053  hspdifhsp  47067  hoiqssbllem3  47075  hspmbllem2  47078  ovolval4lem1  47100  ovnovollem3  47109  vonioolem1  47131  pimdecfgtioo  47168  pimincfltioo  47169  sssmf  47189  mbfresmf  47190  smfaddlem1  47214  smflimlem1  47222  smflimlem2  47223  smflimlem3  47224  smflim  47228  smfresal  47239  smfrec  47240  smfmullem4  47245  smfdiv  47248  smfpimbor1lem2  47250  smflimmpt  47261  smfsuplem1  47262  smfinflem  47268  smflimsuplem3  47273  smflimsuplem5  47275  smflimsuplem6  47276  smflimsuplem7  47277  smflimsupmpt  47280  smfliminflem  47281  smfliminfmpt  47283  simpcntrab  47321  quantgodelALT  47326  chnerlem1  47335  chnerlem2  47336  cos5teq  47351  lambert0  47358  lamberte  47359  aifftbifffaibif  47392  aifftbifffaibifff  47393  abciffcbatnabciffncba  47400  abciffcbatnabciffncbai  47401  nabctnabc  47402  confun4  47413  confun5  47414  plcofph  47415  pldofph  47416  plvcofph  47417  plvcofphax  47418  plvofpos  47419  dandysum2p2e4  47469  fresfo  47519  fcores  47538  3f1oss1  47546  3f1oss2  47547  funfocofob  47549  aiotaint  47562  dfaiota3  47563  ndmaovrcl  47675  tz6.12-afv2  47711  fvmptrabdm  47764  difmodm1lt  47836  uniimafveqt  47864  uniimaelsetpreimafv  47879  iccpartiun  47917  iccpartdisj  47920  ich2exprop  47954  ichnreuop  47955  prpair  47984  fmtnorec2lem  48028  dfodd5  48159  stgoldbwt  48275  sbgoldbb  48281  nnsum3primesle9  48293  nnsum4primeseven  48299  clnbgrcl  48320  clnbgrnvtx0  48326  clnbgredg  48339  grimuhgr  48386  isuspgrim0  48393  isuspgrimlem  48394  gricushgr  48416  grtriclwlk3  48444  isubgr3stgrlem1  48465  isubgr3stgrlem7  48471  uspgrlimlem2  48488  uspgrlimlem4  48490  grlimprclnbgr  48495  gpgusgralem  48555  gpg5order  48559  gpg5nbgrvtx03star  48579  gpg5nbgr3star  48580  gpgvtxdg3  48581  gpg5gricstgr3  48589  pgnbgreunbgrlem3  48617  pgnbgreunbgrlem6  48623  pgnbgreunbgr  48624  pgn4cyclex  48625  lmod0rng  48728  lidldomnnring  48735  ringcinvALTV  48809  altgsumbcALT  48852  ply1sclrmsm  48883  linccl  48913  lincvalsng  48915  lincvalpr  48917  lincdifsn  48923  linc1  48924  lincsum  48928  lincscm  48929  lindslinindsimp2lem5  48961  lincresunit3lem2  48979  2sphere  49248  resinsnALT  49371  tposideq  49386  clduni  49399  neircl  49403  funcrcl2  49577  funcrcl3  49578  funcf2lem2  49580  uprcl2  49687  uprcl3  49688  swapf2fval  49763  swapf1val  49765  fucofvalne  49823  thincn0eu  49929  isinito3  49998  mndtcbas2  50081