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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bicom1  224  impbid1  228  impcon4bid  230  pm5.74  273  imbi1d  344  pm5.501  369  anbiimOLD  653  impbida  812  dedlem0b  1058  dedlema  1059  dedlemb  1060  albi  1845  alexbii  1860  equequ1  2052  equequ2  2053  spsbbi  2113  elequ1  2156  elequ2  2164  sbequ12  2293  sbft  2311  cbv2w  2375  exsb  2397  dral1v  2407  cbv2  2441  cbv2h  2444  ax12b  2462  dral1  2477  dral1ALT  2478  eupickb  2669  eupickbi  2670  2eu2  2686  ralbi  3126  rexbi  3127  ralbida  3282  ceqsalt  3496  rspcebdv  3584  rspceb2dv  3594  ceqex  3620  elabgtOLD  3641  mob2  3687  reu6  3698  sbcg  3825  2reu2  3860  csbiebt  3890  dfss2  3931  reupick  4290  reupick2  4292  uneqdifeq  4458  prnebg  4825  preqsnd  4828  prel12g  4833  iuneqconst  4972  disjeq2  5084  disjeq1  5087  disjss3  5112  reusv2lem2  5373  reusv2lem3  5374  alxfr  5381  ralxfrd  5382  ralxfrd2  5386  copsexgw  5475  copsexgwOLD  5476  copsexg  5477  snopeqop  5492  euotd  5499  poeq2  5576  sotric  5602  sotrieq  5603  freq2  5632  seeq1  5634  seeq2  5635  iss  6040  tz7.7  6389  ordtri1  6397  ordelinel  6467  funeq  6559  funssres  6583  f0dom0  6765  fnbrfvb  6934  ssimaex  6969  fsneq  7033  fvimacnv  7051  elpreima  7056  feldmfvelcdm  7084  eldmrexrnb  7090  fsn  7134  fnsnbg  7165  fnsnbOLD  7167  fmptsng  7169  fmptsnd  7170  fprb  7195  tpres  7202  fconst2g  7204  fconst5  7207  elunirn  7252  f1ocnvfvb  7280  f1prex  7285  foeqcnvco  7301  f1eqcocnv  7302  fliftfun  7313  soisores  7328  isofr  7343  isose  7344  isopo  7347  isoso  7349  f1oiso2  7353  eusvobj2  7405  oprabidw  7444  oprabid  7445  f1opw2  7668  oneqmin  7801  ordelsuc  7818  ordsucelsuc  7820  ordunisuc2  7842  limsuc  7847  fndmexb  7905  resf1ext2b  7934  f1ovv  7957  mptcnfimad  7985  op1steq  8032  opreuopreu  8033  funeldmdif  8047  fvn0elsuppb  8179  extmptsuppeq  8186  rntpos  8237  smoiso2  8358  seqomlem2  8440  oaord  8534  oawordex  8544  oaordex  8545  omord2  8554  om00  8562  oeord  8576  nnaord  8607  nnmord  8620  nnawordex  8625  nnaordex  8626  nnaordex2  8627  eldifsucnn  8652  erexb  8722  swoord1  8729  swoord2  8730  ecelqsdmb  8786  iiner  8789  eceqoveq  8822  mapsnd  8886  ralxpmap  8896  omxpenlem  9068  domtriord  9113  mapxpen  9133  mapunen  9136  ssenen  9141  enfi  9173  nneneq  9192  nndomog  9199  onomeneq  9200  en1eqsnbi  9238  fodomfib  9290  f1opwfi  9315  fsuppunbi  9351  elfiun  9392  suplub2  9423  ordiso2  9479  ordiso  9480  oieu  9503  brwdom2  9537  brwdom3  9546  cantnflem1  9660  ttrclselem2  9697  cardidm  9947  carddom2  9965  pm54.43  9989  acnen  10039  acnen2  10041  alephord  10061  alephinit  10081  dfac5  10114  infdif2  10194  fictb  10229  coflim  10247  fincssdom  10309  fin23lem25  10310  isf32lem9  10347  isf34lem4  10363  fin1a2lem11  10396  axdc3lem2  10437  ficard  10551  fpwwe2lem11  10628  fpwwe2  10630  indpi  10894  nqereq  10922  1idpr  11016  ltapr  11032  leltne  11301  ltlen  11313  ltadd2  11316  addlsub  11632  addid0  11635  ltord1  11742  mul0or  11856  ldiv  12051  ltmul1  12067  mulge0b  12087  lt2msq  12102  nnsub  12282  nn0sub  12556  zrevaddcl  12641  zltp1le  12646  zdiv  12668  nneo  12682  zeo2  12685  zmax  12971  zbtwnre  12972  qrevaddcl  12997  xrlttri  13166  xrleltne  13172  xralrple  13233  xltneg  13245  xleadd1  13283  xlemul1  13318  supxrunb1  13347  supxrunb2  13348  ioo0  13399  iccid  13419  ico0  13420  ioc0  13421  icc0  13422  difreicc  13513  iccsplit  13514  zltaddlt1le  13534  0fz1  13574  uzsplit  13626  fzm1  13637  fzrevral  13642  ssfzo12bi  13792  elfznelfzob  13805  flge  13840  modid2  13933  modmuladd  13951  ssnn0fi  14023  seqf1olem1  14079  hashen  14385  hashdom  14417  hash2exprb  14510  pr2pwpr  14518  hashtpg  14524  hash3tpexb  14533  len0nnbi  14590  ccats1pfxeqbi  14781  reuccatpfxs1  14786  repsdf2  14817  scshwfzeqfzo  14865  relexpindlem  15102  shftlem  15107  shftuz  15108  abslt  15368  absle  15369  rexico  15407  cau3lem  15408  reusq0  15518  rlim2lt  15550  rlim3  15551  o1lo1  15590  rlimdm  15604  climshft  15629  o1dif  15683  isercolllem2  15719  isercoll  15721  zsum  15771  fsum  15773  fsum00  15852  incexclem  15892  zprod  15993  fprod  15997  dvdsval2  16315  moddvds  16323  negdvdsb  16332  dvdsnegb  16333  dvdscmulr  16344  dvdsmulcr  16345  dvdssub2  16361  dvdsaddre2b  16367  fzo0dvdseq  16383  mod2eq1n2dvds  16407  ltoddhalfle  16421  sumodd  16448  bitsf1ocnv  16504  sadcaddlem  16517  bitsuz  16534  dvdsgcdb  16605  gcdzeq  16612  dvdssqlem  16626  lcmeq0  16660  lcmdvdsb  16673  lcmfeq0b  16690  lcmf  16693  lcmfdvdsb  16703  coprmgcdb  16709  cncongr  16729  isprm2lem  16741  dvdsprime  16747  dvdsprm  16764  isprm7  16769  coprm  16772  euclemma  16774  rpexp  16783  prmdvdsncoprmbd  16788  prmdiveq  16847  hashgcdlem  16849  odzdvds  16857  pythagtrip  16896  pc2dvds  16941  pcprmpw2  16944  pcprmpw  16945  vdwapun  17036  ramtcl2  17073  firest  17487  mrieqv2d  17697  isacs2  17711  isssc  17879  setciso  18150  posasymb  18377  pleval2  18393  pltval3  18395  lublecllem  18416  joinle  18442  meetle  18456  latdisd  18555  lubun  18573  clatleglb  18576  letsr  18651  intopsn  18714  gsumval2a  18745  frmdss2  18924  isgrpid2  19045  isgrpinv  19062  f1ghm0to0  19317  symg1bas  19463  oddvdsnn0  19616  oddvds  19619  odeq  19622  odeq1  19632  gexdvds  19656  pgpfi  19677  pgpssslw  19686  fislw  19697  sylow3lem2  19700  lsmelvalm  19723  lsmlub  19736  lsmss1b  19738  lsmss2b  19740  efgs1b  19808  cyggenod  19956  cyggexb  19971  dprdfeq0  20096  ablsimpgfind  20184  ringinvnz1ne0  20385  ringinvnzdiv  20386  unitmulclb  20465  dvreq1  20495  isnzr2  20603  0ringnnzr  20611  0ring01eqbi2  20618  0ring01eqbi  20619  rngciso  20725  ringciso  20759  rrgeq0  20787  domneq0  20795  isabvd  20895  issrngd  20938  lssats2  21101  lspsneq0  21113  lsmelval2  21186  lvecvs0or  21212  lspsneq  21226  lspsneu  21227  lidl1el  21331  lidldvgen  21473  pzriprnglem10  21611  pzriprnglem11  21612  znunit  21684  psgndif  21723  ipeq0  21759  ocvsscon  21796  pjdm2  21832  obselocv  21849  islinds4  21956  psdmul  22300  ply1coe1eq  22431  cply1coe0bi  22433  mat1dimelbas  22599  cramer  22819  toponcomb  23057  tgss3  23114  clsval2  23178  isopn3  23194  elcls3  23211  opncldf1  23212  neiint  23232  neips  23241  opnneissb  23242  opnssneib  23243  opnnei  23248  tpnei  23249  opnneiid  23254  restcld  23300  restopnb  23303  tgcn  23380  tgcnp  23381  subbascn  23382  iscnp4  23391  cnpnei  23392  cncls2  23401  cncls  23402  cnntr  23403  lmss  23426  hausnei2  23481  lpcls  23492  ordtt1  23507  cmpsub  23528  tgcmp  23529  1stcelcls  23589  locfincmp  23654  kgencn2  23685  ptpjpre1  23699  upxp  23751  txcn  23754  txlm  23776  tgqtop  23840  kqfvima  23858  isr0  23865  regr1lem2  23868  hmeoopn  23894  hmeocld  23895  ptuncnv  23935  fbunfip  23997  fgss2  24002  ufilb  24034  ufprim  24037  trufil  24038  cfinufil  24056  ufildr  24059  elfm2  24076  elfm3  24078  rnelfm  24081  fmfnfmlem4  24085  fmco  24089  flimtopon  24098  flimopn  24103  fbflim2  24105  flimrest  24111  flffbas  24123  cnpflf  24129  fclstopon  24140  fclsnei  24147  fclsbas  24149  fclsfnflim  24155  fclscmp  24158  ufilcmp  24160  isfcf  24162  fcfnei  24163  cnpfcf  24169  alexsubb  24174  alexsubALT  24179  cldsubg  24239  tgphaus  24245  tgpt0  24247  tsmsgsum  24267  tsmsres  24272  xbln0  24542  blssexps  24554  blssex  24555  isxms2  24576  prdsbl  24619  neibl  24629  metss  24636  met2ndc  24651  metrest  24652  metcnp3  24668  tngngp3  24784  nmoeq0  24864  xrsxmet  24938  reconn  24957  iccpnfcnv  25074  fgcfil  25401  iscau4  25409  cfilres  25426  iunmbl2  25687  ismbf3d  25784  mbfaddlem  25790  i1faddlem  25823  i1fmullem  25824  ellimc3  26009  dvfsumlem2  26157  tdeglem4  26188  deg1nn0clb  26218  deg1lt0  26219  dvdsq1p  26291  plypf1  26340  0dgrb  26374  plymul0or  26410  taylthlem2  26505  ulmshft  26521  ulmcaulem  26525  ulmcau  26526  cosord  26664  eff1olem  26681  lognegb  26723  eflogeq  26735  logdivlt  26754  efopn  26791  cxpeq0  26811  cxpeq  26890  angpieqvd  26964  dcubic  26979  asinsinb  27030  acoscosb  27031  atantanb  27057  rlimcnp  27098  isppw  27246  isppw2  27247  vmappw  27248  isnsqf  27267  ppieq0  27308  fsumdvdsdiag  27316  dvdsppwf1o  27318  fsumfldivdiag  27322  chpeq0  27340  chteq0  27341  dchrptlem1  27396  lgsdir2lem4  27460  lgsne0  27467  lgsqr  27483  lgsdchrval  27486  gausslemma2dlem1a  27497  lgsquadlem1  27512  m1lgs  27520  2sqreultblem  27580  2sqreunnltblem  27583  nodenselem8  27823  ltlesnd  27907  oldlim  28048  ltslpss  28069  leadds1  28150  ltnegs  28206  negleft  28219  negright  28220  muls0ord  28346  abslts  28410  onlts  28428  n0subs  28524  n0ltsp1le  28526  z12sge0  28644  iscgrglt  28751  brbtwn  29192  brcgr  29193  brbtwn2  29198  axcontlem7  29263  uhgr0vb  29365  edglnl  29436  ausgrusgrb  29458  ushgredgedg  29522  ushgredgedgloop  29524  usgr0vb  29530  usgr1v  29549  nbupgr  29637  nbumgrvtx  29639  nbuhgr2vtx1edgb  29645  edgusgrnbfin  29666  nb3grprlem1  29673  uvtxnbvtxm1  29699  cusgrfilem2  29749  uhgr0edg0rgrb  29867  cusgrm1rusgr  29875  spthonepeq  30044  usgr2pth  30056  wlkiswwlks  30168  wlkiswwlkupgr  30170  wlklnwwlkn  30176  wlklnwwlknupgr  30178  wwlksnextbi  30186  wwlksnredwwlkn0  30188  wwlksnextwrd  30189  wwlksnextprop  30204  usgrwwlks2on  30250  umgrwwlks2on  30251  elwspths2on  30254  elwspths2onw  30255  usgr2wspthons3  30259  elwwlks2  30261  elwspths2spth  30262  clwlkclwwlklem3  30295  loopclwwlkn1b  30336  clwwlknon1sn  30394  clwwlknonwwlknonb  30400  umgr3v3e3cycl  30478  eupth2lem3lem4  30525  frgr0v  30556  frgr3vlem2  30568  2clwwlk2clwwlk  30644  wlkl0  30661  grpoinvf  30827  nvmul0or  30945  nvz  30964  diporthcom  31011  ubthlem3  31167  hvmul0or  31320  his6  31394  hial0  31397  hial02  31398  orthcom  31403  normgt0  31422  ocin  31591  occon3  31592  shsel3  31610  shlub  31709  chssoc  31791  h1de2bi  31849  spansncol  31863  elspansn4  31868  spansnss2  31870  sumspansn  31944  lnopcnbd  32331  lnfncnbd  32352  riesz1  32360  elpjrn  32485  cvcon3  32579  dmdmd  32595  dmdbr3  32600  dmdbr4  32601  dmdbr5  32603  mdslmd1i  32624  atcveq0  32643  chcv1  32650  atssma  32673  atcv0eq  32674  atcv1  32675  disjeq1f  32861  br8d  32896  fpwrelmap  33021  xaddeq0  33041  eliccelico  33065  elicoelioo  33066  indf1ofs  33129  isarchiofld  33462  unitdivcld  34238  xrge0iifcnv  34270  lmxrge0  34289  eulerpartlemgh  34715  dstfrvunirn  34812  fnrelpredd  35427  rankfilimb  35441  fineqvnttrclse  35472  loop1cycl  35564  cusgracyclt3v  35583  cvmliftmolem2  35709  cvmlift2lem12  35741  satfvsucsuc  35792  satfdm  35796  fmlasuc  35813  satffunlem1lem2  35830  satffunlem2lem2  35833  mthmb  36008  climuzcnv  36098  br8  36183  br6  36184  br4  36185  funbreq  36197  axextbdist  36225  dfrdg4  36378  cgrcom  36417  cgrcoml  36423  cgrdegen  36431  btwncom  36441  brsegle  36535  brsegle2  36536  colinbtwnle  36545  btwnoutside  36552  broutsideof3  36553  outsidele  36559  lineunray  36574  lineelsb2  36575  elhf2  36602  elicc3  36753  nn0prpwlem  36758  opnbnd  36761  cldbnd  36762  opnregcld  36766  cldregopn  36767  fnessref  36793  refssfne  36794  neibastop2  36797  fnemeet2  36803  fnejoin2  36805  fgmin  36806  ontgval  36867  ordtop  36872  ordcmp  36883  nndivsub  36893  bj-cbval  37193  bj-cbvex  37194  bj-19.21t  37311  bj-19.23t  37312  bj-19.42t  37315  bj-sbft  37328  bj-nnf-cbval  37330  bj-cbv2hv  37357  bj-equsal1t  37382  bj-19.21t0  37390  bj-ceqsalt0  37444  bj-ceqsalt1  37445  bj-xpnzexb  37522  bj-axreprepsep  37637  cgsex2gd  37706  bj-idreseq  37731  bj-imdiridlem  37754  bj-finsumval0  37854  bj-fvimacnv0  37855  bj-isrvec2  37869  bj-bary1  37881  dfgcd3  37893  isbasisrelowllem1  37926  isbasisrelowllem2  37927  finxpsuclem  37968  wl-lem-exsb  38146  wl-mo3t  38156  matunitlindf  38194  poimirlem6  38202  poimirlem7  38203  poimirlem16  38212  poimirlem19  38215  poimirlem22  38218  poimirlem23  38219  poimirlem24  38220  cnambfre  38244  itg2addnc  38250  brabg2  38293  istotbnd3  38347  sstotbnd2  38350  sstotbnd  38351  sstotbnd3  38352  ssbnd  38364  ismtybnd  38383  reheibor  38415  grpoeqdivid  38457  grpokerinj  38469  rngosn3  38500  rngoueqz  38516  1idl  38602  0rngo  38603  divrngidl  38604  igenval2  38642  ispridlc  38646  isdmn3  38650  relcnveq3  38903  iss2  38920  elrelscnveq3  39203  funALTVeq  39361  disjeq  39410  prtlem10  39566  prter2  39582  dral1-o  39605  lshpinN  39690  lsatcveq0  39733  lsatcv0eq  39748  lsatcv1  39749  islshpcv  39754  lkr0f  39795  lkrshp4  39809  lshpkrlem1  39811  lshpset2N  39820  lfl1dim  39822  lfl1dim2N  39823  lub0N  39890  glb0N  39894  oplecon3b  39901  cmtcomN  39950  cmtbr3N  39955  cmtbr4N  39956  cvrnbtwn2  39976  cvrnbtwn3  39977  cvrcon3b  39978  cvrnbtwn4  39980  cvrcmp  39984  atcvreq0  40015  atnle  40018  atlatle  40021  cvlexchb1  40031  cvlcvr1  40040  hlrelat2  40104  exatleN  40105  cvrval3  40114  cvrval4N  40115  cvrexch  40121  atcvr0eq  40127  lnnat  40128  atcvrj0  40129  atcvrj2b  40133  atltcvr  40136  atbtwn  40147  ps-1  40178  3at  40191  islln2a  40218  llncmp  40223  islpln2a  40249  lplncmp  40263  islvol2aN  40293  4at  40314  lvolcmp  40318  pmaple  40462  lncmp  40484  paddss  40546  llnexchb2lem  40569  2polcon4bN  40619  ispsubcl2N  40648  lhpat3  40747  lautcvr  40793  ltrnid  40836  trlval2  40864  trlatn0  40873  ltrnideq  40876  trlnidatb  40878  cdlemeg49lebilem  41240  trlord  41270  cdlemg1a  41271  cdlemg1cex  41289  tendoid0  41526  dva1dim  41686  cdlemm10N  41819  diarnN  41830  cdlemn  41913  dihlspsnssN  42033  dihatexv  42039  dochkrshp  42087  dochkrshp4  42090  djhlsmcl  42115  lcfl6  42201  lcfl8  42203  lcfrvalsnN  42242  lcfrlem9  42251  mapdval2N  42331  mapdordlem2  42338  mapd1o  42349  mapd0  42366  mapdheq2biN  42431  nnproddivdvdsd  42694  primrootspoweq0  42800  aks6d1c1p1  42801  aks6d1c5lem1  42830  sticksstones11  42850  sticksstones22  42862  grpods  42888  unitscyglem2  42890  eqresfnbd  42930  expeq1d  43012  expeqidd  43013  dvdsexpnn  43021  zdivgd  43025  sn-remul0ord  43096  mulgt0b1d  43173  frlmfzowrdb  43205  frlmsnic  43237  evlselvlem  43249  prjspreln0  43270  elrfi  43354  diophrw  43419  eldioph2b  43423  diophin  43432  rexrabdioph  43450  rmxycomplete  43573  coprmdvdsb  43641  jm2.19  43649  jm2.26  43658  jm2.27  43664  limsuc2  43697  dgraa0p  43805  rngunsnply  43825  fiuneneq  43848  unielss  43874  oaabsb  43950  nnoeomeqom  43968  cantnfresb  43980  tfsconcatrn  43998  tfsconcat0b  44002  tfsconcatrev  44004  oadif1lem  44035  oadif1  44036  fzunt  44110  fzuntd  44111  fzunt1d  44112  fzuntgd  44113  pwelg  44215  nzss  44956  dvconstbi  44973  expgrowth  44974  bcc0  44979  axc11next  45045  pm14.24  45071  sbiota1  45073  sbcim2g  45176  sineq0ALT  45574  mapss2  45851  fsneqrn  45856  mapssbi  45858  rnmptbd2lem  45892  infnsuprnmpt  45894  rnmptbdlem  45899  xralrple2  45999  infxrunb2  46012  xralrple4  46017  xralrple3  46018  xrralrecnnle  46027  xrralrecnnge  46034  reclt0  46035  supxrunb3  46043  supxrleubrnmpt  46049  xrre4  46054  unb2ltle  46058  rexabslelem  46061  suprleubrnmpt  46065  infxrunb3rnmpt  46071  uzub  46074  supminfrnmpt  46088  iccintsng  46168  sqrlearg  46198  uzinico  46204  preimaiocmnf  46205  limcresiooub  46285  limclr  46298  climeldmeq  46308  limsuppnflem  46353  limsupmnflem  46363  limsupmnfuzlem  46369  limsupre3lem  46375  limsupre3uzlem  46378  liminfreuzlem  46445  dvnmul  46586  dvmptfprodlem  46587  ismbl3  46629  ismbl4  46636  fourierdlem50  46799  fourierdlem89  46838  fourierdlem91  46840  dfsalgen2  46984  sge0repnf  47029  sge0lefi  47041  sge0resplit  47049  sge0fodjrnlem  47059  voliunsge0lem  47115  hspdifhsp  47259  isvonmbl  47281  ovnovollem3  47301  vonvolmbl  47304  pimrecltpos  47351  preimaicomnf  47354  pimrecltneg  47367  issmflem  47370  issmfle  47388  issmfgt  47399  smfaddlem1  47406  issmfge  47413  smfresal  47431  smflimmpt  47453  smfinflem  47460  smflimsuplem7  47469  smflimsupmpt  47472  sigarcol  47507  confun  47602  or2expropbi  47697  fsetsniunop  47712  fcoresf1b  47733  f1cof1b  47740  funfocofob  47741  rexsb  47762  euoreqb  47772  ralbinrald  47785  rlimdmafv  47840  fafv2elrnb  47898  tz6.12c-afv2  47905  dfatbrafv2b  47908  fnbrafv2b  47911  rlimdmafv2  47921  f1oresf1o2  47954  el1fzopredsuc  47989  2ffzoeq  47991  nnmul2b  47994  modlt0b  48032  nndivides2  48047  imasetpreimafvbijlemfo  48080  iccpartiun  48109  ichnfb  48140  ich2exprop  48146  sprsymrelfolem2  48168  paireqne  48186  prprelprb  48192  reupr  48197  nprmmul2  48203  nprmmul3  48204  requad01  48312  requad1  48313  requad2  48314  dfodd6  48328  dfeven4  48329  evensumeven  48398  sbgoldbalt  48472  clnbgrel  48519  dfclnbgr6  48547  dfnbgr6  48548  isubgredg  48557  isuspgrim0  48585  isuspgrim  48587  gricushgr  48608  uhgrimisgrgriclem  48621  clnbgrgrim  48625  grimedg  48626  usgrgrtrirex  48641  uspgrlimlem2  48680  uspgrlim  48683  gpgedgiov  48756  gpgedg2ov  48757  gpgedg2iv  48758  gpgnbgrvtx0  48765  gpgnbgrvtx1  48766  isassintop  48901  uzlidlring  48926  rngcisoALTV  48968  ringcisoALTV  49002  domnmsuppn0  49071  lindslininds  49166  snlindsntor  49173  isldepslvec2  49187  affinecomb1  49404  prelrrx2b  49416  rrx2plord2  49424  eenglngeehlnm  49441  rrx2vlinest  49443  line2xlem  49455  line2x  49456  line2y  49457  itsclc0xyqsolb  49472  itsclquadb  49478  mpbiran3d  49497  opnneieqv  49611  iscnrm3lem2  49635  fullthinc2  50151  thincciso  50153