Theorem impbid 212

Description: Deduce an equivalence from two implications. Deduction associated with impbi 208 and impbii 209. (Contributed by NM, 24-Jan-1993.) Prove it from impbid21d 211. (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 211	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 52	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bicom1  221  impbid1  225  impcon4bid  227  pm5.74  270  imbi1d  341  pm5.501  366  anbiim  642  impbida  801  dedlem0b  1045  dedlema  1046  dedlemb  1047  albi  1820  alexbii  1835  equequ1  2027  equequ2  2028  spsbbi  2079  elequ1  2121  elequ2  2129  sbequ12  2259  sbft  2277  cbv2w  2342  exsb  2364  dral1v  2374  cbv2  2408  cbv2h  2411  ax12b  2429  dral1  2444  dral1ALT  2445  eupickb  2636  eupickbi  2637  2eu2  2654  ralbi  3093  rexbi  3094  ralbida  3249  ceqsalt  3476  rspcebdv  3572  rspceb2dv  3582  ceqex  3608  elabgtOLD  3629  mob2  3675  reu6  3686  sbciegftOLD  3780  sbcg  3815  2reu2  3850  csbiebt  3880  dfss2  3921  ssdifsym  4228  reupick  4283  reupick2  4285  uneqdifeq  4447  prnebg  4814  preqsnd  4817  prel12g  4822  iuneqconst  4960  disjeq2  5071  disjeq1  5074  disjss3  5099  reusv2lem2  5348  reusv2lem3  5349  alxfr  5356  ralxfrd  5357  ralxfrd2  5361  copsexgw  5448  copsexg  5449  snopeqop  5464  euotd  5471  poeq2  5546  sotric  5572  sotrieq  5573  freq2  5602  seeq1  5604  seeq2  5605  iss  6004  tz7.7  6353  ordtri1  6360  ordelinel  6430  funeq  6522  funssres  6546  f0dom0  6728  fnbrfvb  6894  ssimaex  6929  fvimacnv  7009  elpreima  7014  feldmfvelcdm  7042  eldmrexrnb  7048  fsn  7092  fnsnbg  7122  fnsnbOLD  7124  fmptsng  7126  fmptsnd  7127  fprb  7152  tpres  7159  fconst2g  7161  fconst5  7164  elunirn  7209  f1ocnvfvb  7237  f1prex  7242  foeqcnvco  7258  f1eqcocnv  7259  fliftfun  7270  soisores  7285  isofr  7300  isose  7301  isopo  7304  isoso  7306  f1oiso2  7310  eusvobj2  7362  oprabidw  7401  oprabid  7402  f1opw2  7625  oneqmin  7757  ordelsuc  7774  ordsucelsuc  7776  ordunisuc2  7798  limsuc  7803  fndmexb  7860  resf1ext2b  7889  f1ovv  7914  mptcnfimad  7942  op1steq  7989  opreuopreu  7990  funeldmdif  8004  fvn0elsuppb  8135  extmptsuppeq  8142  rntpos  8193  smoiso2  8313  seqomlem2  8394  oaord  8486  oawordex  8496  oaordex  8497  omord2  8506  om00  8514  oeord  8528  nnaord  8559  nnmord  8572  nnawordex  8577  nnaordex  8578  nnaordex2  8579  eldifsucnn  8604  erexb  8673  swoord1  8680  swoord2  8681  ecelqsdmb  8737  iiner  8740  eceqoveq  8773  mapsnd  8838  ralxpmap  8848  omxpenlem  9020  domtriord  9065  mapxpen  9085  mapunen  9088  ssenen  9093  enfi  9125  nneneq  9144  nndomog  9151  onomeneq  9152  en1eqsnbi  9190  fodomfib  9243  fodomfibOLD  9245  f1opwfi  9270  fsuppunbi  9306  elfiun  9347  suplub2  9378  ordiso2  9434  ordiso  9435  oieu  9458  brwdom2  9492  brwdom3  9501  cantnflem1  9612  ttrclselem2  9649  cardidm  9885  carddom2  9903  pm54.43  9927  acnen  9977  acnen2  9979  alephord  9999  alephinit  10019  dfac5  10053  infdif2  10133  fictb  10168  coflim  10185  fincssdom  10247  fin23lem25  10248  isf32lem9  10285  isf34lem4  10301  fin1a2lem11  10334  axdc3lem2  10375  ficard  10489  fpwwe2lem11  10566  fpwwe2  10568  indpi  10832  nqereq  10860  1idpr  10954  ltapr  10970  leltne  11236  ltlen  11248  ltadd2  11251  addlsub  11567  addid0  11570  ltord1  11677  mul0or  11791  ldiv  11989  ltmul1  12005  mulge0b  12026  lt2msq  12041  nnsub  12203  nn0sub  12465  zrevaddcl  12550  zltp1le  12555  zdiv  12576  nneo  12590  zeo2  12593  zmax  12872  zbtwnre  12873  qrevaddcl  12898  xrlttri  13067  xrleltne  13073  xralrple  13134  xltneg  13146  xleadd1  13184  xlemul1  13219  supxrunb1  13248  supxrunb2  13249  ioo0  13300  iccid  13320  ico0  13321  ioc0  13322  icc0  13323  difreicc  13414  iccsplit  13415  zltaddlt1le  13435  0fz1  13474  uzsplit  13526  fzm1  13537  fzrevral  13542  ssfzo12bi  13691  elfznelfzob  13704  flge  13739  modid2  13832  modmuladd  13850  ssnn0fi  13922  seqf1olem1  13978  hashen  14284  hashdom  14316  hash2exprb  14408  pr2pwpr  14416  hashtpg  14422  hash3tpexb  14431  len0nnbi  14488  ccats1pfxeqbi  14679  reuccatpfxs1  14684  repsdf2  14715  scshwfzeqfzo  14763  relexpindlem  15000  shftlem  15005  shftuz  15006  abslt  15252  absle  15253  rexico  15291  cau3lem  15292  reusq0  15402  rlim2lt  15434  rlim3  15435  o1lo1  15474  rlimdm  15488  climshft  15513  o1dif  15567  isercolllem2  15603  isercoll  15605  zsum  15655  fsum  15657  fsum00  15735  incexclem  15773  zprod  15874  fprod  15878  dvdsval2  16196  moddvds  16204  negdvdsb  16213  dvdsnegb  16214  dvdscmulr  16225  dvdsmulcr  16226  dvdssub2  16242  dvdsaddre2b  16248  fzo0dvdseq  16264  mod2eq1n2dvds  16288  ltoddhalfle  16302  sumodd  16329  bitsf1ocnv  16385  sadcaddlem  16398  bitsuz  16415  dvdsgcdb  16486  gcdzeq  16493  dvdssqlem  16507  lcmeq0  16541  lcmdvdsb  16554  lcmfeq0b  16571  lcmf  16574  lcmfdvdsb  16584  coprmgcdb  16590  cncongr  16610  isprm2lem  16622  dvdsprime  16628  dvdsprm  16644  isprm7  16649  coprm  16652  euclemma  16654  rpexp  16663  prmdvdsncoprmbd  16668  prmdiveq  16727  hashgcdlem  16729  odzdvds  16737  pythagtrip  16776  pc2dvds  16821  pcprmpw2  16824  pcprmpw  16825  vdwapun  16916  ramtcl2  16953  firest  17366  mrieqv2d  17576  isacs2  17590  isssc  17758  setciso  18029  posasymb  18256  pleval2  18272  pltval3  18274  lublecllem  18295  joinle  18321  meetle  18335  latdisd  18434  lubun  18452  clatleglb  18455  letsr  18530  intopsn  18593  gsumval2a  18624  frmdss2  18802  isgrpid2  18923  isgrpinv  18940  f1ghm0to0  19191  symg1bas  19337  oddvdsnn0  19490  oddvds  19493  odeq  19496  odeq1  19506  gexdvds  19530  pgpfi  19551  pgpssslw  19560  fislw  19571  sylow3lem2  19574  lsmelvalm  19597  lsmlub  19610  lsmss1b  19612  lsmss2b  19614  efgs1b  19682  cyggenod  19830  cyggexb  19845  dprdfeq0  19970  ablsimpgfind  20058  ringinvnz1ne0  20252  ringinvnzdiv  20253  unitmulclb  20334  dvreq1  20364  isnzr2  20468  0ringnnzr  20475  0ring01eqbi  20482  rngciso  20588  ringciso  20622  rrgeq0  20650  domneq0  20658  drngmul0orOLD  20711  isabvd  20762  issrngd  20805  lssats2  20968  lspsneq0  20980  lsmelval2  21054  lvecvs0or  21080  lspsneq  21094  lspsneu  21095  lidl1el  21198  lidldvgen  21306  pzriprnglem10  21462  pzriprnglem11  21463  znunit  21535  psgndif  21574  ipeq0  21610  ocvsscon  21647  pjdm2  21683  obselocv  21700  islinds4  21807  psdmul  22126  ply1coe1eq  22261  cply1coe0bi  22263  mat1dimelbas  22432  cramer  22652  toponcomb  22890  tgss3  22947  clsval2  23011  isopn3  23027  elcls3  23044  opncldf1  23045  neiint  23065  neips  23074  opnneissb  23075  opnssneib  23076  opnnei  23081  tpnei  23082  opnneiid  23087  restcld  23133  restopnb  23136  tgcn  23213  tgcnp  23214  subbascn  23215  iscnp4  23224  cnpnei  23225  cncls2  23234  cncls  23235  cnntr  23236  lmss  23259  hausnei2  23314  lpcls  23325  ordtt1  23340  cmpsub  23361  tgcmp  23362  1stcelcls  23422  locfincmp  23487  kgencn2  23518  ptpjpre1  23532  upxp  23584  txcn  23587  txlm  23609  tgqtop  23673  kqfvima  23691  isr0  23698  regr1lem2  23701  hmeoopn  23727  hmeocld  23728  ptuncnv  23768  fbunfip  23830  fgss2  23835  ufilb  23867  ufprim  23870  trufil  23871  cfinufil  23889  ufildr  23892  elfm2  23909  elfm3  23911  rnelfm  23914  fmfnfmlem4  23918  fmco  23922  flimtopon  23931  flimopn  23936  fbflim2  23938  flimrest  23944  flffbas  23956  cnpflf  23962  fclstopon  23973  fclsnei  23980  fclsbas  23982  fclsfnflim  23988  fclscmp  23991  ufilcmp  23993  isfcf  23995  fcfnei  23996  cnpfcf  24002  alexsubb  24007  alexsubALT  24012  cldsubg  24072  tgphaus  24078  tgpt0  24080  tsmsgsum  24100  tsmsres  24105  xbln0  24375  blssexps  24387  blssex  24388  isxms2  24409  prdsbl  24452  neibl  24462  metss  24469  met2ndc  24484  metrest  24485  metcnp3  24501  tngngp3  24617  nmoeq0  24697  xrsxmet  24771  reconn  24790  iccpnfcnv  24915  fgcfil  25244  iscau4  25252  cfilres  25269  iunmbl2  25531  ismbf3d  25628  mbfaddlem  25634  i1faddlem  25667  i1fmullem  25668  ellimc3  25853  dvfsumlem2  26006  tdeglem4  26038  deg1nn0clb  26068  deg1lt0  26069  dvdsq1p  26141  plypf1  26190  0dgrb  26224  plymul0or  26261  taylthlem2  26355  ulmshft  26372  ulmcaulem  26376  ulmcau  26377  cosord  26513  eff1olem  26530  lognegb  26572  eflogeq  26584  logdivlt  26603  efopn  26640  cxpeq0  26660  cxpeq  26740  angpieqvd  26814  dcubic  26829  asinsinb  26880  acoscosb  26881  atantanb  26907  rlimcnp  26948  isppw  27097  isppw2  27098  vmappw  27099  isnsqf  27118  ppieq0  27159  fsumdvdsdiag  27167  dvdsppwf1o  27169  fsumfldivdiag  27173  chpeq0  27192  chteq0  27193  dchrptlem1  27248  lgsdir2lem4  27312  lgsne0  27319  lgsqr  27335  lgsdchrval  27338  gausslemma2dlem1a  27349  lgsquadlem1  27364  m1lgs  27372  2sqreultblem  27432  2sqreunnltblem  27435  nodenselem8  27676  ltlesnd  27760  oldlim  27900  ltslpss  27921  leadds1  28002  ltnegs  28058  negleft  28071  negright  28072  muls0ord  28198  abslts  28262  onlts  28280  n0subs  28376  n0ltsp1le  28378  z12sge0  28496  iscgrglt  28604  brbtwn  28990  brcgr  28991  brbtwn2  28996  axcontlem7  29061  uhgr0vb  29163  edglnl  29234  ausgrusgrb  29256  ushgredgedg  29320  ushgredgedgloop  29322  usgr0vb  29328  usgr1v  29347  nbupgr  29435  nbumgrvtx  29437  nbuhgr2vtx1edgb  29443  edgusgrnbfin  29464  nb3grprlem1  29471  uvtxnbvtxm1  29497  cusgrfilem2  29548  uhgr0edg0rgrb  29666  cusgrm1rusgr  29674  spthonepeq  29843  usgr2pth  29855  wlkiswwlks  29967  wlkiswwlkupgr  29969  wlklnwwlkn  29975  wlklnwwlknupgr  29977  wwlksnextbi  29985  wwlksnredwwlkn0  29987  wwlksnextwrd  29988  wwlksnextprop  30003  usgrwwlks2on  30049  umgrwwlks2on  30050  elwspths2on  30053  elwspths2onw  30054  usgr2wspthons3  30058  elwwlks2  30060  elwspths2spth  30061  clwlkclwwlklem3  30094  loopclwwlkn1b  30135  clwwlknon1sn  30193  clwwlknonwwlknonb  30199  umgr3v3e3cycl  30277  eupth2lem3lem4  30324  frgr0v  30355  frgr3vlem2  30367  2clwwlk2clwwlk  30443  wlkl0  30460  grpoinvf  30626  nvmul0or  30744  nvz  30763  diporthcom  30810  ubthlem3  30966  hvmul0or  31119  his6  31193  hial0  31196  hial02  31197  orthcom  31202  normgt0  31221  ocin  31390  occon3  31391  shsel3  31409  shlub  31508  chssoc  31590  h1de2bi  31648  spansncol  31662  elspansn4  31667  spansnss2  31669  sumspansn  31743  lnopcnbd  32130  lnfncnbd  32151  riesz1  32159  elpjrn  32284  cvcon3  32378  dmdmd  32394  dmdbr3  32399  dmdbr4  32400  dmdbr5  32402  mdslmd1i  32423  atcveq0  32442  chcv1  32449  atssma  32472  atcv0eq  32473  atcv1  32474  bian1dOLD  32549  disjeq1f  32666  br8d  32704  fpwrelmap  32829  xaddeq0  32850  eliccelico  32874  elicoelioo  32875  indf1ofs  32965  isarchiofld  33299  unitdivcld  34085  xrge0iifcnv  34117  lmxrge0  34136  eulerpartlemgh  34562  dstfrvunirn  34659  fnrelpredd  35274  rankfilimb  35285  fineqvnttrclse  35308  loop1cycl  35359  cusgracyclt3v  35378  cvmliftmolem2  35504  cvmlift2lem12  35536  satfvsucsuc  35587  satfdm  35591  fmlasuc  35608  satffunlem1lem2  35625  satffunlem2lem2  35628  mthmb  35803  climuzcnv  35893  br8  35978  br6  35979  br4  35980  funbreq  35992  axextbdist  36020  dfrdg4  36173  cgrcom  36212  cgrcoml  36218  cgrdegen  36226  btwncom  36236  brsegle  36330  brsegle2  36331  colinbtwnle  36340  btwnoutside  36347  broutsideof3  36348  outsidele  36354  lineunray  36369  lineelsb2  36370  elhf2  36397  elicc3  36539  nn0prpwlem  36544  opnbnd  36547  cldbnd  36548  opnregcld  36552  cldregopn  36553  fnessref  36579  refssfne  36580  neibastop2  36583  fnemeet2  36589  fnejoin2  36591  fgmin  36592  ontgval  36653  ordtop  36658  ordcmp  36669  nndivsub  36679  bj-cbval  36908  bj-cbvex  36909  bj-19.21t  37026  bj-19.23t  37027  bj-19.42t  37030  bj-sbft  37043  bj-nnf-cbval  37045  bj-cbv2hv  37072  bj-equsal1t  37097  bj-19.21t0  37105  bj-ceqsalt0  37159  bj-ceqsalt1  37160  bj-xpnzexb  37236  bj-axreprepsep  37350  cgsex2gd  37419  bj-idreseq  37444  bj-imdiridlem  37467  bj-finsumval0  37567  bj-fvimacnv0  37568  bj-isrvec2  37582  bj-bary1  37594  dfgcd3  37606  isbasisrelowllem1  37637  isbasisrelowllem2  37638  finxpsuclem  37679  wl-lem-exsb  37850  wl-mo3t  37860  matunitlindf  37898  poimirlem6  37906  poimirlem7  37907  poimirlem16  37916  poimirlem19  37919  poimirlem22  37922  poimirlem23  37923  poimirlem24  37924  cnambfre  37948  itg2addnc  37954  brabg2  37997  istotbnd3  38051  sstotbnd2  38054  sstotbnd  38055  sstotbnd3  38056  ssbnd  38068  ismtybnd  38087  reheibor  38119  grpoeqdivid  38161  grpokerinj  38173  rngosn3  38204  rngoueqz  38220  1idl  38306  0rngo  38307  divrngidl  38308  igenval2  38346  ispridlc  38350  isdmn3  38354  relcnveq3  38607  iss2  38624  elrelscnveq3  38907  funALTVeq  39065  disjeq  39114  prtlem10  39270  prter2  39286  dral1-o  39309  lshpinN  39394  lsatcveq0  39437  lsatcv0eq  39452  lsatcv1  39453  islshpcv  39458  lkr0f  39499  lkrshp4  39513  lshpkrlem1  39515  lshpset2N  39524  lfl1dim  39526  lfl1dim2N  39527  lub0N  39594  glb0N  39598  oplecon3b  39605  cmtcomN  39654  cmtbr3N  39659  cmtbr4N  39660  cvrnbtwn2  39680  cvrnbtwn3  39681  cvrcon3b  39682  cvrnbtwn4  39684  cvrcmp  39688  atcvreq0  39719  atnle  39722  atlatle  39725  cvlexchb1  39735  cvlcvr1  39744  hlrelat2  39808  exatleN  39809  cvrval3  39818  cvrval4N  39819  cvrexch  39825  atcvr0eq  39831  lnnat  39832  atcvrj0  39833  atcvrj2b  39837  atltcvr  39840  atbtwn  39851  ps-1  39882  3at  39895  islln2a  39922  llncmp  39927  islpln2a  39953  lplncmp  39967  islvol2aN  39997  4at  40018  lvolcmp  40022  pmaple  40166  lncmp  40188  paddss  40250  llnexchb2lem  40273  2polcon4bN  40323  ispsubcl2N  40352  lhpat3  40451  lautcvr  40497  ltrnid  40540  trlval2  40568  trlatn0  40577  ltrnideq  40580  trlnidatb  40582  cdlemeg49lebilem  40944  trlord  40974  cdlemg1a  40975  cdlemg1cex  40993  tendoid0  41230  dva1dim  41390  cdlemm10N  41523  diarnN  41534  cdlemn  41617  dihlspsnssN  41737  dihatexv  41743  dochkrshp  41791  dochkrshp4  41794  djhlsmcl  41819  lcfl6  41905  lcfl8  41907  lcfrvalsnN  41946  lcfrlem9  41955  mapdval2N  42035  mapdordlem2  42042  mapd1o  42053  mapd0  42070  mapdheq2biN  42135  nnproddivdvdsd  42399  primrootspoweq0  42505  aks6d1c1p1  42506  aks6d1c5lem1  42535  sticksstones11  42555  sticksstones22  42567  grpods  42593  unitscyglem2  42595  eqresfnbd  42633  expeq1d  42723  expeqidd  42724  dvdsexpnn  42732  zdivgd  42736  sn-remul0ord  42807  mulgt0b1d  42871  frlmfzowrdb  42903  frlmsnic  42939  evlselvlem  42973  prjspreln0  42996  elrfi  43080  diophrw  43145  eldioph2b  43149  diophin  43158  rexrabdioph  43180  rmxycomplete  43303  coprmdvdsb  43371  jm2.19  43379  jm2.26  43388  jm2.27  43394  limsuc2  43427  dgraa0p  43535  rngunsnply  43555  fiuneneq  43578  unielss  43604  oaabsb  43680  nnoeomeqom  43698  cantnfresb  43710  tfsconcatrn  43728  tfsconcat0b  43732  tfsconcatrev  43734  oadif1lem  43765  oadif1  43766  fzunt  43840  fzuntd  43841  fzunt1d  43842  fzuntgd  43843  pwelg  43945  nzss  44702  dvconstbi  44719  expgrowth  44720  bcc0  44725  axc11next  44791  pm14.24  44817  sbiota1  44819  sbcim2g  44923  sineq0ALT  45321  mapss2  45592  fsneq  45593  fsneqrn  45598  mapssbi  45600  rnmptbd2lem  45635  infnsuprnmpt  45637  rnmptbdlem  45642  xralrple2  45742  infxrunb2  45755  xralrple4  45760  xralrple3  45761  xrralrecnnle  45770  xrralrecnnge  45777  reclt0  45778  supxrunb3  45786  supxrleubrnmpt  45793  xrre4  45798  unb2ltle  45802  rexabslelem  45805  suprleubrnmpt  45809  infxrunb3rnmpt  45815  uzub  45818  supminfrnmpt  45832  iccintsng  45912  sqrlearg  45942  uzinico  45948  preimaiocmnf  45949  limcresiooub  46029  limclr  46042  climeldmeq  46052  limsuppnflem  46097  limsupmnflem  46107  limsupmnfuzlem  46113  limsupre3lem  46119  limsupre3uzlem  46122  liminfreuzlem  46189  dvnmul  46330  dvmptfprodlem  46331  ismbl3  46373  ismbl4  46380  fourierdlem50  46543  fourierdlem89  46582  fourierdlem91  46584  dfsalgen2  46728  sge0repnf  46773  sge0lefi  46785  sge0resplit  46793  sge0fodjrnlem  46803  voliunsge0lem  46859  hspdifhsp  47003  isvonmbl  47025  ovnovollem3  47045  vonvolmbl  47048  pimrecltpos  47095  preimaicomnf  47098  pimrecltneg  47111  issmflem  47114  issmfle  47132  issmfgt  47143  smfaddlem1  47150  issmfge  47157  smfresal  47175  smflimmpt  47197  smfinflem  47204  smflimsuplem7  47213  smflimsupmpt  47216  sigarcol  47251  confun  47328  or2expropbi  47423  fsetsniunop  47438  fcoresf1b  47459  f1cof1b  47466  funfocofob  47467  rexsb  47488  euoreqb  47498  ralbinrald  47511  rlimdmafv  47566  fafv2elrnb  47624  tz6.12c-afv2  47631  dfatbrafv2b  47634  fnbrafv2b  47637  rlimdmafv2  47647  f1oresf1o2  47680  el1fzopredsuc  47714  2ffzoeq  47716  modlt0b  47752  imasetpreimafvbijlemfo  47794  iccpartiun  47823  ichnfb  47854  ich2exprop  47860  sprsymrelfolem2  47882  paireqne  47900  prprelprb  47906  reupr  47911  requad01  48010  requad1  48011  requad2  48012  dfodd6  48026  dfeven4  48027  evensumeven  48096  sbgoldbalt  48170  clnbgrel  48217  dfclnbgr6  48245  dfnbgr6  48246  isubgredg  48255  isuspgrim0  48283  isuspgrim  48285  gricushgr  48306  uhgrimisgrgriclem  48319  clnbgrgrim  48323  grimedg  48324  usgrgrtrirex  48339  uspgrlimlem2  48378  uspgrlim  48381  gpgedgiov  48454  gpgedg2ov  48455  gpgedg2iv  48456  gpgnbgrvtx0  48463  gpgnbgrvtx1  48464  isassintop  48599  uzlidlring  48624  rngcisoALTV  48666  ringcisoALTV  48700  domnmsuppn0  48758  lindslininds  48853  snlindsntor  48860  isldepslvec2  48874  affinecomb1  49091  prelrrx2b  49103  rrx2plord2  49111  eenglngeehlnm  49128  rrx2vlinest  49130  line2xlem  49142  line2x  49143  line2y  49144  itsclc0xyqsolb  49159  itsclquadb  49165  mpbiran3d  49185  opnneieqv  49299  iscnrm3lem2  49323  fullthinc2  49839  thincciso  49841