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  2288  sbft  2305  cbv2w  2368  exsb  2390  dral1v  2400  cbv2  2434  cbv2h  2437  ax12b  2455  dral1  2470  dral1ALT  2471  eupickb  2662  eupickbi  2663  2eu2  2679  ralbi  3119  rexbi  3120  ralbida  3275  ceqsalt  3486  rspcebdv  3573  rspceb2dv  3583  ceqex  3609  elabgtOLD  3630  mob2  3676  reu6  3687  sbcg  3814  2reu2  3849  csbiebt  3879  dfss2  3920  reupick  4278  reupick2  4280  uneqdifeq  4451  prnebg  4819  preqsnd  4822  prel12g  4827  iuneqconst  4966  disjeq2  5078  disjeq1  5081  disjss3  5106  reusv2lem2  5368  reusv2lem3  5369  alxfr  5376  ralxfrd  5377  ralxfrd2  5381  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  snopeqop  5487  euotd  5494  poeq2  5571  sotric  5597  sotrieq  5598  freq2  5627  seeq1  5629  seeq2  5630  iss  6035  tz7.7  6387  ordtri1  6395  ordelinel  6465  funeq  6557  funssres  6581  f0dom0  6763  fnbrfvb  6932  ssimaex  6967  fsneq  7031  fvimacnv  7049  elpreima  7054  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  7802  ordelsuc  7819  ordsucelsuc  7821  ordunisuc2  7843  limsuc  7848  fndmexb  7906  resf1ext2b  7935  f1ovv  7958  mptcnfimad  7986  op1steq  8033  opreuopreu  8034  funeldmdif  8048  fvn0elsuppb  8182  extmptsuppeq  8189  rntpos  8240  smoiso2  8361  seqomlem2  8443  oaord  8537  oawordex  8547  oaordex  8548  omord2  8557  om00  8565  oeord  8579  nnaord  8610  nnmord  8623  nnawordex  8628  nnaordex  8629  nnaordex2  8630  eldifsucnn  8655  erexb  8725  swoord1  8732  swoord2  8733  ecelqsdmb  8789  iiner  8792  eceqoveq  8825  mapsnd  8896  ralxpmap  8906  omxpenlem  9079  domtriord  9124  mapxpen  9144  mapunen  9147  ssenen  9152  enfi  9184  nneneq  9203  nndomog  9210  onomeneq  9211  en1eqsnbi  9249  fodomfib  9301  f1opwfi  9326  fsuppunbi  9362  elfiun  9403  suplub2  9434  ordiso2  9490  ordiso  9491  oieu  9514  brwdom2  9548  brwdom3  9557  cantnflem1  9671  ttrclselem2  9708  cardidm  9967  carddom2  9985  pm54.43  10009  acnen  10059  acnen2  10061  alephord  10081  alephinit  10101  dfac5  10134  infdif2  10214  fictb  10249  coflim  10266  fincssdom  10328  fin23lem25  10329  isf32lem9  10366  isf34lem4  10382  fin1a2lem11  10415  axdc3lem2  10456  ficard  10574  fpwwe2lem11  10651  fpwwe2  10653  indpi  10917  nqereq  10945  1idpr  11039  ltapr  11055  leltne  11324  ltlen  11336  ltadd2  11339  addlsub  11655  addid0  11658  ltord1  11765  mul0or  11879  ldiv  12074  ltmul1  12090  mulge0b  12110  lt2msq  12125  nnsub  12305  nn0sub  12579  zrevaddcl  12664  zltp1le  12669  zdiv  12692  nneo  12706  zeo2  12709  zmax  12995  zbtwnre  12996  qrevaddcl  13021  xrlttri  13190  xrleltne  13196  xralrple  13257  xltneg  13269  xleadd1  13307  xlemul1  13342  supxrunb1  13371  supxrunb2  13372  ioo0  13423  iccid  13443  ico0  13444  ioc0  13445  icc0  13446  difreicc  13537  iccsplit  13538  zltaddlt1le  13558  0fz1  13598  uzsplit  13651  fzm1  13662  fzrevral  13667  ssfzo12bi  13817  elfznelfzob  13830  flge  13866  modid2  13959  modmuladd  13977  ssnn0fi  14049  seqf1olem1  14105  hashen  14411  hashdom  14443  hash2exprb  14536  pr2pwpr  14544  hashtpg  14550  hash3tpexb  14559  len0nnbi  14616  ccats1pfxeqbi  14811  reuccatpfxs1  14816  repsdf2  14849  scshwfzeqfzo  14897  relexpindlem  15136  shftlem  15141  shftuz  15142  abslt  15402  absle  15403  rexico  15441  cau3lem  15442  reusq0  15552  rlim2lt  15584  rlim3  15585  o1lo1  15624  rlimdm  15638  climshft  15663  o1dif  15717  isercolllem2  15753  isercoll  15755  zsum  15804  fsum  15806  fsum00  15885  incexclem  15925  zprod  16026  fprod  16030  dvdsval2  16347  moddvds  16355  negdvdsb  16364  dvdsnegb  16365  dvdscmulr  16376  dvdsmulcr  16377  dvdssub2  16393  dvdsaddre2b  16399  fzo0dvdseq  16415  mod2eq1n2dvds  16439  ltoddhalfle  16453  sumodd  16480  bitsf1ocnv  16536  sadcaddlem  16549  bitsuz  16566  dvdsgcdb  16637  gcdzeq  16644  dvdssqlem  16658  lcmeq0  16692  lcmdvdsb  16705  lcmfeq0b  16722  lcmf  16725  lcmfdvdsb  16735  coprmgcdb  16741  cncongr  16761  isprm2lem  16773  dvdsprime  16779  dvdsprm  16796  isprm7  16801  coprm  16804  euclemma  16806  rpexp  16815  prmdvdsncoprmbd  16820  prmdiveq  16879  hashgcdlem  16881  odzdvds  16889  pythagtrip  16928  pc2dvds  16973  pcprmpw2  16976  pcprmpw  16977  vdwapun  17068  ramtcl2  17105  firest  17519  mrieqv2d  17729  isacs2  17743  isssc  17911  setciso  18182  posasymb  18409  pleval2  18425  pltval3  18427  lublecllem  18448  joinle  18474  meetle  18488  latdisd  18587  lubun  18605  clatleglb  18608  letsr  18683  intopsn  18748  gsumval2a  18787  frmdss2  18971  isgrpid2  19099  isgrpinv  19116  f1ghm0to0  19371  symg1bas  19517  oddvdsnn0  19670  oddvds  19673  odeq  19676  odeq1  19686  gexdvds  19710  pgpfi  19731  pgpssslw  19740  fislw  19751  sylow3lem2  19754  lsmelvalm  19777  lsmlub  19790  lsmss1b  19792  lsmss2b  19794  efgs1b  19862  cyggenod  20010  cyggexb  20025  dprdfeq0  20150  ablsimpgfind  20238  ringinvnz1ne0  20441  ringinvnzdiv  20442  unitmulclb  20521  dvreq1  20551  isnzr2  20677  0ringnnzr  20685  0ring01eqbi2  20692  0ring01eqbi  20693  rngciso  20799  ringciso  20833  rrgeq0  20861  domneq0  20869  isabvd  20977  issrngd  21020  lssats2  21183  lspsneq0  21195  lsmelval2  21268  lvecvs0or  21294  lspsneq  21308  lspsneu  21309  lidl1el  21413  rspprop  21432  lidldvgen  21564  pzriprnglem10  21702  pzriprnglem11  21703  znunit  21775  psgndif  21814  ipeq0  21850  ocvsscon  21887  pjdm2  21923  obselocv  21940  islinds4  22047  psdmul  22393  ply1coe1eq  22524  cply1coe0bi  22526  mat1dimelbas  22692  matunitlindf  22902  cramer  22915  toponcomb  23153  tgss3  23210  clsval2  23274  isopn3  23290  elcls3  23307  opncldf1  23308  neiint  23328  neips  23337  opnneissb  23338  opnssneib  23339  opnnei  23344  tpnei  23345  opnneiid  23350  restcld  23396  restopnb  23399  tgcn  23476  tgcnp  23477  subbascn  23478  iscnp4  23487  cnpnei  23488  cncls2  23497  cncls  23498  cnntr  23499  lmss  23522  hausnei2  23577  lpcls  23588  ordtt1  23603  cmpsub  23624  tgcmp  23625  1stcelcls  23686  locfincmp  23751  kgencn2  23782  ptpjpre1  23796  upxp  23848  txcn  23851  txlm  23873  tgqtop  23937  kqfvima  23955  isr0  23962  regr1lem2  23965  hmeoopn  23991  hmeocld  23992  ptuncnv  24032  fbunfip  24094  fgss2  24099  ufilb  24131  ufprim  24134  trufil  24135  cfinufil  24153  ufildr  24156  elfm2  24173  elfm3  24175  rnelfm  24178  fmfnfmlem4  24182  fmco  24186  flimtopon  24195  flimopn  24200  fbflim2  24202  flimrest  24208  flffbas  24220  cnpflf  24226  fclstopon  24237  fclsnei  24244  fclsbas  24246  fclsfnflim  24252  fclscmp  24255  ufilcmp  24257  isfcf  24259  fcfnei  24260  cnpfcf  24266  alexsubb  24271  alexsubALT  24276  cldsubg  24336  tgphaus  24342  tgpt0  24344  tsmsgsum  24364  tsmsres  24369  xbln0  24639  blssexps  24651  blssex  24652  isxms2  24673  prdsbl  24716  neibl  24726  metss  24733  met2ndc  24748  metrest  24749  metcnp3  24765  tngngp3  24881  nmoeq0  24961  xrsxmet  25035  reconn  25054  iccpnfcnv  25171  fgcfil  25498  iscau4  25506  cfilres  25523  iunmbl2  25784  ismbf3d  25881  mbfaddlem  25887  i1faddlem  25920  i1fmullem  25921  ellimc3  26106  dvfsumlem2  26254  tdeglem4  26285  deg1nn0clb  26315  deg1lt0  26316  dvdsq1p  26388  plypf1  26437  0dgrb  26471  plymul0or  26507  taylthlem2  26605  ulmshft  26621  ulmcaulem  26625  ulmcau  26626  cosord  26764  eff1olem  26781  lognegb  26823  eflogeq  26835  logdivlt  26854  efopn  26891  cxpeq0  26911  cxpeq  26990  angpieqvd  27064  dcubic  27079  asinsinb  27130  acoscosb  27131  atantanb  27157  rlimcnp  27198  isppw  27346  isppw2  27347  vmappw  27348  isnsqf  27367  ppieq0  27408  fsumdvdsdiag  27416  dvdsppwf1o  27418  fsumfldivdiag  27422  chpeq0  27440  chteq0  27441  dchrptlem1  27496  lgsdir2lem4  27560  lgsne0  27567  lgsqr  27583  lgsdchrval  27586  gausslemma2dlem1a  27597  lgsquadlem1  27612  m1lgs  27620  2sqreultblem  27680  2sqreunnltblem  27683  nodenselem8  27923  ltlesnd  28007  oldlim  28148  ltslpss  28169  leadds1  28250  ltnegs  28306  negleft  28319  negright  28320  muls0ord  28446  abslts  28510  onlts  28528  n0subs  28624  n0ltsp1le  28626  z12sge0  28744  iscgrglt  28852  brbtwn  29340  brcgr  29341  brbtwn2  29346  axcontlem7  29411  uhgr0vb  29513  edglnl  29584  ausgrusgrb  29609  ushgredgedg  29673  ushgredgedgloop  29675  usgr0vb  29681  usgr1v  29700  nbupgr  29788  nbumgrvtx  29790  nbuhgr2vtx1edgb  29796  edgusgrnbfin  29817  nb3grprlem1  29824  uvtxnbvtxm1  29850  cusgrfilem2  29900  uhgr0edg0rgrb  30018  cusgrm1rusgr  30026  spthonepeq  30201  usgr2pth  30213  wlkiswwlks  30328  wlkiswwlkupgr  30330  wlklnwwlkn  30336  wlklnwwlknupgr  30338  wwlksnextbi  30346  wwlksnredwwlkn0  30348  wwlksnextwrd  30349  wwlksnextprop  30364  usgrwwlks2on  30410  umgrwwlks2on  30411  elwspths2on  30414  elwspths2onw  30415  usgr2wspthons3  30419  elwwlks2  30421  elwspths2spth  30422  clwlkclwwlklem3  30455  loopclwwlkn1b  30496  clwwlknon1sn  30554  clwwlknonwwlknonb  30560  loop1cycl  30607  umgr3v3e3cycl  30648  eupth2lem3lem4  30695  frgr0v  30726  frgr3vlem2  30738  2clwwlk2clwwlk  30814  wlkl0  30831  grpoinvf  30997  nvmul0or  31115  nvz  31134  diporthcom  31181  ubthlem3  31337  hvmul0or  31490  his6  31564  hial0  31567  hial02  31568  orthcom  31573  normgt0  31592  ocin  31761  occon3  31762  shsel3  31780  shlub  31879  chssoc  31961  h1de2bi  32019  spansncol  32033  elspansn4  32038  spansnss2  32040  sumspansn  32114  lnopcnbd  32501  lnfncnbd  32522  riesz1  32530  elpjrn  32655  cvcon3  32749  dmdmd  32765  dmdbr3  32770  dmdbr4  32771  dmdbr5  32773  mdslmd1i  32794  atcveq0  32813  chcv1  32820  atssma  32843  atcv0eq  32844  atcv1  32845  disjeq1f  33031  br8d  33066  fpwrelmap  33189  xaddeq0  33209  eliccelico  33233  elicoelioo  33234  indf1ofs  33297  isarchiofld  33624  unitdivcld  34396  xrge0iifcnv  34428  lmxrge0  34447  eulerpartlemgh  34874  dstfrvunirn  34971  fnfvintima  35576  fnrelpredd  35581  rankfilimb  35595  fineqvnttrclse  35635  cusgracyclt3v  35720  cvmliftmolem2  35846  cvmlift2lem12  35878  satfvsucsuc  35929  satfdm  35933  fmlasuc  35950  satffunlem1lem2  35967  satffunlem2lem2  35970  mthmb  36145  climuzcnv  36235  br8  36320  br6  36321  br4  36322  funbreq  36334  axextbdist  36362  dfrdg4  36515  cgrcom  36555  cgrcoml  36561  cgrdegen  36569  btwncom  36579  brsegle  36673  brsegle2  36674  colinbtwnle  36683  btwnoutside  36690  broutsideof3  36691  outsidele  36697  lineunray  36712  lineelsb2  36713  elhf2  36740  ltnmul  36781  ltnadd  36783  elicc3  36921  nn0prpwlem  36926  opnbnd  36929  cldbnd  36930  opnregcld  36934  cldregopn  36935  fnessref  36961  refssfne  36962  neibastop2  36965  fnemeet2  36971  fnejoin2  36973  fgmin  36974  ontgval  37035  ordtop  37040  ordcmp  37051  nndivsub  37061  bj-cbval  37361  bj-cbvex  37362  bj-19.21t  37479  bj-19.23t  37480  bj-19.42t  37483  bj-sbft  37496  bj-nnf-cbval  37498  bj-cbv2hv  37525  bj-equsal1t  37550  bj-19.21t0  37558  bj-ceqsalt0  37612  bj-ceqsalt1  37613  bj-xpnzexb  37690  bj-axreprepsep  37805  cgsex2gd  37874  bj-idreseq  37899  bj-imdiridlem  37922  bj-finsumval0  38022  bj-fvimacnv0  38023  bj-isrvec2  38037  bj-bary1  38049  dfgcd3  38061  isbasisrelowllem1  38094  isbasisrelowllem2  38095  finxpsuclem  38136  wl-lem-exsb  38314  wl-mo3t  38324  poimirlem6  38360  poimirlem7  38361  poimirlem16  38370  poimirlem19  38373  poimirlem22  38376  poimirlem23  38377  poimirlem24  38378  cnambfre  38402  itg2addnc  38408  brabg2  38452  istotbnd3  38506  sstotbnd2  38509  sstotbnd  38510  sstotbnd3  38511  ssbnd  38523  ismtybnd  38542  reheibor  38574  grpoeqdivid  38616  grpokerinj  38628  rngosn3  38659  rngoueqz  38675  1idl  38761  0rngo  38762  divrngidl  38763  igenval2  38801  ispridlc  38805  isdmn3  38809  relcnveq3  39060  iss2  39077  elrelscnveq3  39360  funALTVeq  39518  disjeq  39567  prtlem10  39723  prter2  39739  dral1-o  39762  lshpinN  39847  lsatcveq0  39890  lsatcv0eq  39905  lsatcv1  39906  islshpcv  39911  lkr0f  39952  lkrshp4  39966  lshpkrlem1  39968  lshpset2N  39977  lfl1dim  39979  lfl1dim2N  39980  lub0N  40047  glb0N  40051  oplecon3b  40058  cmtcomN  40107  cmtbr3N  40112  cmtbr4N  40113  cvrnbtwn2  40133  cvrnbtwn3  40134  cvrcon3b  40135  cvrnbtwn4  40137  cvrcmp  40141  atcvreq0  40172  atnle  40175  atlatle  40178  cvlexchb1  40188  cvlcvr1  40197  hlrelat2  40261  exatleN  40262  cvrval3  40271  cvrval4N  40272  cvrexch  40278  atcvr0eq  40284  lnnat  40285  atcvrj0  40286  atcvrj2b  40290  atltcvr  40293  atbtwn  40304  ps-1  40335  3at  40348  islln2a  40375  llncmp  40380  islpln2a  40406  lplncmp  40420  islvol2aN  40450  4at  40471  lvolcmp  40475  pmaple  40619  lncmp  40641  paddss  40703  llnexchb2lem  40726  2polcon4bN  40776  ispsubcl2N  40805  lhpat3  40904  lautcvr  40950  ltrnid  40993  trlval2  41021  trlatn0  41030  ltrnideq  41033  trlnidatb  41035  cdlemeg49lebilem  41397  trlord  41427  cdlemg1a  41428  cdlemg1cex  41446  tendoid0  41683  dva1dim  41843  cdlemm10N  41976  diarnN  41987  cdlemn  42070  dihlspsnssN  42190  dihatexv  42196  dochkrshp  42244  dochkrshp4  42247  djhlsmcl  42272  lcfl6  42358  lcfl8  42360  lcfrvalsnN  42399  lcfrlem9  42408  mapdval2N  42488  mapdordlem2  42495  mapd1o  42506  mapd0  42523  mapdheq2biN  42588  nnproddivdvdsd  42851  primrootspoweq0  42957  aks6d1c1p1  42958  aks6d1c5lem1  42987  sticksstones11  43007  sticksstones22  43019  grpods  43045  unitscyglem2  43047  eqresfnbd  43087  expeq1d  43184  expeqidd  43185  dvdsexpnn  43193  zdivgd  43197  sn-remul0ord  43268  mulgt0b1d  43345  frlmfzowrdb  43377  frlmsnic  43407  evlselvlem  43419  prjspreln0  43440  elrfi  43524  diophrw  43589  eldioph2b  43593  diophin  43602  rexrabdioph  43620  rmxycomplete  43743  coprmdvdsb  43811  jm2.19  43819  jm2.26  43828  jm2.27  43834  limsuc2  43867  dgraa0p  43975  rngunsnply  43995  fiuneneq  44018  unielss  44044  oaabsb  44120  nnoeomeqom  44138  cantnfresb  44150  tfsconcatrn  44168  tfsconcat0b  44172  tfsconcatrev  44174  oadif1lem  44205  oadif1  44206  fzunt  44280  fzuntd  44281  fzunt1d  44282  fzuntgd  44283  pwelg  44385  nzss  45126  dvconstbi  45143  expgrowth  45144  bcc0  45149  axc11next  45215  pm14.24  45241  sbiota1  45243  sbcim2g  45346  sineq0ALT  45744  mapss2  46021  fsneqrn  46026  mapssbi  46028  rnmptbd2lem  46062  infnsuprnmpt  46064  rnmptbdlem  46069  xralrple2  46169  infxrunb2  46182  xralrple4  46187  xralrple3  46188  xrralrecnnle  46197  xrralrecnnge  46204  reclt0  46205  supxrunb3  46213  supxrleubrnmpt  46219  xrre4  46224  unb2ltle  46228  rexabslelem  46231  suprleubrnmpt  46235  infxrunb3rnmpt  46241  uzub  46244  supminfrnmpt  46258  iccintsng  46338  sqrlearg  46368  uzinico  46374  preimaiocmnf  46375  limcresiooub  46455  limclr  46468  climeldmeq  46478  limsuppnflem  46523  limsupmnflem  46533  limsupmnfuzlem  46539  limsupre3lem  46545  limsupre3uzlem  46548  liminfreuzlem  46615  dvnmul  46756  dvmptfprodlem  46757  ismbl3  46799  ismbl4  46806  fourierdlem50  46969  fourierdlem89  47008  fourierdlem91  47010  dfsalgen2  47154  sge0repnf  47199  sge0lefi  47211  sge0resplit  47219  sge0fodjrnlem  47229  voliunsge0lem  47285  hspdifhsp  47429  isvonmbl  47451  ovnovollem3  47471  vonvolmbl  47474  pimrecltpos  47521  preimaicomnf  47524  pimrecltneg  47537  issmflem  47540  issmfle  47558  issmfgt  47569  smfaddlem1  47576  issmfge  47583  smfresal  47601  smflimmpt  47623  smfinflem  47630  smflimsuplem7  47639  smflimsupmpt  47642  sigarcol  47677  tmachlem-agreeprod  47750  confun  47812  or2expropbi  47907  fsetsniunop  47922  fcoresf1b  47943  f1cof1b  47950  funfocofob  47951  rexsb  47972  euoreqb  47982  ralbinrald  47995  rlimdmafv  48050  fafv2elrnb  48108  tz6.12c-afv2  48115  dfatbrafv2b  48118  fnbrafv2b  48121  rlimdmafv2  48131  f1oresf1o2  48164  el1fzopredsuc  48199  2ffzoeq  48201  nnmul2b  48204  modlt0b  48242  nndivides2  48257  imasetpreimafvbijlemfo  48290  iccpartiun  48319  ichnfb  48350  ich2exprop  48356  sprsymrelfolem2  48378  paireqne  48396  prprelprb  48402  reupr  48407  nprmmul2  48413  nprmmul3  48414  requad01  48522  requad1  48523  requad2  48524  dfodd6  48538  dfeven4  48539  evensumeven  48608  sbgoldbalt  48682  clnbgrel  48729  dfclnbgr6  48757  dfnbgr6  48758  isubgredg  48767  isuspgrim0  48795  isuspgrim  48797  gricushgr  48818  uhgrimisgrgriclem  48831  clnbgrgrim  48835  grimedg  48836  usgrgrtrirex  48851  uspgrlimlem2  48890  uspgrlim  48893  gpgedgiov  48966  gpgedg2ov  48967  gpgedg2iv  48968  gpgnbgrvtx0  48975  gpgnbgrvtx1  48976  isassintop  49110  uzlidlring  49135  rngcisoALTV  49177  ringcisoALTV  49211  isidom3  49245  domnmsuppn0  49284  lindslininds  49379  snlindsntor  49386  isldepslvec2  49400  affinecomb1  49617  prelrrx2b  49629  rrx2plord2  49637  eenglngeehlnm  49654  rrx2vlinest  49656  line2xlem  49668  line2x  49669  line2y  49670  itsclc0xyqsolb  49685  itsclquadb  49691  mpbiran3d  49710  opnneieqv  49822  iscnrm3lem2  49846  fullthinc2  50362  thincciso  50364  alsralrex  50723  alsraln0  50724