Theorem impbid 215

Description: Deduce an equivalence from two implications. Deduction associated with impbi 211 and impbii 212. (Contributed by NM, 24-Jan-1993.) Prove it from impbid21d 214. (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	1, 2	impbid21d 214	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 53	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:  bicom1  224  impbid1  228  impcon4bid  230  pm5.74  273  imbi1d  344  pm5.501  369  anbiimOLD  654  impbida  813  dedlem0b  1060  dedlema  1061  dedlemb  1062  albi  1851  alexbii  1866  equequ1  2058  equequ2  2059  spsbbi  2110  elequ1  2152  elequ2  2160  sbequ12  2286  sbft  2303  cbv2w  2366  exsb  2388  dral1v  2398  cbv2  2432  cbv2h  2435  ax12b  2453  dral1  2468  dral1ALT  2469  eupickb  2660  eupickbi  2661  2eu2  2677  ralbi  3117  rexbi  3118  ralbida  3273  ceqsalt  3483  rspcebdv  3570  rspceb2dv  3580  ceqex  3606  elabgtOLD  3627  mob2  3673  reu6  3684  sbcg  3811  2reu2  3846  csbiebt  3876  dfss2  3917  reupick  4275  reupick2  4277  uneqdifeq  4448  prnebg  4816  preqsnd  4819  prel12g  4824  iuneqconst  4963  disjeq2  5074  disjeq1  5077  disjss3  5102  reusv2lem2  5364  reusv2lem3  5365  alxfr  5372  ralxfrd  5373  ralxfrd2  5377  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  snopeqop  5483  euotd  5490  poeq2  5567  sotric  5593  sotrieq  5594  freq2  5623  seeq1  5625  seeq2  5626  iss  6033  tz7.7  6385  ordtri1  6393  ordelinel  6463  funeq  6555  funssres  6580  f0dom0  6762  fnbrfvb  6931  ssimaex  6966  fsneq  7030  fvimacnv  7048  elpreima  7053  feldmfvelcdm  7082  eldmrexrnb  7088  fsn  7132  fnsnbg  7165  fnsnbOLD  7167  fmptsng  7169  fmptsnd  7170  fprb  7195  tpres  7203  fconst2g  7205  fconst5  7208  elunirn  7251  f1ocnvfvb  7283  f1prex  7288  foeqcnvco  7304  f1eqcocnv  7305  fliftfun  7316  soisores  7331  isofr  7346  isose  7347  isopo  7350  isoso  7352  f1oiso2  7356  eusvobj2  7408  oprabidw  7447  oprabid  7448  f1opw2  7672  oneqmin  7805  ordelsuc  7822  ordsucelsuc  7824  ordunisuc2  7846  limsuc  7851  fndmexb  7909  resf1ext2b  7938  f1ovv  7961  mptcnfimad  7989  op1steq  8036  opreuopreu  8037  funeldmdif  8050  fvn0elsuppb  8184  extmptsuppeq  8191  rntpos  8242  smoiso2  8363  seqomlem2  8447  oaord  8541  oawordex  8551  oaordex  8552  omord2  8561  om00  8569  oeord  8583  nnaord  8614  nnmord  8627  nnawordex  8632  nnaordex  8633  nnaordex2  8634  eldifsucnn  8659  erexb  8729  swoord1  8736  swoord2  8737  ecelqsdmb  8793  iiner  8796  eceqoveq  8829  mapsnd  8900  ralxpmap  8910  omxpenlem  9083  domtriord  9128  mapxpen  9148  mapunen  9151  ssenen  9156  enfi  9188  nneneq  9207  nndomog  9214  onomeneq  9215  en1eqsnbi  9253  fodomfib  9305  f1opwfi  9330  fsuppunbi  9366  elfiun  9407  suplub2  9438  ordiso2  9494  ordiso  9495  oieu  9518  brwdom2  9552  brwdom3  9561  cantnflem1  9675  ttrclselem2  9712  elhf2  9882  cardidm  9989  carddom2  10007  pm54.43  10031  acnen  10081  acnen2  10083  alephord  10103  alephinit  10123  dfac5  10156  infdif2  10236  fictb  10271  coflim  10288  fincssdom  10350  fin23lem25  10351  isf32lem9  10388  isf34lem4  10404  fin1a2lem11  10437  axdc3lem2  10478  ficard  10598  fpwwe2lem11  10675  fpwwe2  10677  indpi  10941  nqereq  10969  1idpr  11063  ltapr  11079  leltne  11348  ltlen  11360  ltadd2  11363  addlsub  11679  addid0  11682  ltord1  11789  mul0or  11903  ldiv  12098  ltmul1  12114  mulge0b  12134  lt2msq  12149  nnsub  12329  nn0sub  12603  zrevaddcl  12688  zltp1le  12693  zdiv  12716  nneo  12730  zeo2  12733  zmax  13019  zbtwnre  13020  qrevaddcl  13046  xrlttri  13215  xrleltne  13221  xralrple  13282  xltneg  13294  xleadd1  13332  xlemul1  13367  supxrunb1  13396  supxrunb2  13397  ioo0  13448  iccid  13468  ico0  13469  ioc0  13470  icc0  13471  difreicc  13562  iccsplit  13563  zltaddlt1le  13583  0fz1  13623  uzsplit  13676  fzm1  13687  fzrevral  13692  ssfzo12bi  13842  elfznelfzob  13855  flge  13891  modid2  13984  modmuladd  14002  ssnn0fi  14074  seqf1olem1  14130  hashen  14436  hashdom  14468  hash2exprb  14561  pr2pwpr  14569  hashtpg  14575  hash3tpexb  14584  len0nnbi  14641  ccats1pfxeqbi  14836  reuccatpfxs1  14841  repsdf2  14874  scshwfzeqfzo  14922  relexpindlem  15161  shftlem  15166  shftuz  15167  abslt  15427  absle  15428  rexico  15466  cau3lem  15467  reusq0  15577  rlim2lt  15609  rlim3  15610  o1lo1  15649  rlimdm  15663  climshft  15688  o1dif  15742  isercolllem2  15778  isercoll  15780  zsum  15829  fsum  15831  fsum00  15910  incexclem  15950  zprod  16049  fprod  16053  dvdsval2  16370  moddvds  16378  negdvdsb  16387  dvdsnegb  16388  dvdscmulr  16399  dvdsmulcr  16400  dvdssub2  16416  dvdsaddre2b  16422  fzo0dvdseq  16438  mod2eq1n2dvds  16462  ltoddhalfle  16476  sumodd  16503  bitsf1ocnv  16559  sadcaddlem  16572  bitsuz  16589  dvdsgcdb  16660  gcdzeq  16667  dvdssqlem  16681  lcmeq0  16715  lcmdvdsb  16728  lcmfeq0b  16745  lcmf  16748  lcmfdvdsb  16758  coprmgcdb  16764  cncongr  16784  isprm2lem  16796  dvdsprime  16802  dvdsprm  16819  isprm7  16824  coprm  16827  euclemma  16829  rpexp  16838  prmdvdsncoprmbd  16843  prmdiveq  16902  hashgcdlem  16904  odzdvds  16912  pythagtrip  16951  pc2dvds  16996  pcprmpw2  16999  pcprmpw  17000  vdwapun  17091  ramtcl2  17128  firest  17542  mrieqv2d  17752  isacs2  17766  isssc  17934  setciso  18205  posasymb  18432  pleval2  18448  pltval3  18450  lublecllem  18471  joinle  18497  meetle  18511  latdisd  18610  lubun  18628  clatleglb  18631  letsr  18706  intopsn  18771  gsumval2a  18813  frmdss2  18998  isgrpid2  19126  isgrpinv  19143  f1ghm0to0  19398  symg1bas  19544  oddvdsnn0  19697  oddvds  19700  odeq  19703  odeq1  19713  gexdvds  19737  pgpfi  19758  pgpssslw  19767  fislw  19778  sylow3lem2  19781  lsmelvalm  19804  lsmlub  19817  lsmss1b  19819  lsmss2b  19821  efgs1b  19889  cyggenod  20037  cyggexb  20052  dprdfeq0  20177  ablsimpgfind  20265  ringinvnz1ne0  20470  ringinvnzdiv  20471  unitmulclb  20550  dvreq1  20580  isnzr2  20707  0ringnnzr  20715  0ring01eqbi2  20722  0ring01eqbi  20723  rngciso  20829  ringciso  20863  rrgeq0  20891  domneq0  20899  isabvd  21008  issrngd  21051  lssats2  21214  lspsneq0  21226  lsmelval2  21299  lvecvs0or  21325  lspsneq  21339  lspsneu  21340  lidl1el  21444  rspprop  21463  lidldvgen  21597  pzriprnglem10  21735  pzriprnglem11  21736  znunit  21808  psgndif  21847  ipeq0  21883  ocvsscon  21920  pjdm2  21956  obselocv  21973  islinds4  22080  psdmul  22426  ply1coe1eq  22557  cply1coe0bi  22559  mat1dimelbas  22725  matunitlindf  22935  cramer  22948  toponcomb  23186  tgss3  23243  clsval2  23307  isopn3  23323  elcls3  23340  opncldf1  23341  neiint  23361  neips  23370  opnneissb  23371  opnssneib  23372  opnnei  23377  tpnei  23378  opnneiid  23383  restcld  23429  restopnb  23432  tgcn  23509  tgcnp  23510  subbascn  23511  iscnp4  23520  cnpnei  23521  cncls2  23530  cncls  23531  cnntr  23532  lmss  23555  hausnei2  23610  lpcls  23621  ordtt1  23636  cmpsub  23657  tgcmp  23658  1stcelcls  23719  locfincmp  23784  kgencn2  23815  ptpjpre1  23829  upxp  23881  txcn  23884  txlm  23906  tgqtop  23970  kqfvima  23988  isr0  23995  regr1lem2  23998  hmeoopn  24024  hmeocld  24025  ptuncnv  24065  fbunfip  24127  fgss2  24132  ufilb  24164  ufprim  24167  trufil  24168  cfinufil  24186  ufildr  24189  elfm2  24206  elfm3  24208  rnelfm  24211  fmfnfmlem4  24215  fmco  24219  flimtopon  24228  flimopn  24233  fbflim2  24235  flimrest  24241  flffbas  24253  cnpflf  24259  fclstopon  24270  fclsnei  24277  fclsbas  24279  fclsfnflim  24285  fclscmp  24288  ufilcmp  24290  isfcf  24292  fcfnei  24293  cnpfcf  24299  alexsubb  24304  alexsubALT  24309  cldsubg  24369  tgphaus  24375  tgpt0  24377  tsmsgsum  24397  tsmsres  24402  xbln0  24672  blssexps  24684  blssex  24685  isxms2  24706  prdsbl  24749  neibl  24759  metss  24766  met2ndc  24781  metrest  24782  metcnp3  24798  tngngp3  24914  nmoeq0  24994  xrsxmet  25068  reconn  25087  iccpnfcnv  25204  fgcfil  25531  iscau4  25539  cfilres  25556  iunmbl2  25817  ismbf3d  25914  mbfaddlem  25920  i1faddlem  25953  i1fmullem  25954  ellimc3  26138  dvfsumlem2  26286  tdeglem4  26317  deg1nn0clb  26347  deg1lt0  26348  dvdsq1p  26420  plypf1  26470  0dgrb  26504  plymul0or  26540  taylthlem2  26642  ulmshft  26658  ulmcaulem  26662  ulmcau  26663  cosord  26800  eff1olem  26817  lognegb  26859  eflogeq  26871  logdivlt  26890  efopn  26927  cxpeq0  26947  cxpeq  27026  angpieqvd  27100  dcubic  27115  asinsinb  27166  acoscosb  27167  atantanb  27193  rlimcnp  27234  isppw  27382  isppw2  27383  vmappw  27384  isnsqf  27403  ppieq0  27444  fsumdvdsdiag  27452  dvdsppwf1o  27454  fsumfldivdiag  27458  chpeq0  27476  chteq0  27477  dchrptlem1  27532  lgsdir2lem4  27596  lgsne0  27603  lgsqr  27619  lgsdchrval  27622  gausslemma2dlem1a  27633  lgsquadlem1  27648  m1lgs  27656  2sqreultblem  27716  2sqreunnltblem  27719  nodenselem8  27959  ltlesnd  28043  oldlim  28184  ltslpss  28205  leadds1  28286  ltnegs  28342  negleft  28355  negright  28356  muls0ord  28482  abslts  28546  onlts  28564  n0subs  28660  n0ltsp1le  28662  z12sge0  28780  iscgrglt  28888  brbtwn  29388  brcgr  29389  brbtwn2  29394  axcontlem7  29459  uhgr0vb  29561  edglnl  29632  ausgrusgrb  29657  ushgredgedg  29721  ushgredgedgloop  29723  usgr0vb  29729  usgr1v  29748  nbupgr  29836  nbumgrvtx  29838  nbuhgr2vtx1edgb  29844  edgusgrnbfin  29865  nb3grprlem1  29872  uvtxnbvtxm1  29898  cusgrfilem2  29948  uhgr0edg0rgrb  30066  cusgrm1rusgr  30074  spthonepeq  30249  usgr2pth  30261  wlkiswwlks  30376  wlkiswwlkupgr  30378  wlklnwwlkn  30384  wlklnwwlknupgr  30386  wwlksnextbi  30394  wwlksnredwwlkn0  30396  wwlksnextwrd  30397  wwlksnextprop  30412  usgrwwlks2on  30458  umgrwwlks2on  30459  elwspths2on  30462  elwspths2onw  30463  usgr2wspthons3  30467  elwwlks2  30469  elwspths2spth  30470  clwlkclwwlklem3  30503  loopclwwlkn1b  30544  clwwlknon1sn  30602  clwwlknonwwlknonb  30608  loop1cycl  30655  umgr3v3e3cycl  30696  eupth2lem3lem4  30743  frgr0v  30774  frgr3vlem2  30786  2clwwlk2clwwlk  30862  wlkl0  30879  grpoinvf  31045  nvmul0or  31163  nvz  31182  diporthcom  31229  ubthlem3  31385  hvmul0or  31538  his6  31612  hial0  31615  hial02  31616  orthcom  31621  normgt0  31640  ocin  31809  occon3  31810  shsel3  31828  shlub  31927  chssoc  32009  h1de2bi  32067  spansncol  32081  elspansn4  32086  spansnss2  32088  sumspansn  32162  lnopcnbd  32549  lnfncnbd  32570  riesz1  32578  elpjrn  32703  cvcon3  32797  dmdmd  32813  dmdbr3  32818  dmdbr4  32819  dmdbr5  32821  mdslmd1i  32842  atcveq0  32861  chcv1  32868  atssma  32891  atcv0eq  32892  atcv1  32893  disjeq1f  33078  br8d  33113  fpwrelmap  33236  xaddeq0  33256  eliccelico  33280  elicoelioo  33281  indf1ofs  33344  isarchiofld  33671  unitdivcld  34444  xrge0iifcnv  34476  lmxrge0  34495  eulerpartlemgh  34922  dstfrvunirn  35019  fnfvintima  35624  fnrelpredd  35629  rankfilimb  35643  fineqvnttrclse  35693  cusgracyclt3v  35818  cvmliftmolem2  35944  cvmlift2lem12  35976  satfvsucsuc  36027  satfdm  36031  fmlasuc  36048  satffunlem1lem2  36065  satffunlem2lem2  36068  mthmb  36243  climuzcnv  36333  br8  36418  br6  36419  br4  36420  funbreq  36432  axextbdist  36460  dfrdg4  36613  cgrcom  36653  cgrcoml  36659  cgrdegen  36667  btwncom  36677  brsegle  36771  brsegle2  36772  colinbtwnle  36781  btwnoutside  36788  broutsideof3  36789  outsidele  36795  lineunray  36810  lineelsb2  36811  ltnmul  36863  ltnadd  36865  elicc3  37003  nn0prpwlem  37008  opnbnd  37011  cldbnd  37012  opnregcld  37016  cldregopn  37017  fnessref  37043  refssfne  37044  neibastop2  37047  fnemeet2  37053  fnejoin2  37055  fgmin  37056  ontgval  37117  ordtop  37122  ordcmp  37133  nndivsub  37143  bj-cbval  37443  bj-cbvex  37444  bj-19.21t  37561  bj-19.23t  37562  bj-19.42t  37565  bj-sbft  37578  bj-nnf-cbval  37580  bj-cbv2hv  37607  bj-equsal1t  37632  bj-19.21t0  37640  bj-ceqsalt0  37694  bj-ceqsalt1  37695  bj-xpnzexb  37772  bj-axreprepsep  37887  cgsex2gd  37954  bj-idreseq  37979  bj-imdiridlem  38002  bj-finsumval0  38102  bj-fvimacnv0  38103  bj-isrvec2  38117  bj-bary1  38129  dfgcd3  38141  isbasisrelowllem1  38174  isbasisrelowllem2  38175  finxpsuclem  38216  wl-lem-exsb  38394  wl-mo3t  38404  poimirlem6  38440  poimirlem7  38441  poimirlem16  38450  poimirlem19  38453  poimirlem22  38456  poimirlem23  38457  poimirlem24  38458  cnambfre  38482  itg2addnc  38488  brabg2  38532  istotbnd3  38586  sstotbnd2  38589  sstotbnd  38590  sstotbnd3  38591  ssbnd  38603  ismtybnd  38622  reheibor  38654  grpoeqdivid  38696  grpokerinj  38708  rngosn3  38739  rngoueqz  38755  1idl  38841  0rngo  38842  divrngidl  38843  igenval2  38881  ispridlc  38885  isdmn3  38889  relcnveq3  39140  iss2  39157  elrelscnveq3  39440  funALTVeq  39598  disjeq  39647  prtlem10  39803  prter2  39819  dral1-o  39842  lshpinN  39927  lsatcveq0  39970  lsatcv0eq  39985  lsatcv1  39986  islshpcv  39991  lkr0f  40032  lkrshp4  40046  lshpkrlem1  40048  lshpset2N  40057  lfl1dim  40059  lfl1dim2N  40060  lub0N  40127  glb0N  40131  oplecon3b  40138  cmtcomN  40187  cmtbr3N  40192  cmtbr4N  40193  cvrnbtwn2  40213  cvrnbtwn3  40214  cvrcon3b  40215  cvrnbtwn4  40217  cvrcmp  40221  atcvreq0  40252  atnle  40255  atlatle  40258  cvlexchb1  40268  cvlcvr1  40277  hlrelat2  40341  exatleN  40342  cvrval3  40351  cvrval4N  40352  cvrexch  40358  atcvr0eq  40364  lnnat  40365  atcvrj0  40366  atcvrj2b  40370  atltcvr  40373  atbtwn  40384  ps-1  40415  3at  40428  islln2a  40455  llncmp  40460  islpln2a  40486  lplncmp  40500  islvol2aN  40530  4at  40551  lvolcmp  40555  pmaple  40699  lncmp  40721  paddss  40783  llnexchb2lem  40806  2polcon4bN  40856  ispsubcl2N  40885  lhpat3  40984  lautcvr  41030  ltrnid  41073  trlval2  41101  trlatn0  41110  ltrnideq  41113  trlnidatb  41115  cdlemeg49lebilem  41477  trlord  41507  cdlemg1a  41508  cdlemg1cex  41526  tendoid0  41763  dva1dim  41923  cdlemm10N  42056  diarnN  42067  cdlemn  42150  dihlspsnssN  42270  dihatexv  42276  dochkrshp  42324  dochkrshp4  42327  djhlsmcl  42352  lcfl6  42438  lcfl8  42440  lcfrvalsnN  42479  lcfrlem9  42488  mapdval2N  42568  mapdordlem2  42575  mapd1o  42586  mapd0  42603  mapdheq2biN  42668  nnproddivdvdsd  42931  primrootspoweq0  43037  aks6d1c1p1  43038  aks6d1c5lem1  43067  sticksstones11  43087  sticksstones22  43099  grpods  43125  unitscyglem2  43127  eqresfnbd  43167  expeq1d  43264  expeqidd  43265  dvdsexpnn  43273  zdivgd  43277  sn-remul0ord  43348  mulgt0b1d  43425  frlmfzowrdb  43457  frlmsnic  43487  evlselvlem  43499  prjspreln0  43520  elrfi  43604  diophrw  43669  eldioph2b  43673  diophin  43682  rexrabdioph  43700  rmxycomplete  43823  coprmdvdsb  43891  jm2.19  43899  jm2.26  43908  jm2.27  43914  limsuc2  43947  dgraa0p  44055  rngunsnply  44075  fiuneneq  44098  unielss  44124  oaabsb  44200  nnoeomeqom  44218  cantnfresb  44230  tfsconcatrn  44248  tfsconcat0b  44252  tfsconcatrev  44254  oadif1lem  44285  oadif1  44286  fzunt  44360  fzuntd  44361  fzunt1d  44362  fzuntgd  44363  pwelg  44465  nzss  45206  dvconstbi  45223  expgrowth  45224  bcc0  45229  axc11next  45295  pm14.24  45321  sbiota1  45323  sbcim2g  45426  sineq0ALT  45824  mapss2  46101  fsneqrn  46106  mapssbi  46108  rnmptbd2lem  46142  infnsuprnmpt  46144  rnmptbdlem  46149  xralrple2  46249  infxrunb2  46262  xralrple4  46267  xralrple3  46268  xrralrecnnle  46277  xrralrecnnge  46284  reclt0  46285  supxrunb3  46293  supxrleubrnmpt  46299  xrre4  46304  unb2ltle  46308  rexabslelem  46311  suprleubrnmpt  46315  infxrunb3rnmpt  46321  uzub  46324  supminfrnmpt  46338  iccintsng  46418  sqrlearg  46448  uzinico  46454  preimaiocmnf  46455  limcresiooub  46535  limclr  46548  climeldmeq  46558  limsuppnflem  46603  limsupmnflem  46613  limsupmnfuzlem  46619  limsupre3lem  46625  limsupre3uzlem  46628  liminfreuzlem  46695  dvnmul  46836  dvmptfprodlem  46837  ismbl3  46879  ismbl4  46886  fourierdlem50  47049  fourierdlem89  47088  fourierdlem91  47090  dfsalgen2  47234  sge0repnf  47279  sge0lefi  47291  sge0resplit  47299  sge0fodjrnlem  47309  voliunsge0lem  47365  hspdifhsp  47509  isvonmbl  47531  ovnovollem3  47551  vonvolmbl  47554  pimrecltpos  47601  preimaicomnf  47604  pimrecltneg  47617  issmflem  47620  issmfle  47638  issmfgt  47649  smfaddlem1  47656  issmfge  47663  smfresal  47681  smflimmpt  47703  smfinflem  47710  smflimsuplem7  47719  smflimsupmpt  47722  sigarcol  47757  tmachlem-agreeprod  47830  confun  47892  or2expropbi  47987  fsetsniunop  48002  fcoresf1b  48023  f1cof1b  48030  funfocofob  48031  rexsb  48052  euoreqb  48062  ralbinrald  48075  rlimdmafv  48130  fafv2elrnb  48188  tz6.12c-afv2  48195  dfatbrafv2b  48198  fnbrafv2b  48201  rlimdmafv2  48211  f1oresf1o2  48244  el1fzopredsuc  48279  2ffzoeq  48281  nnmul2b  48284  modlt0b  48322  nndivides2  48337  imasetpreimafvbijlemfo  48370  iccpartiun  48399  ichnfb  48430  ich2exprop  48436  sprsymrelfolem2  48458  paireqne  48476  prprelprb  48482  reupr  48487  nprmmul2  48493  nprmmul3  48494  requad01  48602  requad1  48603  requad2  48604  dfodd6  48618  dfeven4  48619  evensumeven  48688  sbgoldbalt  48762  clnbgrel  48809  dfclnbgr6  48837  dfnbgr6  48838  isubgredg  48847  isuspgrim0  48875  isuspgrim  48877  gricushgr  48898  uhgrimisgrgriclem  48911  clnbgrgrim  48915  grimedg  48916  usgrgrtrirex  48931  uspgrlimlem2  48970  uspgrlim  48973  gpgedgiov  49046  gpgedg2ov  49047  gpgedg2iv  49048  gpgnbgrvtx0  49055  gpgnbgrvtx1  49056  isassintop  49190  uzlidlring  49215  rngcisoALTV  49257  ringcisoALTV  49291  isidom3  49325  domnmsuppn0  49364  lindslininds  49459  snlindsntor  49466  isldepslvec2  49480  affinecomb1  49697  prelrrx2b  49709  rrx2plord2  49717  eenglngeehlnm  49734  rrx2vlinest  49736  line2xlem  49748  line2x  49749  line2y  49750  itsclc0xyqsolb  49765  itsclquadb  49771  mpbiran3d  49790  opnneibid  49902  iscnrm3lem2  49926  fullthinc2  50442  thincciso  50444  alsralrex  50806  alsraln0  50807