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  2144  excomim  2201  stdpc5  2247  sbequ2  2287  sb9i  2554  mo4  2596  2mo  2678  ax9ALT  2760  eleq2w2  2761  eqeq1d  2767  r19.37v  3193  rmoeq1  3402  elabgt  3633  euind  3689  reuind  3718  sbcimdv  3814  sbcg  3818  ra4v  3839  ra4  3840  csbied  3890  ssrmof  4006  elunnel1  4108  elunnel2  4109  unssd  4145  n0moeu  4314  eqeuel  4320  ss0  4359  iftrueb  4502  elinsn  4678  disjtp2  4684  rabsnif  4691  prprc  4735  elpwdifsn  4759  ssunsn2  4795  preqr1  4815  intss2  5076  disjxiun  5108  unisn2  5277  snexALT  5356  reusv3i  5377  snexOLD  5415  pocl  5579  brrelex12  5715  0nelrel0  5723  elrel  5786  exopxfr2  5832  dmxp  5921  xpssres  6019  elinxp  6020  imadisjlnd  6085  elimasni  6095  inisegn0  6102  xpdifid  6167  xpdifcnvepel  6168  imadifssranOLD  6205  dmsnsnsn  6223  relcnvtrgOLD  6271  xpco  6294  reuop  6298  predprc  6343  sucprc  6443  onunel  6472  iotaint  6518  iotanul  6520  funun  6586  funcnv3  6610  funimass1  6622  funssxp  6738  f0dom0  6766  dffv3  6881  dffv2  6980  fsneq  7034  fndmin  7044  sspreima  7067  iinpreima  7068  fveqressseq  7078  fsn2  7136  f1ounsn  7279  f12dfv  7280  f13dfv  7281  isoselem  7348  oprabidw  7450  oprabid  7451  ovima0  7599  sorpsscmpl  7741  abnex  7762  pwuncl  7775  ordsuci  7813  peano2  7892  1stval  7994  2ndval  7995  1stdm  8043  oprabco  8097  f1o2ndf1  8123  poxp  8130  frxp3  8153  suppval1  8168  fnsuppeq0  8194  frrlem4  8292  tz7.48lem  8434  tz7.49c  8439  ord1eln01  8487  ord2eln012  8488  undifixp  8938  bren2  8986  ensym  9006  en1uniel  9033  domunsn  9122  limenpsi  9147  findcard2  9156  unfi  9162  pwssfi  9168  php4  9201  isinf  9232  en2  9247  fiint  9293  rneqdmfinf1o  9297  elfiun  9397  marypha1lem  9400  supval2  9422  eqinf  9452  brwdom2  9542  zfreg  9565  tcmin  9715  frmin  9728  prwf  9790  r1pw  9824  rankuni2b  9832  rankr1id  9841  djuun  9928  cardval3  9954  ficardom  9963  cardmin2  10001  isinfcard  10092  iscard3  10093  alephval3  10110  dfac9  10136  kmlem6  10155  fin23lem29  10340  fin23lem30  10341  isf32lem11  10362  isfin1-3  10385  fin45  10391  fin1a2lem12  10410  fin1a2lem13  10411  axcc2lem  10435  dominf  10444  axdc4lem  10454  dominfac  10577  pwcfsdom  10587  cfpwsdom  10588  tskuni  10787  wfgru  10820  0nn0m1nnn0  12670  rpregt0  13051  supxrun  13362  elicore  13445  xrge0nre  13500  elfz1end  13603  elfzonlteqm1  13791  modfzo0difsn  14001  fzennn  14026  cardfz  14028  fsuppmapnn0fiub0  14051  ser0  14112  crreczi  14286  faclbnd  14348  bcn1  14371  hashrabsn01  14431  hashge0  14445  prsshashgt1  14469  hashssdif  14471  hashdifpr  14474  hashsn01  14475  hashgt23el  14483  hashpw  14495  hashres  14497  hash3tpexb  14553  ccatw2s1p1  14698  swrdswrd  14768  swrdccatin2  14792  pfxccatpfx1  14799  repsundef  14836  trclublem  15060  reltrclfv  15082  dmtrclfv  15083  cau3lem  15434  harmonic  15940  mertenslem2  15966  prodf1  15972  fprodfac  16054  rpnnen2lem12  16307  sqrt2irr0  16333  sadadd2lem2  16534  saddisjlem  16548  lcmftp  16720  lcmfunsnlem2lem1  16722  lcmfunsnlem2lem2  16723  prmind2  16769  prm2orodd  16775  pceq0  16957  prmreclem6  17007  0ram  17106  ram0  17108  cshwsiun  17185  ressbas2  17324  ressinbas  17331  ressval3d  17332  catpropd  17791  initoid  18084  termoid  18085  initoeu2lem0  18096  arwhoma  18128  joinfval  18453  meetfval  18467  lubun  18597  psssdm  18664  ex-chn1  18719  ex-chn2  18720  ismgmn0  18726  plusfeq  18732  idresefmnd  18999  qsxpid  19291  snsymgefmndeq  19513  fvcosymgeq  19547  pmtrprfv3  19572  pmtr3ncomlem1  19591  ablsubadd23  19931  ablsubsub23  19942  cygabl  20009  gsummptfzsplitl  20051  gsum2dlem1  20088  gsum2dlem2  20089  gsum2d  20090  rng1zrlem  20307  opprnzr  20674  cntzsubrng  20720  ringcinv  20824  opprdomn  20870  drngmcl  20909  staffn  21000  scafeq  21057  lbsexg  21342  rngridlmcl  21396  rnglidl1  21412  df2idl2  21450  2idlss  21455  ssdifidlprm  21540  prmirred  21678  frgpcyg  21777  ipfeq  21854  dsmmbas2  21941  zlmassa  22107  ply1bascl2  22418  lply1binom  22524  mamufacex  22607  matsubgcell  22645  matinvgcell  22646  matepmcl  22673  matepm2cl  22674  marrepcl  22775  marepvcl  22780  mulmarep1el  22783  mulmarep1gsum1  22784  mulmarep1gsum2  22785  nfimdetndef  22800  mdetfval1  22801  m1detdiag  22808  mdetdiag  22810  slesolinvbi  22892  pmatcoe1fsupp  22912  mat2pmatbas  22937  mat2pmatmul  22942  m2cpminvid2lem  22965  monmatcollpw  22990  pm2mpf1  23010  pm2mpghm  23027  cayhamlem1  23077  isbasis3g  23160  isopn2  23243  ntrval2  23262  toponmre  23304  innei  23336  restcld  23383  restcldi  23384  neitr  23391  discmp  23609  cmpsublem  23610  cmpsub  23611  ssref  23724  dissnref  23740  ptcnp  23834  imasnopn  23902  imasncld  23903  imasncls  23904  kqf  23959  fbun  24052  opnfbas  24054  supfil  24107  ufprim  24121  acufl  24129  filufint  24132  ufldom  24174  hausflf2  24210  alexsubALTlem4  24262  cnextfval  24274  cnextfun  24276  cnextfres1  24280  efmndtmd  24313  trust  24441  ustuqtop1  24453  metustid  24766  metustbl  24778  restmetu  24782  zlmclm  25326  cphassr  25426  ehleudisval  25633  ovolun  25713  vitalilem2  25823  dvcobr  26160  dvmptfsum  26189  rolle  26204  dvfsumlem2  26241  plyn0mulidp  26497  ulmcaulem  26612  logfac  26821  logno1  26856  logreclem  26982  prmorcht  27397  pclogsum  27434  gausslemma2dlem0i  27583  gausslemma2dlem1a  27584  2lgslem1c  27612  2sqlem10  27647  chto1lb  27697  cutsval  28028  addsproplem2  28218  oncutlt  28512  n0s0suc  28590  tgjustf  28797  tgldimor  28826  axcontlem7  29379  lfgredgge2  29533  edgupgr  29543  lfuhgr2  29558  ausgrusgrb  29577  ausgrumgri  29579  uspgredg2vlem  29635  uspgredg2v  29636  usgredg2vlem2  29638  usgredg2v  29639  ushgredgedg  29641  ushgredgedgloop  29643  griedg0ssusgr  29677  umgrres1lem  29722  upgrres1  29725  nbgrcl  29747  nbgrnvtx0  29751  nbuhgr  29755  nbuhgr2vtx1edgb  29764  edgnbusgreu  29779  nb3grprlem2  29793  nb3grpr2  29795  nb3gr2nb  29796  cplgr2vpr  29845  cplgr3v  29847  vtxdumgrval  29898  umgr2v2evtxel  29934  usgrvd0nedg  29945  finsumvtxdg2ssteplem4  29960  wlk1walk  30050  wlk0prc  30064  wlkp1lem8  30090  wlkp1  30091  spthdep  30151  usgr2pthlem  30180  usgr2pth  30181  crctprop  30210  cyclprop  30211  cyclnumvtx  30219  crctcshwlkn0  30241  wwlknllvtx  30266  wlkiswwlks1  30287  wlkswwlksf1o  30299  wwlksnextproplem3  30331  wwlksnwwlksnon  30335  umgr2wlkon  30370  wwlks2onv  30373  elwspths2on  30382  elwspths2onw  30383  elwwlks2  30389  elwspths2spth  30390  rusgrnumwwlks  30397  clwlkclwwlklem2a4  30419  clwlkclwwlklem2  30422  clwlkclwwlkf  30430  erclwwlkref  30442  erclwwlknref  30491  erclwwlknsym  30492  erclwwlkntr  30493  hashecclwwlkn1  30499  umgrhashecclwwlk  30500  clwlknf1oclwwlknlem1  30503  clwwlknon1  30519  clwwlknon1nloop  30521  clwwlkvbij  30535  0clwlkv  30553  uhgr3cyclex  30608  umgr3cyclex  30609  vdn0conngrumgrv2  30622  eupthi  30629  eucrctshift  30669  frcond1  30692  frcond4  30696  frgr3v  30701  3vfriswmgr  30704  1to2vfriswmgr  30705  1to3vfriswmgr  30706  2pthfrgr  30710  4cycl2v2nb  30715  n4cyclfrgr  30717  frgrnbnb  30719  frgrwopreglem4a  30736  clwlknon2num  30794  numclwwlkqhash  30801  frgrreg  30820  frgrregord013  30821  ex-ceil  30874  grpoidinvlem3  30933  nmlno0lem  31220  blocni  31232  pythi  31277  normpythi  31569  shmodsi  31816  pjchi  31859  chlubii  31899  osumi  32069  nmlnop0iALT  32422  cnlnssadj  32507  nmopcoi  32522  mdbr3  32724  mdbr4  32725  ssmd1  32738  dmdsl3  32742  mdexchi  32762  atssma  32805  atoml2i  32810  chirredlem3  32819  mdsymlem1  32830  dmdbr6ati  32850  dmdbr7ati  32851  cdjreui  32859  cdj3lem2b  32864  addltmulALT  32873  difuncomp  32973  iundifdif  32982  imadifxp  33021  fresf1o  33051  2ndimaxp  33066  acunirnmpt2  33080  suppiniseg  33106  fressupp  33108  fdifsuppconst  33109  ressupprn  33110  disjdsct  33123  1stpreimas  33126  preiman0  33130  resf1o  33149  xrge0addge  33177  xlt2addrd  33178  fz2ssnn0  33204  f1ocnt  33219  elq2  33230  nexple  33251  gsummpt2d  33437  gsumfs2d  33449  gsumwun  33464  psgnfzto1stlem  33488  fzto1st  33491  psgnfzto1st  33493  cycpmco2f1  33512  cycpmco2rn  33513  cycpmco2lem7  33520  elrgspn  33634  elrgspnsubrunlem2  33636  elrlocbasi  33655  ricnzr1  33676  sdrginvcl  33689  nsgqusf1olem2  33791  elrspunidl  33804  ssmxidl  33825  selvply1rhmlem2  33979  lbsdiflsp0  34084  fldextfld1  34105  fldextfld2  34106  constrconj  34203  constrllcllem  34210  constrlccllem  34211  constrcccllem  34212  submat1n  34263  submatres  34264  locfinreflem  34298  ldlfcntref  34312  zarclsun  34328  zarclsiin  34329  zarclsint  34330  zarcmplem  34339  mndpluscn  34384  pnfneige0  34409  pl1cn  34413  gsumesum  34517  esumcst  34521  esumrnmpt2  34526  esumcvgre  34549  esum2d  34551  pwsiga  34588  ldsysgenld  34619  measxun2  34669  volmeas  34690  ddemeas  34695  aean  34703  mbfmfun  34712  1stmbfm  34719  2ndmbfm  34720  omssubadd  34759  carsgclctunlem1  34776  sibfof  34799  eulerpartlemmf  34834  probun  34878  dstfrvclim1  34937  coinfliprv  34942  ballotlem2  34948  ballotlemic  34966  ballotlem1c  34967  signstres  35031  bnj529  35199  bnj1379  35287  bnj1424  35295  bnj1436  35296  bnj607  35373  bnj908  35388  bnj1097  35438  bnj1118  35441  bnj1128  35447  bnj1145  35450  bnj1154  35456  bnj1174  35460  bnj1189  35466  bnj1417  35498  axprALT2  35565  rankfo  35567  acnum  35586  tz9.1regs  35608  axsepg2  35614  axsepg4  35617  kardcard2b  35639  cusgr3cyclex  35673  cvmliftlem10  35827  satfv1  35896  fmlasuc0  35917  satffunlem2lem1  35937  mrsub0  36049  mrsubccat  36051  mrsubcn  36052  bcprod  36271  socnv  36297  dfon2lem3  36316  dfon2lem7  36320  dfon2lem8  36321  rdgprc0  36324  fvsingle  36451  unisnif  36456  funpartlem  36475  hfun  36711  ss-ax8  36798  trer  36888  clsun  36900  opnregcld  36902  cldregopn  36903  df3nandALT1  36971  lukshef-ax2  36987  nandsym1  36994  weiunfr  37039  dfttc4lem2  37101  knoppndvlem9  37170  bj-mt2bi  37221  bj-gl4  37249  bj-babygodel  37257  bj-babylob  37258  bj-ssbid2ALT  37346  bj-nfext  37400  bj-1upln0  37706  bj-snex  37732  eleq2w2ALT  37744  bj-brrelex12ALT  37764  bj-restsnid  37790  bj-snmooreb  37817  bj-opelrelex  37849  bj-inftyexpitaudisj  37910  bj-inftyexpidisj  37915  bj-elccinfty  37919  finorwe  38089  ctbssinf  38113  fvineqsnf1  38117  pibt2  38124  wl-ifpimpr  38173  wl-ifp4impr  38174  wl-1xor  38189  wl-1mintru1  38195  lindsadd  38325  lindsenlbs  38327  poimirlem9  38341  poimirlem13  38345  poimirlem14  38346  poimirlem25  38357  poimirlem26  38358  mblfinlem2  38370  mblfinlem3  38371  mblfinlem4  38372  ismblfin  38373  mbfresfi  38378  ftc1cnnc  38404  dvasin  38416  fnopabco  38436  frinfm  38448  caushft  38474  bndss  38499  notornotel1  38806  tsbi2  38845  rabeq12f  38868  relcnveq3  39038  relcnveq2  39040  cnvref4  39061  ralrnmo  39072  raldmqsmo  39074  disjressuc2  39122  cnvcosseq  39238  symrelcoss3  39266  dfrefrels2  39304  dfrefrel2  39306  dfcnvrefrels2  39319  dfcnvrefrel2  39321  dfsymrels2  39336  elrelscnveq3  39338  dfsymrel2  39344  symrefref2  39358  dftrrels2  39370  dftrrel2  39372  n0elim  39446  disjimeceqim  39515  membpartlem19  39625  axc11n-16  39774  glbconN  40213  paddssat  40650  pclunN  40734  paddunN  40763  poldmj1N  40764  ltrnnid  40972  dibglbN  42002  mndmolinv  42924  primrootsunit1  42926  primrootscoprmpow  42928  primrootscoprbij  42931  aks6d1c2lem4  42956  aks6d1c2  42959  aks6d1c5lem3  42966  deg1gprod  42969  sticksstones3  42977  sticksstones11  42985  sticksstones12a  42986  sticksstones12  42987  sticksstones13  42988  aks6d1c6isolem1  43003  aks6d1c6lem5  43006  grpods  43023  unitscyglem2  43025  unitscyglem3  43026  unitscyglem4  43027  aks5lem7  43029  exbiii  43041  sn-0ne2  43244  sn-0lt1  43326  istopclsd  43508  pellex  43639  monotoddzzfi  43746  jm2.23  43800  expdioph  43827  wopprc  43834  kelac1  43867  dfac21  43870  lsmfgcl  43878  pwssplit4  43893  isnumbasgrp  43911  dgraalem  43949  ordnexbtwnsuc  44071  cantnfresb  44128  dflim5  44133  rp-tfslim  44157  ifpbi1  44280  rp-fakeanorass  44316  rp-isfinite5  44320  iscard4  44336  minregex  44337  pr2cv  44351  superficl  44370  ssuncl  44373  sssymdifcl  44375  relintab  44386  cnvssb  44389  cotrintab  44417  clcnvlem  44426  cnvtrrel  44473  brfvrcld2  44495  relexpxpmin  44520  relexpaddss  44521  unhe1  44588  frege55lem1b  44698  frege58bid  44705  frege92  44758  uneqsn  44828  ntrk2imkb  44840  neik0pk1imk0  44850  gneispace  44937  k0004lem2  44951  k0004val0  44957  ismnushort  45088  pm10.12  45145  pm11.61  45180  sbiota1  45221  bi1imp  45268  bi2imp  45269  bi3impb  45270  bi3impa  45271  bi13impib  45273  bi123impib  45274  bi13impia  45275  bi123impia  45276  bi13imp23  45278  bi13imp2  45279  bi12imp3  45280  tratrb  45322  dfvd1imp  45361  dfvd2imp  45389  e1bi  45415  e2bi  45418  e3bi  45523  3ornot23VD  45632  3impexpbicomVD  45642  3impexpbicomiVD  45643  tratrbVD  45646  ssralv2VD  45651  equncomiVD  45654  truniALTVD  45663  ee33VD  45664  onfrALTlem3VD  45672  onfrALTlem2VD  45674  onfrALTlem1VD  45675  onfrALTVD  45676  relopabVD  45686  2uasbanhVD  45696  vk15.4jVD  45699  unisnALT  45711  chordthmALT  45718  iunconnlem2  45720  wfaxpow  45783  wfaxun  45785  fnchoice  45826  uzwo4  45850  inabs3  45853  rexanuz3  45891  disjrnmpt2  45983  disjinfi  45987  iunmapsn  46010  ssfiunibd  46105  iuneqfzuzlem  46127  iuneqfzuz  46128  xrge0ge0  46140  xrssre  46141  infrpge  46144  allbutfi  46185  supxrunb3  46191  eluzelz2  46194  uz0  46203  allbutfiinf  46211  infxrunb3rnmpt  46219  uzublem  46221  uzub  46222  uzid3  46226  infxrlesupxr  46227  infrpgernmpt  46256  supminfxrrnmpt  46262  rexanuz2nf  46283  eliocre  46302  lbioc  46306  ioonct  46330  uzinico  46352  fsumiunss  46368  fmuldfeq  46376  mccl  46391  climsuse  46401  islptre  46412  lptioo2  46424  lptioo1  46425  islpcn  46430  fnlimfvre  46465  climbddf  46478  limsupubuzlem  46503  limsupmnfuzlem  46517  limsupequzmptlem  46519  limsupre3uzlem  46526  xlimcl  46613  cnrefiisplem  46620  xlimliminflimsup  46653  icccncfext  46678  cncfiooicclem1  46684  cncfiooicc  46685  ioodvbdlimc1lem2  46723  ioodvbdlimc2lem  46725  dvnprodlem1  46737  dvnprodlem3  46739  volioc  46763  itgioocnicc  46768  stoweidlem28  46819  stoweidlem57  46848  wallispilem3  46858  wallispilem4  46859  wallispi  46861  wallispi2lem1  46862  wallispi2  46864  stirlinglem12  46876  fourierdlem42  46940  fourierdlem48  46945  fourierdlem50  46947  fourierdlem52  46949  fourierdlem71  46968  fourierdlem73  46970  fourierdlem74  46971  fourierdlem75  46972  fourierdlem76  46973  fourierdlem80  46977  fourierdlem93  46990  fourierdlem101  46998  fourierdlem103  47000  fourierdlem104  47001  fourierswlem  47021  fouriersw  47022  etransclem26  47051  etransclem37  47062  rrxsnicc  47091  saluncl  47108  intsaluni  47120  intsal  47121  salgencl  47123  salexct  47125  sssalgen  47126  salgenuni  47128  issalgend  47129  salgencntex  47134  subsaliuncllem  47148  subsaliuncl  47149  sge00  47167  sge0sn  47170  sge0cl  47172  sge0f1o  47173  sge0pnffigt  47187  sge0resplit  47197  sge0split  47200  sge0iunmptlemre  47206  sge0xaddlem2  47225  iundjiun  47251  meadjun  47253  meassle  47254  meadjiunlem  47256  meaiunlelem  47259  volmea  47265  caragenunidm  47299  omeunle  47307  omeiunltfirp  47310  caratheodorylem1  47317  caratheodory  47319  icoresmbl  47334  volicorescl  47344  ovncvrrp  47355  ovnsubaddlem2  47362  hoidmv1le  47385  hoidmvlelem1  47386  hoidmvlelem2  47387  hoidmvlelem5  47390  hoidmvle  47391  ovnhoilem2  47393  hspdifhsp  47407  hoiqssbllem3  47415  hspmbllem2  47418  ovolval4lem1  47440  ovnovollem3  47449  vonioolem1  47471  pimdecfgtioo  47508  pimincfltioo  47509  mbfresmf  47530  smfaddlem1  47554  smflimlem1  47562  smflimlem2  47563  smflimlem3  47564  smflim  47568  smfresal  47579  smfrec  47580  smfmullem4  47585  smfdiv  47588  smfpimbor1lem2  47590  smflimmpt  47601  smfsuplem1  47602  smfinflem  47608  smflimsuplem3  47613  smflimsuplem5  47615  smflimsuplem6  47616  smflimsuplem7  47617  smflimsupmpt  47620  smfliminflem  47621  smfliminfmpt  47623  simpcntrab  47661  quantgodelALT  47666  chnerlem1  47675  chnerlem2  47676  sqrtnzqaa  47682  cos5teq  47694  lambert0  47701  lamberte  47702  aifftbifffaibif  47735  aifftbifffaibifff  47736  abciffcbatnabciffncba  47743  abciffcbatnabciffncbai  47744  nabctnabc  47745  confun4  47756  confun5  47757  plcofph  47758  pldofph  47759  plvcofph  47760  plvcofphax  47761  plvofpos  47762  dandysum2p2e4  47812  fresfo  47862  fcores  47881  3f1oss1  47889  3f1oss2  47890  funfocofob  47892  aiotaint  47905  dfaiota3  47906  ndmaovrcl  48018  tz6.12-afv2  48054  fvmptrabdm  48107  difmodm1lt  48179  uniimafveqt  48207  uniimaelsetpreimafv  48222  iccpartiun  48260  iccpartdisj  48263  ich2exprop  48297  ichnreuop  48298  prpair  48327  fmtnorec2lem  48371  dfodd5  48502  stgoldbwt  48618  sbgoldbb  48624  nnsum3primesle9  48636  nnsum4primeseven  48642  clnbgrcl  48663  clnbgrnvtx0  48669  clnbgredg  48682  grimuhgr  48729  isuspgrim0  48736  isuspgrimlem  48737  gricushgr  48759  grtriclwlk3  48787  isubgr3stgrlem1  48808  isubgr3stgrlem7  48814  uspgrlimlem2  48831  uspgrlimlem4  48833  grlimprclnbgr  48838  gpgusgralem  48898  gpg5order  48902  gpg5nbgrvtx03star  48922  gpg5nbgr3star  48923  gpgvtxdg3  48924  gpg5gricstgr3  48932  pgnbgreunbgrlem3  48960  pgnbgreunbgrlem6  48966  pgnbgreunbgr  48967  pgn4cyclex  48968  lmod0rng  49070  lidldomnnring  49077  ringcinvALTV  49151  altgsumbcALT  49209  ply1sclrmsm  49240  linccl  49270  lincvalsng  49272  lincvalpr  49274  lincdifsn  49280  linc1  49281  lincsum  49285  lincscm  49286  lindslinindsimp2lem5  49318  lincresunit3lem2  49336  2sphere  49605  resinsnALT  49727  tposideq  49742  clduni  49755  neircl  49759  funcrcl2  49933  funcrcl3  49934  funcf2lem2  49936  uprcl2  50043  uprcl3  50044  swapf2fval  50119  swapf1val  50121  fucofvalne  50179  thincn0eu  50285  isinito3  50354  mndtcbas2  50437  alsralrex  50666