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  1636  nic-ax  1705  nfnt  1888  19.25  1914  nfimd  1928  19.37imv  1981  alcomimw  2077  sbbii  2114  nsb  2144  excomim  2202  stdpc5  2247  sbequ2  2287  sb9i  2552  mo4  2594  2mo  2676  ax9ALT  2758  eleq2w2  2759  eqeq1d  2765  r19.37v  3192  rmoeq1  3400  elabgt  3629  euind  3685  reuind  3714  sbcimdv  3810  sbcg  3814  ra4v  3836  ra4  3837  csbied  3887  ssrmof  3981  elunnel1  4156  elunnel2  4157  unssd  4193  n0moeu  4310  eqeuel  4316  ss0  4355  iftrueb  4498  elinsn  4671  disjtp2  4677  rabsnif  4684  prprc  4728  elpwdifsn  4752  ssunsn2  4786  preqr1  4806  intss2  5071  disjxiun  5103  unisn2  5269  snexALT  5349  reusv3i  5370  snexOLD  5404  pocl  5571  brrelex12  5707  0nelrel0  5715  elrel  5779  exopxfr2  5827  dmxp  5916  xpssres  6013  elinxp  6014  imadisjlnd  6084  elimasni  6095  inisegn0  6102  xpdifid  6165  xpdifcnvepel  6166  cnvssb  6195  imadifssranOLDOLD  6210  dmsnsnsn  6228  relcnvtrgOLD  6276  xpco  6299  reuop  6303  predprc  6348  sucprc  6448  onunel  6477  iotaint  6524  iotanul  6526  funun  6595  funcnv3  6621  funimass1  6633  funssxp  6749  f0dom0  6777  dffv3  6892  dffv2  6991  fsneq  7045  fndmin  7055  sspreima  7078  iinpreima  7080  fveqressseq  7090  fsn2  7148  f1ounsn  7290  f12dfv  7291  f13dfv  7292  isoselem  7359  oprabidw  7461  oprabid  7462  ovima0  7610  sorpsscmpl  7760  abnex  7781  pwuncl  7794  ordsuci  7832  peano2  7911  1stval  8013  2ndval  8014  1stdm  8061  oprabco  8119  f1o2ndf1  8146  poxp  8153  frxp3  8181  suppval1  8197  fnsuppeq0  8223  frrlem4  8321  tz7.48lemOLD  8465  tz7.49c  8470  ord1eln01  8518  ord2eln012  8519  undifixp  8976  bren2  9024  ensym  9044  en1uniel  9071  domunsn  9160  limenpsi  9185  findcard2  9194  unfi  9200  pwssfi  9206  php4  9239  isinf  9270  en2  9285  fiint  9332  rneqdmfinf1o  9336  elfiun  9435  marypha1lem  9438  supval2  9460  eqinf  9490  brwdom2  9580  zfreg  9603  tcmin  9753  frmin  9766  prwf  9832  r1pw  9872  rankuni2b  9880  rankr1id  9891  hfun  9931  hfunOLD  9932  djuun  10020  cardval3  10046  ficardom  10055  cardmin2  10093  isinfcard  10184  iscard3  10185  alephval3  10202  dfac9  10228  kmlem6  10247  fin23lem29  10432  fin23lem30  10433  isf32lem11  10454  isfin1-3  10477  fin45  10483  fin1a2lem12  10502  fin1a2lem13  10503  axcc2lem  10527  dominf  10536  axdc4lem  10546  dominfac  10671  pwcfsdom  10681  cfpwsdom  10682  tskuni  10881  wfgru  10914  0nn0m1nnn0  12766  rpregt0  13148  supxrun  13459  elicore  13542  xrge0nre  13597  elfz1end  13701  elfzonlteqm1  13889  modfzo0difsn  14099  fzennn  14124  cardfz  14126  fsuppmapnn0fiub0  14149  ser0  14210  crreczi  14385  faclbnd  14447  bcn1  14470  hashrabsn01  14530  hashge0  14544  prsshashgt1  14568  hashssdif  14570  hashdifpr  14573  hashsn01  14574  hashgt23el  14582  hashpw  14594  hashres  14596  hash3tpexb  14652  ccatw2s1p1  14798  swrdswrd  14868  swrdccatin2  14892  pfxccatpfx1  14899  repsundef  14936  trclublem  15163  reltrclfv  15185  dmtrclfv  15186  cau3lem  15537  harmonic  16043  mertenslem2  16069  prodf1  16075  fprodfac  16155  rpnnen2lem12  16408  sqrt2irr0  16434  sadadd2lem2  16635  saddisjlem  16649  lcmftp  16826  lcmfunsnlem2lem1  16828  lcmfunsnlem2lem2  16829  prmind2  16875  prm2orodd  16881  pceq0  17064  prmreclem6  17114  0ram  17213  ram0  17215  cshwsiun  17292  ressbas2  17431  ressinbas  17438  ressval3d  17439  catpropd  17898  initoid  18191  termoid  18192  initoeu2lem0  18203  arwhoma  18235  joinfval  18560  meetfval  18574  lubun  18704  psssdm  18771  ex-chn1  18826  ex-chn2  18827  ismgmn0  18833  plusfeq  18839  idresefmnd  19110  qsxpid  19402  snsymgefmndeq  19624  fvcosymgeq  19658  pmtrprfv3  19683  pmtr3ncomlem1  19702  ablsubadd23  20042  ablsubsub23  20053  cygabl  20120  gsummptfzsplitl  20162  gsum2dlem1  20199  gsum2dlem2  20200  gsum2d  20201  rng1zrlem  20418  opprnzr  20788  cntzsubrng  20834  ringcinv  20938  opprdomn  20984  drngmcl  21024  staffn  21115  scafeq  21172  lbsexg  21457  rngridlmcl  21511  rnglidl1  21527  2idl1el  21564  df2idl2  21566  2idlss  21571  ssdifidlprm  21657  prmirred  21795  frgpcyg  21894  ipfeq  21971  dsmmbas2  22058  lindsenlbs  22172  zlmassa  22226  ply1bascl2  22537  lply1binom  22643  mamufacex  22726  matsubgcell  22764  matinvgcell  22765  matepmcl  22792  matepm2cl  22793  marrepcl  22894  marepvcl  22899  mulmarep1el  22902  mulmarep1gsum1  22903  mulmarep1gsum2  22904  nfimdetndef  22919  mdetfval1  22920  m1detdiag  22927  mdetdiag  22929  slesolinvbi  23014  pmatcoe1fsupp  23034  mat2pmatbas  23059  mat2pmatmul  23064  m2cpminvid2lem  23087  monmatcollpw  23112  pm2mpf1  23132  pm2mpghm  23149  cayhamlem1  23199  isbasis3g  23282  isopn2  23365  ntrval2  23384  toponmre  23426  innei  23458  restcld  23505  restcldi  23506  neitr  23513  discmp  23731  cmpsublem  23732  cmpsub  23733  ssref  23846  dissnref  23862  ptcnp  23956  imasnopn  24024  imasncld  24025  imasncls  24026  kqf  24081  fbun  24174  opnfbas  24176  supfil  24229  ufprim  24243  acufl  24251  filufint  24254  ufldom  24296  hausflf2  24332  alexsubALTlem4  24384  cnextfval  24396  cnextfun  24398  cnextfres1  24402  efmndtmd  24435  trust  24563  ustuqtop1  24575  metustid  24888  metustbl  24900  restmetu  24904  zlmclm  25448  cphassr  25548  ehleudisval  25755  ovolun  25835  vitalilem2  25945  dvcobr  26281  dvmptfsum  26310  rolle  26325  dvfsumlem2  26362  plyn0mulidp  26617  ulmcaulem  26736  logfac  26944  logno1  26979  logreclem  27105  prmorcht  27520  pclogsum  27557  gausslemma2dlem0i  27706  gausslemma2dlem1a  27707  2lgslem1c  27735  2sqlem10  27770  chto1lb  27820  cutsval  28181  addsproplem2  28371  oncutlt  28665  n0s0suc  28743  tgjustf  28950  tgldimor  28980  cgraer  29392  angmgmlem  29410  axcontlem7  29563  lfgredgge2  29717  edgupgr  29727  lfuhgr2  29742  ausgrusgrb  29761  ausgrumgri  29763  uspgredg2vlem  29819  uspgredg2v  29820  usgredg2vlem2  29822  usgredg2v  29823  ushgredgedg  29825  ushgredgedgloop  29827  griedg0ssusgr  29861  umgrres1lem  29906  upgrres1  29909  nbgrcl  29931  nbgrnvtx0  29935  nbuhgr  29939  nbuhgr2vtx1edgb  29948  edgnbusgreu  29963  nb3grprlem2  29977  nb3grpr2  29979  nb3gr2nb  29980  cplgr2vpr  30029  cplgr3v  30031  vtxdumgrval  30082  umgr2v2evtxel  30118  usgrvd0nedg  30129  finsumvtxdg2ssteplem4  30144  wlk1walk  30234  wlk0prc  30248  wlkp1lem8  30274  wlkp1  30275  spthdep  30335  usgr2pthlem  30364  usgr2pth  30365  crctprop  30394  cyclprop  30395  cyclnumvtx  30403  crctcshwlkn0  30425  wwlknllvtx  30450  wlkiswwlks1  30471  wlkswwlksf1o  30483  wwlksnextproplem3  30515  wwlksnwwlksnon  30519  umgr2wlkon  30554  wwlks2onv  30557  elwspths2on  30566  elwspths2onw  30567  elwwlks2  30573  elwspths2spth  30574  rusgrnumwwlks  30581  clwlkclwwlklem2a4  30603  clwlkclwwlklem2  30606  clwlkclwwlkf  30614  erclwwlkref  30626  erclwwlknref  30675  erclwwlknsym  30676  erclwwlkntr  30677  hashecclwwlkn1  30683  umgrhashecclwwlk  30684  clwlknf1oclwwlknlem1  30687  clwwlknon1  30703  clwwlknon1nloop  30705  clwwlkvbij  30719  0clwlkv  30737  uhgr3cyclex  30798  umgr3cyclex  30799  vdn0conngrumgrv2  30812  eupthi  30819  eucrctshift  30859  frcond1  30882  frcond4  30886  frgr3v  30891  3vfriswmgr  30894  1to2vfriswmgr  30895  1to3vfriswmgr  30896  2pthfrgr  30900  4cycl2v2nb  30905  n4cyclfrgr  30907  frgrnbnb  30909  frgrwopreglem4a  30926  clwlknon2num  30984  numclwwlkqhash  30991  frgrreg  31010  frgrregord013  31011  ex-ceil  31064  grpoidinvlem3  31123  nmlno0lem  31410  blocni  31422  pythi  31467  normpythi  31759  shmodsi  32006  pjchi  32049  chlubii  32089  osumi  32259  nmlnop0iALT  32612  cnlnssadj  32697  nmopcoi  32712  mdbr3  32914  mdbr4  32915  ssmd1  32928  dmdsl3  32932  mdexchi  32952  atssma  32995  atoml2i  33000  chirredlem3  33009  mdsymlem1  33020  dmdbr6ati  33040  dmdbr7ati  33041  cdjreui  33049  cdj3lem2b  33054  addltmulALT  33105  difuncomp  33205  iundifdif  33214  imadifxp  33252  fresf1o  33282  2ndimaxp  33297  suppiniseg  33336  fressupp  33338  fdifsuppconst  33339  ressupprn  33340  disjdsct  33353  1stpreimas  33356  preiman0  33360  resf1o  33378  xrge0addge  33406  xlt2addrd  33407  fz2ssnn0  33433  f1ocnt  33448  elq2  33459  nexple  33480  gsummpt2d  33666  gsumfs2d  33678  gsumwun  33693  psgnfzto1stlem  33717  fzto1st  33720  psgnfzto1st  33722  cycpmco2f1  33741  cycpmco2rn  33742  cycpmco2lem7  33749  elrgspn  33863  elrgspnsubrunlem2  33865  elrlocbasi  33884  ricnzr1  33905  sdrginvcl  33918  rsp2idlid  33987  nsgqusf1olem2  34021  elrspunidl  34034  ssmxidl  34055  lbsdiflsp0  34314  fldextfld1  34335  fldextfld2  34336  constrconj  34433  constrllcllem  34440  constrlccllem  34441  constrcccllem  34442  submat1n  34493  submatres  34494  locfinreflem  34528  ldlfcntref  34542  zarclsun  34558  zarclsiin  34559  zarclsint  34560  zarcmplem  34569  mndpluscn  34614  pnfneige0  34639  pl1cn  34643  gsumesum  34747  esumcst  34751  esumrnmpt2  34756  esumcvgre  34779  esum2d  34781  pwsiga  34818  ldsysgenld  34849  measxun2  34899  volmeas  34920  ddemeas  34925  aean  34933  mbfmfun  34942  1stmbfm  34948  2ndmbfm  34949  carsgclctunlem1  35005  sibfof  35028  eulerpartlemmf  35063  probun  35107  dstfrvclim1  35166  coinfliprv  35171  ballotlem2  35177  ballotlemic  35195  ballotlem1c  35196  signstres  35260  bnj529  35428  bnj1379  35516  bnj1424  35524  bnj1436  35525  bnj607  35602  bnj908  35617  bnj1097  35667  bnj1118  35670  bnj1128  35676  bnj1145  35679  bnj1154  35685  bnj1174  35689  bnj1189  35695  bnj1417  35727  ordunmax  35775  soinfdom  35780  axprALT2  35798  rankfo  35799  acnum  35829  weexenwe  35830  tz9.1regs  35876  axsepg2  35882  axsepg4  35885  kardcard2b  35907  maxssj0  35963  j0ltaleph  35965  cusgr3cyclex  36025  smrepsrep  36045  cvmliftlem10  36183  satfv1  36252  fmlasuc0  36273  satffunlem2lem1  36293  mrsub0  36405  mrsubccat  36407  mrsubcn  36408  bcprod  36633  socnv  36659  dfon2lem3  36677  dfon2lem7  36681  dfon2lem8  36682  rdgprc0  36685  fvsingle  36812  unisnif  36817  funpartlem  36836  ss-ax8  37144  trer  37234  clsun  37246  opnregcld  37248  cldregopn  37249  df3nandALT1  37317  lukshef-ax2  37333  nandsym1  37340  weiunfr  37385  dfttc4lem2  37447  knoppndvlem9  37516  bj-mt2bi  37567  bj-gl4  37595  bj-babygodel  37603  bj-babylob  37604  bj-ssbid2ALT  37692  bj-nfext  37746  bj-1upln0  38052  bj-snex  38078  eleq2w2ALT  38104  bj-brrelex12ALT  38124  bj-restsnid  38150  bj-snmooreb  38177  bj-opelrelex  38208  bj-inftyexpitaudisj  38269  bj-inftyexpidisj  38274  bj-elccinfty  38278  finorwe  38448  ctbssinf  38472  fvineqsnf1  38476  pibt2  38483  wl-ifpimpr  38532  wl-ifp4impr  38533  wl-1xor  38548  wl-1mintru1  38554  lindsadd  38679  poimirlem9  38690  poimirlem13  38694  poimirlem14  38695  poimirlem25  38706  poimirlem26  38707  mblfinlem2  38719  mblfinlem3  38720  mblfinlem4  38721  ismblfin  38722  mbfresfi  38727  ftc1cnnc  38753  dvasin  38765  fnopabco  38800  frinfm  38812  caushft  38838  bndss  38863  notornotel1  39170  tsbi2  39209  rabeq12f  39232  relcnveq3  39402  relcnveq2  39404  cnvref4  39425  ralrnmo  39436  raldmqsmo  39438  disjressuc2  39486  cnvcosseq  39602  symrelcoss3  39630  dfrefrels2  39668  dfrefrel2  39670  dfcnvrefrels2  39683  dfcnvrefrel2  39685  dfsymrels2  39700  elrelscnveq3  39702  dfsymrel2  39708  symrefref2  39722  dftrrels2  39734  dftrrel2  39736  n0elim  39810  disjimeceqim  39879  membpartlem19  39989  axc11n-16  40138  glbconN  40577  paddssat  41014  pclunN  41098  paddunN  41127  poldmj1N  41128  ltrnnid  41336  dibglbN  42366  mndmolinv  43288  primrootsunit1  43290  primrootscoprmpow  43292  primrootscoprbij  43295  aks6d1c2lem4  43320  aks6d1c2  43323  aks6d1c5lem3  43330  deg1gprod  43333  sticksstones3  43341  sticksstones11  43349  sticksstones12a  43350  sticksstones12  43351  sticksstones13  43352  aks6d1c6isolem1  43367  aks6d1c6lem5  43370  grpods  43387  unitscyglem2  43389  unitscyglem3  43390  unitscyglem4  43391  aks5lem7  43393  exbiii  43405  sn-0ne2  43600  sn-0lt1  43682  istopclsd  43854  pellex  43985  monotoddzzfi  44092  jm2.23  44146  expdioph  44173  wopprc  44180  kelac1  44208  dfac21  44211  lsmfgcl  44219  pwssplit4  44234  isnumbasgrp  44252  dgraalem  44290  ordnexbtwnsuc  44412  cantnfresb  44469  dflim5  44474  rp-tfslim  44498  ifpbi1  44621  rp-fakeanorass  44657  rp-isfinite5  44661  iscard4  44677  minregex  44678  pr2cv  44692  superficl  44711  ssuncl  44714  sssymdifcl  44716  relintab  44727  cotrintab  44757  clcnvlem  44766  cnvtrrel  44813  brfvrcld2  44835  relexpxpmin  44860  relexpaddss  44861  unhe1  44928  frege55lem1b  45038  frege58bid  45045  frege92  45098  uneqsn  45168  ntrk2imkb  45180  neik0pk1imk0  45190  gneispace  45277  k0004lem2  45291  k0004val0  45297  ismnushort  45428  pm10.12  45485  pm11.61  45520  sbiota1  45560  bi1imp  45607  bi2imp  45608  bi3impb  45609  bi3impa  45610  bi13impib  45612  bi123impib  45613  bi13impia  45614  bi123impia  45615  bi13imp23  45617  bi13imp2  45618  bi12imp3  45619  tratrb  45661  dfvd1imp  45700  dfvd2imp  45728  e1bi  45754  e2bi  45757  e3bi  45862  3ornot23VD  45971  3impexpbicomVD  45981  3impexpbicomiVD  45982  tratrbVD  45985  ssralv2VD  45990  equncomiVD  45993  truniALTVD  46002  ee33VD  46003  onfrALTlem3VD  46011  onfrALTlem2VD  46013  onfrALTlem1VD  46014  onfrALTVD  46015  relopabVD  46025  2uasbanhVD  46035  vk15.4jVD  46038  unisnALT  46050  chordthmALT  46057  iunconnlem2  46059  wfaxpow  46129  wfaxun  46131  hfstructfun  46168  fnchoice  46188  uzwo4  46212  inabs3  46215  rexanuz3  46253  disjrnmpt2  46345  disjinfi  46349  iunmapsn  46372  ssfiunibd  46467  iuneqfzuzlem  46488  iuneqfzuz  46489  xrge0ge0  46501  xrssre  46502  infrpge  46505  allbutfi  46546  supxrunb3  46552  eluzelz2  46555  uz0  46564  allbutfiinf  46572  infxrunb3rnmpt  46580  uzublem  46582  uzub  46583  uzid3  46587  infxrlesupxr  46588  infrpgernmpt  46617  supminfxrrnmpt  46623  rexanuz2nf  46644  eliocre  46663  lbioc  46667  ioonct  46691  uzinico  46713  fsumiunss  46729  fmuldfeq  46737  mccl  46752  climsuse  46762  islptre  46773  lptioo2  46785  lptioo1  46786  islpcn  46791  fnlimfvre  46826  climbddf  46839  limsupubuzlem  46864  limsupmnfuzlem  46878  limsupequzmptlem  46880  limsupre3uzlem  46887  xlimcl  46974  cnrefiisplem  46981  xlimliminflimsup  47014  icccncfext  47039  cncfiooicclem1  47045  cncfiooicc  47046  ioodvbdlimc1lem2  47084  ioodvbdlimc2lem  47086  dvnprodlem1  47098  dvnprodlem3  47100  volioc  47124  itgioocnicc  47129  stoweidlem28  47180  stoweidlem57  47209  wallispilem3  47219  wallispilem4  47220  wallispi  47222  wallispi2lem1  47223  wallispi2  47225  stirlinglem12  47237  fourierdlem42  47301  fourierdlem48  47306  fourierdlem50  47308  fourierdlem52  47310  fourierdlem71  47329  fourierdlem73  47331  fourierdlem74  47332  fourierdlem75  47333  fourierdlem76  47334  fourierdlem80  47338  fourierdlem93  47351  fourierdlem101  47359  fourierdlem103  47361  fourierdlem104  47362  fourierswlem  47382  fouriersw  47383  etransclem26  47412  etransclem37  47423  rrxsnicc  47452  saluncl  47469  intsaluni  47481  intsal  47482  salgencl  47484  salexct  47486  sssalgen  47487  salgenuni  47489  issalgend  47490  salgencntex  47495  subsaliuncllem  47509  subsaliuncl  47510  sge00  47528  sge0sn  47531  sge0cl  47533  sge0f1o  47534  sge0pnffigt  47548  sge0resplit  47558  sge0split  47561  sge0iunmptlemre  47567  sge0xaddlem2  47586  iundjiun  47612  meadjun  47614  meassle  47615  meadjiunlem  47617  meaiunlelem  47620  volmea  47626  caragenunidm  47660  omeunle  47668  omeiunltfirp  47671  caratheodorylem1  47678  caratheodory  47680  icoresmbl  47695  volicorescl  47705  ovncvrrp  47716  ovnsubaddlem2  47723  hoidmv1le  47746  hoidmvlelem1  47747  hoidmvlelem2  47748  hoidmvlelem5  47751  hoidmvle  47752  ovnhoilem2  47754  hspdifhsp  47768  hoiqssbllem3  47776  hspmbllem2  47779  ovolval4lem1  47801  ovnovollem3  47810  vonioolem1  47832  pimdecfgtioo  47869  pimincfltioo  47870  mbfresmf  47891  smfaddlem1  47915  smflimlem1  47923  smflimlem2  47924  smflimlem3  47925  smflim  47929  smfresal  47940  smfrec  47941  smfmullem4  47946  smfdiv  47949  smfpimbor1lem2  47951  smflimmpt  47962  smfsuplem1  47963  smfinflem  47969  smflimsuplem3  47974  smflimsuplem5  47976  smflimsuplem6  47977  smflimsuplem7  47978  smflimsupmpt  47981  smfliminflem  47982  smfliminfmpt  47984  simpcntrab  48022  quantgodelALT  48027  chnerlem1  48034  chnerlem2  48035  cos5teq  48068  lambert0  48079  lamberte  48080  aifftbifffaibif  48133  aifftbifffaibifff  48134  abciffcbatnabciffncba  48141  abciffcbatnabciffncbai  48142  nabctnabc  48143  confun4  48154  confun5  48155  plcofph  48156  pldofph  48157  plvcofph  48158  plvcofphax  48159  plvofpos  48160  dandysum2p2e4  48210  fresfo  48260  fcores  48279  3f1oss1  48287  3f1oss2  48288  funfocofob  48290  aiotaint  48303  dfaiota3  48304  ndmaovrcl  48416  tz6.12-afv2  48452  fvmptrabdm  48505  difmodm1lt  48577  uniimafveqt  48605  uniimaelsetpreimafv  48620  iccpartiun  48658  iccpartdisj  48661  ich2exprop  48695  ichnreuop  48696  prpair  48725  fmtnorec2lem  48769  dfodd5  48900  stgoldbwt  49016  sbgoldbb  49022  nnsum3primesle9  49034  nnsum4primeseven  49040  clnbgrcl  49061  clnbgrnvtx0  49067  clnbgredg  49080  grimuhgr  49127  isuspgrim0  49134  isuspgrimlem  49135  gricushgr  49157  grtriclwlk3  49185  isubgr3stgrlem1  49206  isubgr3stgrlem7  49212  uspgrlimlem2  49229  uspgrlimlem4  49231  grlimprclnbgr  49236  gpgusgralem  49296  gpg5order  49300  gpg5nbgrvtx03star  49320  gpg5nbgr3star  49321  gpgvtxdg3  49322  gpg5gricstgr3  49330  pgnbgreunbgrlem3  49358  pgnbgreunbgrlem6  49364  pgnbgreunbgr  49365  pgn4cyclex  49366  lmod0rng  49468  lidldomnnring  49475  ringcinvALTV  49549  altgsumbcALT  49607  ply1sclrmsm  49638  linccl  49668  lincvalsng  49670  lincvalpr  49672  lincdifsn  49678  linc1  49679  lincsum  49683  lincscm  49684  lindslinindsimp2lem5  49716  lincresunit3lem2  49734  2sphere  50003  resinsnALT  50128  tposideq  50143  clduni  50157  neircl  50161  funcrcl2  50335  funcrcl3  50336  funcf2lem2  50338  uprcl2  50447  uprcl3  50448  swapf2fval  50529  swapf1val  50531  fucofvalne  50589  thincn0eu  50708  isinito3  50777  mndtcobeq  50863  alsralrex  51125