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  1030  pm5.16  1031  4exmid  1067  simp1bi  1163  simp2bi  1164  simp3bi  1165  syl3an1b  1430  syl3an2b  1431  syl3an3b  1432  nic-ax  1703  nfnt  1886  19.25  1910  nfimd  1924  19.37imv  1977  alcomimw  2073  sbbii  2110  nsb  2141  excomim  2198  stdpc5  2244  sbequ2  2285  sb9i  2552  mo4  2594  2mo  2676  ax9ALT  2758  eleq2w2  2759  eqeq1d  2765  r19.37v  3191  rmoeq1  3400  elabgt  3631  euind  3687  reuind  3716  sbcimdv  3812  sbcg  3816  ra4v  3838  ra4  3839  csbied  3889  ssrmof  4005  elunnel1  4108  elunnel2  4109  unssd  4145  n0moeu  4314  eqeuel  4320  ss0  4359  iftrueb  4500  elinsn  4676  disjtp2  4682  rabsnif  4689  prprc  4733  elpwdifsn  4757  ssunsn2  4793  preqr1  4813  intss2  5074  disjxiun  5106  unisn2  5275  snexALT  5354  reusv3i  5375  snexOLD  5413  pocl  5577  brrelex12  5713  0nelrel0  5721  elrel  5784  exopxfr2  5830  dmxp  5919  xpssres  6017  elinxp  6018  imadisjlnd  6083  elimasni  6093  inisegn0  6100  xpdifid  6165  xpdifcnvepel  6166  imadifssranOLD  6203  dmsnsnsn  6221  relcnvtrg  6268  xpco  6290  reuop  6294  predprc  6339  sucprc  6439  onunel  6468  iotaint  6514  iotanul  6516  funun  6582  funcnv3  6606  funimass1  6618  funssxp  6734  f0dom0  6762  dffv3  6877  dffv2  6976  fsneq  7030  fndmin  7040  sspreima  7063  iinpreima  7064  fveqressseq  7074  fsn2  7132  f1ounsn  7270  f12dfv  7271  f13dfv  7272  isoselem  7339  oprabidw  7441  oprabid  7442  ovima0  7589  sorpsscmpl  7731  abnex  7752  pwuncl  7765  ordsuci  7803  peano2  7882  1stval  7984  2ndval  7985  1stdm  8033  oprabco  8087  f1o2ndf1  8113  poxp  8120  frxp3  8143  suppval1  8158  fnsuppeq0  8184  frrlem4  8282  tz7.48lem  8424  tz7.49c  8429  ord1eln01  8477  ord2eln012  8478  undifixp  8928  bren2  8976  ensym  8996  en1uniel  9022  domunsn  9111  limenpsi  9136  findcard2  9145  unfi  9151  pwssfi  9157  php4  9190  isinf  9221  en2  9236  fiint  9282  rneqdmfinf1o  9286  elfiun  9386  marypha1lem  9389  supval2  9411  eqinf  9441  brwdom2  9531  zfreg  9554  tcmin  9704  frmin  9717  prwf  9779  r1pw  9813  rankuni2b  9821  rankr1id  9830  djuun  9908  cardval3  9934  ficardom  9943  cardmin2  9981  isinfcard  10072  iscard3  10073  alephval3  10090  dfac9  10116  kmlem6  10135  fin23lem29  10320  fin23lem30  10321  isf32lem11  10342  isfin1-3  10365  fin45  10371  fin1a2lem12  10390  fin1a2lem13  10391  axcc2lem  10415  dominf  10424  axdc4lem  10434  dominfac  10553  pwcfsdom  10563  cfpwsdom  10564  tskuni  10763  wfgru  10796  rpregt0  13026  supxrun  13337  elicore  13420  xrge0nre  13475  elfz1end  13578  elfzonlteqm1  13766  modfzo0difsn  13975  fzennn  14000  cardfz  14002  fsuppmapnn0fiub0  14025  ser0  14086  crreczi  14260  faclbnd  14322  bcn1  14345  hashrabsn01  14405  hashge0  14419  prsshashgt1  14443  hashssdif  14445  hashdifpr  14448  hashsn01  14449  hashgt23el  14457  hashpw  14469  hashres  14471  hash3tpexb  14527  ccatw2s1p1  14670  swrdswrd  14738  swrdccatin2  14762  pfxccatpfx1  14769  repsundef  14804  trclublem  15028  reltrclfv  15050  dmtrclfv  15051  cau3lem  15402  harmonic  15909  mertenslem2  15935  prodf1  15941  fprodfac  16023  rpnnen2lem12  16276  sqrt2irr0  16302  lcmftp  16689  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  prmind2  16738  prm2orodd  16744  pceq0  16926  prmreclem6  16976  0ram  17075  ram0  17077  cshwsiun  17154  ressbas2  17293  ressinbas  17300  ressval3d  17301  catpropd  17760  initoid  18053  termoid  18054  initoeu2lem0  18065  arwhoma  18097  joinfval  18422  meetfval  18436  lubun  18566  psssdm  18633  ex-chn1  18688  ex-chn2  18689  ismgmn0  18695  plusfeq  18701  idresefmnd  18953  qsxpid  19238  snsymgefmndeq  19460  fvcosymgeq  19494  pmtrprfv3  19519  pmtr3ncomlem1  19538  ablsubadd23  19878  ablsubsub23  19889  cygabl  19956  gsummptfzsplitl  19998  gsum2dlem1  20035  gsum2dlem2  20036  gsum2d  20037  rng1zrlem  20254  opprnzr  20620  cntzsubrng  20666  ringcinv  20770  opprdomn  20816  drngmcl  20855  staffn  20946  scafeq  21003  lbsexg  21288  rngridlmcl  21342  rnglidl1  21358  df2idl2  21396  2idlss  21401  ssdifidlprm  21486  prmirred  21624  frgpcyg  21723  ipfeq  21800  dsmmbas2  21887  zlmassa  22053  ply1bascl2  22364  lply1binom  22470  mamufacex  22553  matsubgcell  22591  matinvgcell  22592  matepmcl  22619  matepm2cl  22620  marrepcl  22721  marepvcl  22726  mulmarep1el  22729  mulmarep1gsum1  22730  mulmarep1gsum2  22731  nfimdetndef  22746  mdetfval1  22747  m1detdiag  22754  mdetdiag  22756  slesolinvbi  22838  pmatcoe1fsupp  22858  mat2pmatbas  22883  mat2pmatmul  22888  m2cpminvid2lem  22911  monmatcollpw  22936  pm2mpf1  22956  pm2mpghm  22973  cayhamlem1  23023  isbasis3g  23106  isopn2  23189  ntrval2  23208  toponmre  23250  innei  23282  restcld  23329  restcldi  23330  neitr  23337  discmp  23555  cmpsublem  23556  cmpsub  23557  ssref  23669  dissnref  23685  ptcnp  23779  imasnopn  23847  imasncld  23848  imasncls  23849  kqf  23904  fbun  23997  opnfbas  23999  supfil  24052  ufprim  24066  acufl  24074  filufint  24077  ufldom  24119  hausflf2  24155  alexsubALTlem4  24207  cnextfval  24219  cnextfun  24221  cnextfres1  24225  efmndtmd  24258  trust  24386  ustuqtop1  24398  metustid  24711  metustbl  24723  restmetu  24727  zlmclm  25271  cphassr  25371  ehleudisval  25578  ovolun  25658  vitalilem2  25768  dvcobr  26105  dvmptfsum  26134  rolle  26149  dvfsumlem2  26186  plyn0mulidp  26442  ulmcaulem  26557  logfac  26766  logno1  26801  logreclem  26927  prmorcht  27342  pclogsum  27379  gausslemma2dlem0i  27528  gausslemma2dlem1a  27529  2lgslem1c  27557  2sqlem10  27592  chto1lb  27642  cutsval  27973  addsproplem2  28163  oncutlt  28457  n0s0suc  28535  tgjustf  28742  tgldimor  28771  axcontlem7  29320  lfgredgge2  29474  edgupgr  29484  ausgrusgrb  29515  ausgrumgri  29517  uspgredg2vlem  29573  uspgredg2v  29574  usgredg2vlem2  29576  usgredg2v  29577  ushgredgedg  29579  ushgredgedgloop  29581  griedg0ssusgr  29615  umgrres1lem  29660  upgrres1  29663  nbgrcl  29685  nbgrnvtx0  29689  nbuhgr  29693  nbuhgr2vtx1edgb  29702  edgnbusgreu  29717  nb3grprlem2  29731  nb3grpr2  29733  nb3gr2nb  29734  cplgr2vpr  29783  cplgr3v  29785  vtxdumgrval  29836  umgr2v2evtxel  29872  usgrvd0nedg  29883  finsumvtxdg2ssteplem4  29898  wlk1walk  29988  wlk0prc  30002  wlkp1lem8  30028  wlkp1  30029  spthdep  30083  usgr2pthlem  30112  usgr2pth  30113  crctprop  30141  cyclprop  30142  cyclnumvtx  30149  crctcshwlkn0  30170  wwlknllvtx  30195  wlkiswwlks1  30216  wlkswwlksf1o  30228  wwlksnextproplem3  30260  wwlksnwwlksnon  30264  umgr2wlkon  30299  wwlks2onv  30302  elwspths2on  30311  elwspths2onw  30312  elwwlks2  30318  elwspths2spth  30319  rusgrnumwwlks  30326  clwlkclwwlklem2a4  30348  clwlkclwwlklem2  30351  clwlkclwwlkf  30359  erclwwlkref  30371  erclwwlknref  30420  erclwwlknsym  30421  erclwwlkntr  30422  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwlknf1oclwwlknlem1  30432  clwwlknon1  30448  clwwlknon1nloop  30450  clwwlkvbij  30464  0clwlkv  30482  uhgr3cyclex  30533  umgr3cyclex  30534  vdn0conngrumgrv2  30547  eupthi  30554  eucrctshift  30594  frcond1  30617  frcond4  30621  frgr3v  30626  3vfriswmgr  30629  1to2vfriswmgr  30630  1to3vfriswmgr  30631  2pthfrgr  30635  4cycl2v2nb  30640  n4cyclfrgr  30642  frgrnbnb  30644  frgrwopreglem4a  30661  clwlknon2num  30719  numclwwlkqhash  30726  frgrreg  30745  frgrregord013  30746  ex-ceil  30799  grpoidinvlem3  30858  nmlno0lem  31145  blocni  31157  pythi  31202  normpythi  31494  shmodsi  31741  pjchi  31784  chlubii  31824  osumi  31994  nmlnop0iALT  32347  cnlnssadj  32432  nmopcoi  32447  mdbr3  32649  mdbr4  32650  ssmd1  32663  dmdsl3  32667  mdexchi  32687  atssma  32730  atoml2i  32735  chirredlem3  32744  mdsymlem1  32755  dmdbr6ati  32775  dmdbr7ati  32776  cdjreui  32784  cdj3lem2b  32789  addltmulALT  32798  difuncomp  32898  iundifdif  32907  imadifxp  32946  fresf1o  32976  2ndimaxp  32991  acunirnmpt2  33005  suppiniseg  33031  fressupp  33033  fdifsuppconst  33034  ressupprn  33035  disjdsct  33048  1stpreimas  33051  preiman0  33055  resf1o  33075  xrge0addge  33103  xlt2addrd  33104  fz2ssnn0  33130  f1ocnt  33145  elq2  33156  nexple  33177  s2rnOLD  33264  s3rnOLD  33266  gsummpt2d  33369  gsumfs2d  33381  gsumwun  33396  psgnfzto1stlem  33420  fzto1st  33423  psgnfzto1st  33425  cycpmco2f1  33444  cycpmco2rn  33445  cycpmco2lem7  33452  elrgspn  33566  elrgspnsubrunlem2  33568  elrlocbasi  33587  ricnzr1  33608  sdrginvcl  33621  nsgqusf1olem2  33723  elrspunidl  33736  ssmxidl  33757  selvply1rhmlem2  33911  lbsdiflsp0  34016  fldextfld1  34037  fldextfld2  34038  constrconj  34135  constrllcllem  34142  constrlccllem  34143  constrcccllem  34144  submat1n  34195  submatres  34196  locfinreflem  34230  ldlfcntref  34244  zarclsun  34260  zarclsiin  34261  zarclsint  34262  zarcmplem  34271  mndpluscn  34316  pnfneige0  34341  pl1cn  34345  gsumesum  34449  esumcst  34453  esumrnmpt2  34458  esumcvgre  34481  esum2d  34483  pwsiga  34520  ldsysgenld  34550  measxun2  34600  volmeas  34621  ddemeas  34626  aean  34634  mbfmfun  34643  1stmbfm  34650  2ndmbfm  34651  omssubadd  34690  carsgclctunlem1  34707  sibfof  34730  eulerpartlemmf  34765  probun  34809  dstfrvclim1  34868  coinfliprv  34873  ballotlem2  34879  ballotlemic  34897  ballotlem1c  34898  signstres  34962  bnj529  35130  bnj1379  35218  bnj1424  35226  bnj1436  35227  bnj607  35304  bnj908  35319  bnj1097  35369  bnj1118  35372  bnj1128  35378  bnj1145  35381  bnj1154  35387  bnj1174  35391  bnj1189  35397  bnj1417  35429  axprALT2  35503  rankfo  35505  acnum  35525  tz9.1regs  35547  axsepg2  35553  axsepg4  35556  kardcard2b  35578  0nn0m1nnn0  35604  lfuhgr2  35611  cusgr3cyclex  35628  cvmliftlem10  35786  satfv1  35855  fmlasuc0  35876  satffunlem2lem1  35896  mrsub0  36008  mrsubccat  36010  mrsubcn  36011  bcprod  36230  socnv  36256  dfon2lem3  36275  dfon2lem7  36279  dfon2lem8  36280  rdgprc0  36283  fvsingle  36410  unisnif  36415  funpartlem  36434  hfun  36670  ss-ax8  36757  trer  36847  clsun  36859  opnregcld  36861  cldregopn  36862  df3nandALT1  36930  lukshef-ax2  36946  nandsym1  36953  weiunfr  36998  dfttc4lem2  37060  knoppndvlem9  37129  bj-mt2bi  37180  bj-gl4  37208  bj-babygodel  37216  bj-babylob  37217  bj-ssbid2ALT  37305  bj-nfext  37359  bj-1upln0  37665  bj-snex  37691  eleq2w2ALT  37703  bj-brrelex12ALT  37723  bj-restsnid  37749  bj-snmooreb  37776  bj-opelrelex  37808  bj-inftyexpitaudisj  37869  bj-inftyexpidisj  37874  bj-elccinfty  37878  finorwe  38048  ctbssinf  38072  fvineqsnf1  38076  pibt2  38083  wl-ifpimpr  38132  wl-ifp4impr  38133  wl-1xor  38148  wl-1mintru1  38154  lindsadd  38284  lindsenlbs  38286  poimirlem9  38300  poimirlem13  38304  poimirlem14  38305  poimirlem25  38316  poimirlem26  38317  mblfinlem2  38329  mblfinlem3  38330  mblfinlem4  38331  ismblfin  38332  mbfresfi  38337  ftc1cnnc  38363  dvasin  38375  fnopabco  38394  frinfm  38406  caushft  38432  bndss  38457  notornotel1  38764  tsbi2  38803  rabeq12f  38826  relcnveq3  38996  relcnveq2  38998  cnvref4  39019  ralrnmo  39030  raldmqsmo  39032  disjressuc2  39080  cnvcosseq  39196  symrelcoss3  39224  dfrefrels2  39262  dfrefrel2  39264  dfcnvrefrels2  39277  dfcnvrefrel2  39279  dfsymrels2  39294  elrelscnveq3  39296  dfsymrel2  39302  symrefref2  39316  dftrrels2  39328  dftrrel2  39330  n0elim  39404  disjimeceqim  39473  membpartlem19  39583  axc11n-16  39732  glbconN  40171  paddssat  40608  pclunN  40692  paddunN  40721  poldmj1N  40722  ltrnnid  40930  dibglbN  41960  mndmolinv  42882  primrootsunit1  42884  primrootscoprmpow  42886  primrootscoprbij  42889  aks6d1c2lem4  42914  aks6d1c2  42917  aks6d1c5lem3  42924  deg1gprod  42927  sticksstones3  42935  sticksstones11  42943  sticksstones12a  42944  sticksstones12  42945  sticksstones13  42946  aks6d1c6isolem1  42961  aks6d1c6lem5  42964  grpods  42981  unitscyglem2  42983  unitscyglem3  42984  unitscyglem4  42985  aks5lem7  42987  exbiii  42999  sn-0ne2  43187  sn-0lt1  43269  istopclsd  43451  pellex  43582  monotoddzzfi  43689  jm2.23  43743  expdioph  43770  wopprc  43777  kelac1  43810  dfac21  43813  lsmfgcl  43821  pwssplit4  43836  isnumbasgrp  43854  dgraalem  43892  ordnexbtwnsuc  44014  cantnfresb  44071  dflim5  44076  rp-tfslim  44100  ifpbi1  44223  rp-fakeanorass  44259  rp-isfinite5  44263  iscard4  44279  minregex  44280  pr2cv  44294  superficl  44313  ssuncl  44316  sssymdifcl  44318  relintab  44329  cnvssb  44332  cotrintab  44360  clcnvlem  44369  cnvtrrel  44416  brfvrcld2  44438  relexpxpmin  44463  relexpaddss  44464  unhe1  44531  frege55lem1b  44641  frege58bid  44648  frege92  44701  uneqsn  44771  ntrk2imkb  44783  neik0pk1imk0  44793  gneispace  44880  k0004lem2  44894  k0004val0  44900  ismnushort  45031  pm10.12  45088  pm11.61  45123  sbiota1  45164  bi1imp  45211  bi2imp  45212  bi3impb  45213  bi3impa  45214  bi13impib  45216  bi123impib  45217  bi13impia  45218  bi123impia  45219  bi13imp23  45221  bi13imp2  45222  bi12imp3  45223  tratrb  45265  dfvd1imp  45304  dfvd2imp  45332  e1bi  45358  e2bi  45361  e3bi  45466  3ornot23VD  45575  3impexpbicomVD  45585  3impexpbicomiVD  45586  tratrbVD  45589  ssralv2VD  45594  equncomiVD  45597  truniALTVD  45606  ee33VD  45607  onfrALTlem3VD  45615  onfrALTlem2VD  45617  onfrALTlem1VD  45618  onfrALTVD  45619  relopabVD  45629  2uasbanhVD  45639  vk15.4jVD  45642  unisnALT  45654  chordthmALT  45661  iunconnlem2  45663  wfaxpow  45726  wfaxun  45728  fnchoice  45769  uzwo4  45793  inabs3  45796  rexanuz3  45834  disjrnmpt2  45926  disjinfi  45930  iunmapsn  45953  ssfiunibd  46048  iuneqfzuzlem  46070  iuneqfzuz  46071  xrge0ge0  46083  xrssre  46084  infrpge  46087  allbutfi  46128  supxrunb3  46134  eluzelz2  46137  uz0  46146  allbutfiinf  46154  infxrunb3rnmpt  46162  uzublem  46164  uzub  46165  uzid3  46169  infxrlesupxr  46170  infrpgernmpt  46199  supminfxrrnmpt  46205  rexanuz2nf  46226  eliocre  46245  lbioc  46249  ioonct  46273  uzinico  46295  fsumiunss  46311  fmuldfeq  46319  mccl  46334  climsuse  46344  islptre  46355  lptioo2  46367  lptioo1  46368  islpcn  46373  fnlimfvre  46408  climbddf  46421  limsupubuzlem  46446  limsupmnfuzlem  46460  limsupequzmptlem  46462  limsupre3uzlem  46469  xlimcl  46556  cnrefiisplem  46563  xlimliminflimsup  46596  icccncfext  46621  cncfiooicclem1  46627  cncfiooicc  46628  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnprodlem1  46680  dvnprodlem3  46682  volioc  46706  itgioocnicc  46711  stoweidlem28  46762  stoweidlem57  46791  wallispilem3  46801  wallispilem4  46802  wallispi  46804  wallispi2lem1  46805  wallispi2  46807  stirlinglem12  46819  fourierdlem42  46883  fourierdlem48  46888  fourierdlem50  46890  fourierdlem52  46892  fourierdlem71  46911  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem80  46920  fourierdlem93  46933  fourierdlem101  46941  fourierdlem103  46943  fourierdlem104  46944  fourierswlem  46964  fouriersw  46965  etransclem26  46994  etransclem37  47005  rrxsnicc  47034  saluncl  47051  intsaluni  47063  intsal  47064  salgencl  47066  salexct  47068  sssalgen  47069  salgenuni  47071  issalgend  47072  salgencntex  47077  subsaliuncllem  47091  subsaliuncl  47092  sge00  47110  sge0sn  47113  sge0cl  47115  sge0f1o  47116  sge0pnffigt  47130  sge0resplit  47140  sge0split  47143  sge0iunmptlemre  47149  sge0xaddlem2  47168  iundjiun  47194  meadjun  47196  meassle  47197  meadjiunlem  47199  meaiunlelem  47202  volmea  47208  caragenunidm  47242  omeunle  47250  omeiunltfirp  47253  caratheodorylem1  47260  caratheodory  47262  icoresmbl  47277  volicorescl  47287  ovncvrrp  47298  ovnsubaddlem2  47305  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem2  47330  hoidmvlelem5  47333  hoidmvle  47334  ovnhoilem2  47336  hspdifhsp  47350  hoiqssbllem3  47358  hspmbllem2  47361  ovolval4lem1  47383  ovnovollem3  47392  vonioolem1  47414  pimdecfgtioo  47451  pimincfltioo  47452  mbfresmf  47473  smfaddlem1  47497  smflimlem1  47505  smflimlem2  47506  smflimlem3  47507  smflim  47511  smfresal  47522  smfrec  47523  smfmullem4  47528  smfdiv  47531  smfpimbor1lem2  47533  smflimmpt  47544  smfsuplem1  47545  smfinflem  47551  smflimsuplem3  47556  smflimsuplem5  47558  smflimsuplem6  47559  smflimsuplem7  47560  smflimsupmpt  47563  smfliminflem  47564  smfliminfmpt  47566  simpcntrab  47604  quantgodelALT  47609  chnerlem1  47618  chnerlem2  47619  sqrtnzqaa  47625  cos5teq  47637  lambert0  47644  lamberte  47645  aifftbifffaibif  47678  aifftbifffaibifff  47679  abciffcbatnabciffncba  47686  abciffcbatnabciffncbai  47687  nabctnabc  47688  confun4  47699  confun5  47700  plcofph  47701  pldofph  47702  plvcofph  47703  plvcofphax  47704  plvofpos  47705  dandysum2p2e4  47755  fresfo  47805  fcores  47824  3f1oss1  47832  3f1oss2  47833  funfocofob  47835  aiotaint  47848  dfaiota3  47849  ndmaovrcl  47961  tz6.12-afv2  47997  fvmptrabdm  48050  difmodm1lt  48122  uniimafveqt  48150  uniimaelsetpreimafv  48165  iccpartiun  48203  iccpartdisj  48206  ich2exprop  48240  ichnreuop  48241  prpair  48270  fmtnorec2lem  48314  dfodd5  48445  stgoldbwt  48561  sbgoldbb  48567  nnsum3primesle9  48579  nnsum4primeseven  48585  clnbgrcl  48606  clnbgrnvtx0  48612  clnbgredg  48625  grimuhgr  48672  isuspgrim0  48679  isuspgrimlem  48680  gricushgr  48702  grtriclwlk3  48730  isubgr3stgrlem1  48751  isubgr3stgrlem7  48757  uspgrlimlem2  48774  uspgrlimlem4  48776  grlimprclnbgr  48781  gpgusgralem  48841  gpg5order  48845  gpg5nbgrvtx03star  48865  gpg5nbgr3star  48866  gpgvtxdg3  48867  gpg5gricstgr3  48875  pgnbgreunbgrlem3  48903  pgnbgreunbgrlem6  48909  pgnbgreunbgr  48910  pgn4cyclex  48911  lmod0rng  49014  lidldomnnring  49021  ringcinvALTV  49095  altgsumbcALT  49153  ply1sclrmsm  49184  linccl  49214  lincvalsng  49216  lincvalpr  49218  lincdifsn  49224  linc1  49225  lincsum  49229  lincscm  49230  lindslinindsimp2lem5  49262  lincresunit3lem2  49280  2sphere  49549  resinsnALT  49671  tposideq  49686  clduni  49699  neircl  49703  funcrcl2  49877  funcrcl3  49878  funcf2lem2  49880  uprcl2  49987  uprcl3  49988  swapf2fval  50063  swapf1val  50065  fucofvalne  50123  thincn0eu  50229  isinito3  50298  mndtcbas2  50381  alsralrex  50610