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  2143  excomim  2200  stdpc5  2245  sbequ2  2285  sb9i  2550  mo4  2592  2mo  2674  ax9ALT  2756  eleq2w2  2757  eqeq1d  2763  r19.37v  3189  rmoeq1  3397  elabgt  3626  euind  3682  reuind  3711  sbcimdv  3807  sbcg  3811  ra4v  3832  ra4  3833  csbied  3883  ssrmof  3999  elunnel1  4101  elunnel2  4102  unssd  4138  n0moeu  4307  eqeuel  4313  ss0  4352  iftrueb  4495  elinsn  4671  disjtp2  4677  rabsnif  4684  prprc  4728  elpwdifsn  4752  ssunsn2  4788  preqr1  4808  intss2  5068  disjxiun  5100  unisn2  5266  snexALT  5345  reusv3i  5366  snexOLD  5400  pocl  5567  brrelex12  5703  0nelrel0  5711  elrel  5774  exopxfr2  5822  dmxp  5911  xpssres  6007  elinxp  6008  imadisjlnd  6078  elimasni  6089  inisegn0  6096  xpdifid  6159  xpdifcnvepel  6160  cnvssb  6189  imadifssranOLDOLD  6203  dmsnsnsn  6221  relcnvtrgOLD  6269  xpco  6292  reuop  6296  predprc  6341  sucprc  6441  onunel  6470  iotaint  6516  iotanul  6518  funun  6586  funcnv3  6610  funimass1  6622  funssxp  6738  f0dom0  6766  dffv3  6881  dffv2  6980  fsneq  7034  fndmin  7044  sspreima  7067  iinpreima  7069  fveqressseq  7079  fsn2  7137  f1ounsn  7280  f12dfv  7281  f13dfv  7282  isoselem  7349  oprabidw  7451  oprabid  7452  ovima0  7600  sorpsscmpl  7750  abnex  7771  pwuncl  7784  ordsuci  7822  peano2  7901  1stval  8003  2ndval  8004  1stdm  8051  oprabco  8107  f1o2ndf1  8133  poxp  8140  frxp3  8168  suppval1  8183  fnsuppeq0  8209  frrlem4  8307  tz7.48lemOLD  8451  tz7.49c  8456  ord1eln01  8504  ord2eln012  8505  undifixp  8962  bren2  9010  ensym  9030  en1uniel  9057  domunsn  9146  limenpsi  9171  findcard2  9180  unfi  9186  pwssfi  9192  php4  9225  isinf  9256  en2  9271  fiint  9318  rneqdmfinf1o  9322  elfiun  9422  marypha1lem  9425  supval2  9447  eqinf  9477  brwdom2  9567  zfreg  9590  tcmin  9740  frmin  9753  prwf  9819  r1pw  9859  rankuni2b  9867  rankr1id  9878  hfun  9918  hfunOLD  9919  djuun  10007  cardval3  10033  ficardom  10042  cardmin2  10080  isinfcard  10171  iscard3  10172  alephval3  10189  dfac9  10215  kmlem6  10234  fin23lem29  10419  fin23lem30  10420  isf32lem11  10441  isfin1-3  10464  fin45  10470  fin1a2lem12  10489  fin1a2lem13  10490  axcc2lem  10514  dominf  10523  axdc4lem  10533  dominfac  10658  pwcfsdom  10668  cfpwsdom  10669  tskuni  10868  wfgru  10901  0nn0m1nnn0  12753  rpregt0  13135  supxrun  13446  elicore  13529  xrge0nre  13584  elfz1end  13688  elfzonlteqm1  13876  modfzo0difsn  14086  fzennn  14111  cardfz  14113  fsuppmapnn0fiub0  14136  ser0  14197  crreczi  14372  faclbnd  14434  bcn1  14457  hashrabsn01  14517  hashge0  14531  prsshashgt1  14555  hashssdif  14557  hashdifpr  14560  hashsn01  14561  hashgt23el  14569  hashpw  14581  hashres  14583  hash3tpexb  14639  ccatw2s1p1  14784  swrdswrd  14854  swrdccatin2  14878  pfxccatpfx1  14885  repsundef  14922  trclublem  15148  reltrclfv  15170  dmtrclfv  15171  cau3lem  15522  harmonic  16028  mertenslem2  16054  prodf1  16060  fprodfac  16140  rpnnen2lem12  16393  sqrt2irr0  16419  sadadd2lem2  16620  saddisjlem  16634  lcmftp  16811  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  prmind2  16860  prm2orodd  16866  pceq0  17049  prmreclem6  17099  0ram  17198  ram0  17200  cshwsiun  17277  ressbas2  17416  ressinbas  17423  ressval3d  17424  catpropd  17883  initoid  18176  termoid  18177  initoeu2lem0  18188  arwhoma  18220  joinfval  18545  meetfval  18559  lubun  18689  psssdm  18756  ex-chn1  18811  ex-chn2  18812  ismgmn0  18818  plusfeq  18824  idresefmnd  19095  qsxpid  19387  snsymgefmndeq  19609  fvcosymgeq  19643  pmtrprfv3  19668  pmtr3ncomlem1  19687  ablsubadd23  20027  ablsubsub23  20038  cygabl  20105  gsummptfzsplitl  20147  gsum2dlem1  20184  gsum2dlem2  20185  gsum2d  20186  rng1zrlem  20403  opprnzr  20773  cntzsubrng  20819  ringcinv  20923  opprdomn  20969  drngmcl  21009  staffn  21100  scafeq  21157  lbsexg  21442  rngridlmcl  21496  rnglidl1  21512  2idl1el  21549  df2idl2  21551  2idlss  21556  ssdifidlprm  21642  prmirred  21780  frgpcyg  21879  ipfeq  21956  dsmmbas2  22043  lindsenlbs  22157  zlmassa  22211  ply1bascl2  22522  lply1binom  22628  mamufacex  22711  matsubgcell  22749  matinvgcell  22750  matepmcl  22777  matepm2cl  22778  marrepcl  22879  marepvcl  22884  mulmarep1el  22887  mulmarep1gsum1  22888  mulmarep1gsum2  22889  nfimdetndef  22904  mdetfval1  22905  m1detdiag  22912  mdetdiag  22914  slesolinvbi  22999  pmatcoe1fsupp  23019  mat2pmatbas  23044  mat2pmatmul  23049  m2cpminvid2lem  23072  monmatcollpw  23097  pm2mpf1  23117  pm2mpghm  23134  cayhamlem1  23184  isbasis3g  23267  isopn2  23350  ntrval2  23369  toponmre  23411  innei  23443  restcld  23490  restcldi  23491  neitr  23498  discmp  23716  cmpsublem  23717  cmpsub  23718  ssref  23831  dissnref  23847  ptcnp  23941  imasnopn  24009  imasncld  24010  imasncls  24011  kqf  24066  fbun  24159  opnfbas  24161  supfil  24214  ufprim  24228  acufl  24236  filufint  24239  ufldom  24281  hausflf2  24317  alexsubALTlem4  24369  cnextfval  24381  cnextfun  24383  cnextfres1  24387  efmndtmd  24420  trust  24548  ustuqtop1  24560  metustid  24873  metustbl  24885  restmetu  24889  zlmclm  25433  cphassr  25533  ehleudisval  25740  ovolun  25820  vitalilem2  25930  dvcobr  26266  dvmptfsum  26295  rolle  26310  dvfsumlem2  26347  plyn0mulidp  26602  ulmcaulem  26721  logfac  26929  logno1  26964  logreclem  27090  prmorcht  27505  pclogsum  27542  gausslemma2dlem0i  27691  gausslemma2dlem1a  27692  2lgslem1c  27720  2sqlem10  27755  chto1lb  27805  cutsval  28166  addsproplem2  28356  oncutlt  28650  n0s0suc  28728  tgjustf  28935  tgldimor  28965  cgraer  29377  angmgmlem  29395  axcontlem7  29548  lfgredgge2  29702  edgupgr  29712  lfuhgr2  29727  ausgrusgrb  29746  ausgrumgri  29748  uspgredg2vlem  29804  uspgredg2v  29805  usgredg2vlem2  29807  usgredg2v  29808  ushgredgedg  29810  ushgredgedgloop  29812  griedg0ssusgr  29846  umgrres1lem  29891  upgrres1  29894  nbgrcl  29916  nbgrnvtx0  29920  nbuhgr  29924  nbuhgr2vtx1edgb  29933  edgnbusgreu  29948  nb3grprlem2  29962  nb3grpr2  29964  nb3gr2nb  29965  cplgr2vpr  30014  cplgr3v  30016  vtxdumgrval  30067  umgr2v2evtxel  30103  usgrvd0nedg  30114  finsumvtxdg2ssteplem4  30129  wlk1walk  30219  wlk0prc  30233  wlkp1lem8  30259  wlkp1  30260  spthdep  30320  usgr2pthlem  30349  usgr2pth  30350  crctprop  30379  cyclprop  30380  cyclnumvtx  30388  crctcshwlkn0  30410  wwlknllvtx  30435  wlkiswwlks1  30456  wlkswwlksf1o  30468  wwlksnextproplem3  30500  wwlksnwwlksnon  30504  umgr2wlkon  30539  wwlks2onv  30542  elwspths2on  30551  elwspths2onw  30552  elwwlks2  30558  elwspths2spth  30559  rusgrnumwwlks  30566  clwlkclwwlklem2a4  30588  clwlkclwwlklem2  30591  clwlkclwwlkf  30599  erclwwlkref  30611  erclwwlknref  30660  erclwwlknsym  30661  erclwwlkntr  30662  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  clwlknf1oclwwlknlem1  30672  clwwlknon1  30688  clwwlknon1nloop  30690  clwwlkvbij  30704  0clwlkv  30722  uhgr3cyclex  30783  umgr3cyclex  30784  vdn0conngrumgrv2  30797  eupthi  30804  eucrctshift  30844  frcond1  30867  frcond4  30871  frgr3v  30876  3vfriswmgr  30879  1to2vfriswmgr  30880  1to3vfriswmgr  30881  2pthfrgr  30885  4cycl2v2nb  30890  n4cyclfrgr  30892  frgrnbnb  30894  frgrwopreglem4a  30911  clwlknon2num  30969  numclwwlkqhash  30976  frgrreg  30995  frgrregord013  30996  ex-ceil  31049  grpoidinvlem3  31108  nmlno0lem  31395  blocni  31407  pythi  31452  normpythi  31744  shmodsi  31991  pjchi  32034  chlubii  32074  osumi  32244  nmlnop0iALT  32597  cnlnssadj  32682  nmopcoi  32697  mdbr3  32899  mdbr4  32900  ssmd1  32913  dmdsl3  32917  mdexchi  32937  atssma  32980  atoml2i  32985  chirredlem3  32994  mdsymlem1  33005  dmdbr6ati  33025  dmdbr7ati  33026  cdjreui  33034  cdj3lem2b  33039  addltmulALT  33048  difuncomp  33148  iundifdif  33157  imadifxp  33195  fresf1o  33225  2ndimaxp  33240  acunirnmpt2  33254  suppiniseg  33279  fressupp  33281  fdifsuppconst  33282  ressupprn  33283  disjdsct  33296  1stpreimas  33299  preiman0  33303  resf1o  33322  xrge0addge  33350  xlt2addrd  33351  fz2ssnn0  33377  f1ocnt  33392  elq2  33403  nexple  33424  gsummpt2d  33610  gsumfs2d  33622  gsumwun  33637  psgnfzto1stlem  33661  fzto1st  33664  psgnfzto1st  33666  cycpmco2f1  33685  cycpmco2rn  33686  cycpmco2lem7  33693  elrgspn  33807  elrgspnsubrunlem2  33809  elrlocbasi  33828  ricnzr1  33849  sdrginvcl  33862  rsp2idlid  33931  nsgqusf1olem2  33965  elrspunidl  33978  ssmxidl  33999  lbsdiflsp0  34258  fldextfld1  34279  fldextfld2  34280  constrconj  34377  constrllcllem  34384  constrlccllem  34385  constrcccllem  34386  submat1n  34437  submatres  34438  locfinreflem  34472  ldlfcntref  34486  zarclsun  34502  zarclsiin  34503  zarclsint  34504  zarcmplem  34513  mndpluscn  34558  pnfneige0  34583  pl1cn  34587  gsumesum  34691  esumcst  34695  esumrnmpt2  34700  esumcvgre  34723  esum2d  34725  pwsiga  34762  ldsysgenld  34793  measxun2  34843  volmeas  34864  ddemeas  34869  aean  34877  mbfmfun  34886  1stmbfm  34892  2ndmbfm  34893  omssubadd  34932  carsgclctunlem1  34949  sibfof  34972  eulerpartlemmf  35007  probun  35051  dstfrvclim1  35110  coinfliprv  35115  ballotlem2  35121  ballotlemic  35139  ballotlem1c  35140  signstres  35204  bnj529  35372  bnj1379  35460  bnj1424  35468  bnj1436  35469  bnj607  35546  bnj908  35561  bnj1097  35611  bnj1118  35614  bnj1128  35620  bnj1145  35623  bnj1154  35629  bnj1174  35633  bnj1189  35639  bnj1417  35671  soinfdom  35717  axprALT2  35734  rankfo  35735  acnum  35755  weexenwe  35756  tz9.1regs  35802  axsepg2  35808  axsepg4  35811  kardcard2b  35833  cusgr3cyclex  35911  cvmliftlem10  36059  satfv1  36128  fmlasuc0  36149  satffunlem2lem1  36169  mrsub0  36281  mrsubccat  36283  mrsubcn  36284  bcprod  36503  socnv  36529  dfon2lem3  36547  dfon2lem7  36551  dfon2lem8  36552  rdgprc0  36555  fvsingle  36682  unisnif  36687  funpartlem  36706  ss-ax8  37014  trer  37104  clsun  37116  opnregcld  37118  cldregopn  37119  df3nandALT1  37187  lukshef-ax2  37203  nandsym1  37210  weiunfr  37255  dfttc4lem2  37317  knoppndvlem9  37386  bj-mt2bi  37437  bj-gl4  37465  bj-babygodel  37473  bj-babylob  37474  bj-ssbid2ALT  37562  bj-nfext  37616  bj-1upln0  37922  bj-snex  37948  eleq2w2ALT  37962  bj-brrelex12ALT  37982  bj-restsnid  38008  bj-snmooreb  38035  bj-opelrelex  38065  bj-inftyexpitaudisj  38126  bj-inftyexpidisj  38131  bj-elccinfty  38135  finorwe  38305  ctbssinf  38329  fvineqsnf1  38333  pibt2  38340  wl-ifpimpr  38389  wl-ifp4impr  38390  wl-1xor  38405  wl-1mintru1  38411  lindsadd  38536  poimirlem9  38547  poimirlem13  38551  poimirlem14  38552  poimirlem25  38563  poimirlem26  38564  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  mbfresfi  38584  ftc1cnnc  38610  dvasin  38622  fnopabco  38657  frinfm  38669  caushft  38695  bndss  38720  notornotel1  39027  tsbi2  39066  rabeq12f  39089  relcnveq3  39259  relcnveq2  39261  cnvref4  39282  ralrnmo  39293  raldmqsmo  39295  disjressuc2  39343  cnvcosseq  39459  symrelcoss3  39487  dfrefrels2  39525  dfrefrel2  39527  dfcnvrefrels2  39540  dfcnvrefrel2  39542  dfsymrels2  39557  elrelscnveq3  39559  dfsymrel2  39565  symrefref2  39579  dftrrels2  39591  dftrrel2  39593  n0elim  39667  disjimeceqim  39736  membpartlem19  39846  axc11n-16  39995  glbconN  40434  paddssat  40871  pclunN  40955  paddunN  40984  poldmj1N  40985  ltrnnid  41193  dibglbN  42223  mndmolinv  43145  primrootsunit1  43147  primrootscoprmpow  43149  primrootscoprbij  43152  aks6d1c2lem4  43177  aks6d1c2  43180  aks6d1c5lem3  43187  deg1gprod  43190  sticksstones3  43198  sticksstones11  43206  sticksstones12a  43207  sticksstones12  43208  sticksstones13  43209  aks6d1c6isolem1  43224  aks6d1c6lem5  43227  grpods  43244  unitscyglem2  43246  unitscyglem3  43247  unitscyglem4  43248  aks5lem7  43250  exbiii  43262  sn-0ne2  43457  sn-0lt1  43539  istopclsd  43710  pellex  43841  monotoddzzfi  43948  jm2.23  44002  expdioph  44029  wopprc  44036  kelac1  44064  dfac21  44067  lsmfgcl  44075  pwssplit4  44090  isnumbasgrp  44108  dgraalem  44146  ordnexbtwnsuc  44268  cantnfresb  44325  dflim5  44330  rp-tfslim  44354  ifpbi1  44477  rp-fakeanorass  44513  rp-isfinite5  44517  iscard4  44533  minregex  44534  pr2cv  44548  superficl  44567  ssuncl  44570  sssymdifcl  44572  relintab  44583  cotrintab  44613  clcnvlem  44622  cnvtrrel  44669  brfvrcld2  44691  relexpxpmin  44716  relexpaddss  44717  unhe1  44784  frege55lem1b  44894  frege58bid  44901  frege92  44954  uneqsn  45024  ntrk2imkb  45036  neik0pk1imk0  45046  gneispace  45133  k0004lem2  45147  k0004val0  45153  ismnushort  45284  pm10.12  45341  pm11.61  45376  sbiota1  45417  bi1imp  45464  bi2imp  45465  bi3impb  45466  bi3impa  45467  bi13impib  45469  bi123impib  45470  bi13impia  45471  bi123impia  45472  bi13imp23  45474  bi13imp2  45475  bi12imp3  45476  tratrb  45518  dfvd1imp  45557  dfvd2imp  45585  e1bi  45611  e2bi  45614  e3bi  45719  3ornot23VD  45828  3impexpbicomVD  45838  3impexpbicomiVD  45839  tratrbVD  45842  ssralv2VD  45847  equncomiVD  45850  truniALTVD  45859  ee33VD  45860  onfrALTlem3VD  45868  onfrALTlem2VD  45870  onfrALTlem1VD  45871  onfrALTVD  45872  relopabVD  45882  2uasbanhVD  45892  vk15.4jVD  45895  unisnALT  45907  chordthmALT  45914  iunconnlem2  45916  wfaxpow  45986  wfaxun  45988  hfstructfun  46025  fnchoice  46045  uzwo4  46069  inabs3  46072  rexanuz3  46110  disjrnmpt2  46202  disjinfi  46206  iunmapsn  46229  ssfiunibd  46324  iuneqfzuzlem  46345  iuneqfzuz  46346  xrge0ge0  46358  xrssre  46359  infrpge  46362  allbutfi  46403  supxrunb3  46409  eluzelz2  46412  uz0  46421  allbutfiinf  46429  infxrunb3rnmpt  46437  uzublem  46439  uzub  46440  uzid3  46444  infxrlesupxr  46445  infrpgernmpt  46474  supminfxrrnmpt  46480  rexanuz2nf  46501  eliocre  46520  lbioc  46524  ioonct  46548  uzinico  46570  fsumiunss  46586  fmuldfeq  46594  mccl  46609  climsuse  46619  islptre  46630  lptioo2  46642  lptioo1  46643  islpcn  46648  fnlimfvre  46683  climbddf  46696  limsupubuzlem  46721  limsupmnfuzlem  46735  limsupequzmptlem  46737  limsupre3uzlem  46744  xlimcl  46831  cnrefiisplem  46838  xlimliminflimsup  46871  icccncfext  46896  cncfiooicclem1  46902  cncfiooicc  46903  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem1  46955  dvnprodlem3  46957  volioc  46981  itgioocnicc  46986  stoweidlem28  47037  stoweidlem57  47066  wallispilem3  47076  wallispilem4  47077  wallispi  47079  wallispi2lem1  47080  wallispi2  47082  stirlinglem12  47094  fourierdlem42  47158  fourierdlem48  47163  fourierdlem50  47165  fourierdlem52  47167  fourierdlem71  47186  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem80  47195  fourierdlem93  47208  fourierdlem101  47216  fourierdlem103  47218  fourierdlem104  47219  fourierswlem  47239  fouriersw  47240  etransclem26  47269  etransclem37  47280  rrxsnicc  47309  saluncl  47326  intsaluni  47338  intsal  47339  salgencl  47341  salexct  47343  sssalgen  47344  salgenuni  47346  issalgend  47347  salgencntex  47352  subsaliuncllem  47366  subsaliuncl  47367  sge00  47385  sge0sn  47388  sge0cl  47390  sge0f1o  47391  sge0pnffigt  47405  sge0resplit  47415  sge0split  47418  sge0iunmptlemre  47424  sge0xaddlem2  47443  iundjiun  47469  meadjun  47471  meassle  47472  meadjiunlem  47474  meaiunlelem  47477  volmea  47483  caragenunidm  47517  omeunle  47525  omeiunltfirp  47528  caratheodorylem1  47535  caratheodory  47537  icoresmbl  47552  volicorescl  47562  ovncvrrp  47573  ovnsubaddlem2  47580  hoidmv1le  47603  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem5  47608  hoidmvle  47609  ovnhoilem2  47611  hspdifhsp  47625  hoiqssbllem3  47633  hspmbllem2  47636  ovolval4lem1  47658  ovnovollem3  47667  vonioolem1  47689  pimdecfgtioo  47726  pimincfltioo  47727  mbfresmf  47748  smfaddlem1  47772  smflimlem1  47780  smflimlem2  47781  smflimlem3  47782  smflim  47786  smfresal  47797  smfrec  47798  smfmullem4  47803  smfdiv  47806  smfpimbor1lem2  47808  smflimmpt  47819  smfsuplem1  47820  smfinflem  47826  smflimsuplem3  47831  smflimsuplem5  47833  smflimsuplem6  47834  smflimsuplem7  47835  smflimsupmpt  47838  smfliminflem  47839  smfliminfmpt  47841  simpcntrab  47879  quantgodelALT  47884  chnerlem1  47891  chnerlem2  47892  cos5teq  47925  lambert0  47936  lamberte  47937  aifftbifffaibif  47990  aifftbifffaibifff  47991  abciffcbatnabciffncba  47998  abciffcbatnabciffncbai  47999  nabctnabc  48000  confun4  48011  confun5  48012  plcofph  48013  pldofph  48014  plvcofph  48015  plvcofphax  48016  plvofpos  48017  dandysum2p2e4  48067  fresfo  48117  fcores  48136  3f1oss1  48144  3f1oss2  48145  funfocofob  48147  aiotaint  48160  dfaiota3  48161  ndmaovrcl  48273  tz6.12-afv2  48309  fvmptrabdm  48362  difmodm1lt  48434  uniimafveqt  48462  uniimaelsetpreimafv  48477  iccpartiun  48515  iccpartdisj  48518  ich2exprop  48552  ichnreuop  48553  prpair  48582  fmtnorec2lem  48626  dfodd5  48757  stgoldbwt  48873  sbgoldbb  48879  nnsum3primesle9  48891  nnsum4primeseven  48897  clnbgrcl  48918  clnbgrnvtx0  48924  clnbgredg  48937  grimuhgr  48984  isuspgrim0  48991  isuspgrimlem  48992  gricushgr  49014  grtriclwlk3  49042  isubgr3stgrlem1  49063  isubgr3stgrlem7  49069  uspgrlimlem2  49086  uspgrlimlem4  49088  grlimprclnbgr  49093  gpgusgralem  49153  gpg5order  49157  gpg5nbgrvtx03star  49177  gpg5nbgr3star  49178  gpgvtxdg3  49179  gpg5gricstgr3  49187  pgnbgreunbgrlem3  49215  pgnbgreunbgrlem6  49221  pgnbgreunbgr  49222  pgn4cyclex  49223  lmod0rng  49325  lidldomnnring  49332  ringcinvALTV  49406  altgsumbcALT  49464  ply1sclrmsm  49495  linccl  49525  lincvalsng  49527  lincvalpr  49529  lincdifsn  49535  linc1  49536  lincsum  49540  lincscm  49541  lindslinindsimp2lem5  49573  lincresunit3lem2  49591  2sphere  49860  resinsnALT  49980  tposideq  49995  clduni  50008  neircl  50012  funcrcl2  50186  funcrcl3  50187  funcf2lem2  50189  uprcl2  50296  uprcl3  50297  swapf2fval  50372  swapf1val  50374  fucofvalne  50432  thincn0eu  50538  isinito3  50607  mndtcobeq  50690  alsralrex  50907