Theorem impbid 214

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bicom1  223  impbid1  227  impcon4bid  229  pm5.74  272  imbi1d  343  pm5.501  368  anbiimOLD  651  impbida  810  dedlem0b  1056  dedlema  1057  dedlemb  1058  albi  1840  alexbii  1855  equequ1  2047  equequ2  2048  spsbbi  2108  elequ1  2151  elequ2  2159  sbequ12  2288  sbft  2306  cbv2w  2370  exsb  2392  dral1v  2402  cbv2  2436  cbv2h  2439  ax12b  2457  dral1  2472  dral1ALT  2473  eupickb  2664  eupickbi  2665  2eu2  2681  ralbi  3119  rexbi  3120  ralbida  3275  ceqsalt  3489  rspcebdv  3577  rspceb2dv  3587  ceqex  3613  elabgtOLD  3634  mob2  3680  reu6  3691  sbcg  3818  2reu2  3853  csbiebt  3883  dfss2  3924  reupick  4283  reupick2  4285  uneqdifeq  4448  prnebg  4816  preqsnd  4819  prel12g  4824  iuneqconst  4963  disjeq2  5073  disjeq1  5076  disjss3  5101  reusv2lem2  5358  reusv2lem3  5359  alxfr  5366  ralxfrd  5367  ralxfrd2  5371  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  snopeqop  5477  euotd  5484  poeq2  5561  sotric  5587  sotrieq  5588  freq2  5617  seeq1  5619  seeq2  5620  iss  6026  tz7.7  6374  ordtri1  6381  ordelinel  6451  funeq  6543  funssres  6567  f0dom0  6750  fnbrfvb  6919  ssimaex  6954  fsneq  7018  fvimacnv  7036  elpreima  7041  feldmfvelcdm  7069  eldmrexrnb  7075  fsn  7119  fnsnbg  7150  fnsnbOLD  7152  fmptsng  7154  fmptsnd  7155  fprb  7180  tpres  7187  fconst2g  7189  fconst5  7192  elunirn  7237  f1ocnvfvb  7265  f1prex  7270  foeqcnvco  7286  f1eqcocnv  7287  fliftfun  7298  soisores  7313  isofr  7328  isose  7329  isopo  7332  isoso  7334  f1oiso2  7338  eusvobj2  7390  oprabidw  7429  oprabid  7430  f1opw2  7653  oneqmin  7785  ordelsuc  7802  ordsucelsuc  7804  ordunisuc2  7826  limsuc  7831  fndmexb  7889  resf1ext2b  7918  f1ovv  7941  mptcnfimad  7969  op1steq  8016  opreuopreu  8017  funeldmdif  8031  fvn0elsuppb  8163  extmptsuppeq  8170  rntpos  8221  smoiso2  8342  seqomlem2  8424  oaord  8518  oawordex  8528  oaordex  8529  omord2  8538  om00  8546  oeord  8560  nnaord  8591  nnmord  8604  nnawordex  8609  nnaordex  8610  nnaordex2  8611  eldifsucnn  8636  erexb  8706  swoord1  8713  swoord2  8714  ecelqsdmb  8770  iiner  8773  eceqoveq  8806  mapsnd  8870  ralxpmap  8880  omxpenlem  9052  domtriord  9097  mapxpen  9117  mapunen  9120  ssenen  9125  enfi  9157  nneneq  9176  nndomog  9183  onomeneq  9184  en1eqsnbi  9222  fodomfib  9275  fodomfibOLD  9276  f1opwfi  9301  fsuppunbi  9337  elfiun  9378  suplub2  9409  ordiso2  9465  ordiso  9466  oieu  9489  brwdom2  9523  brwdom3  9532  cantnflem1  9646  ttrclselem2  9683  cardidm  9919  carddom2  9937  pm54.43  9961  acnen  10011  acnen2  10013  alephord  10033  alephinit  10053  dfac5  10087  infdif2  10167  fictb  10202  coflim  10220  fincssdom  10282  fin23lem25  10283  isf32lem9  10320  isf34lem4  10336  fin1a2lem11  10369  axdc3lem2  10410  ficard  10524  fpwwe2lem11  10601  fpwwe2  10603  indpi  10867  nqereq  10895  1idpr  10989  ltapr  11005  leltne  11274  ltlen  11286  ltadd2  11289  addlsub  11605  addid0  11608  ltord1  11715  mul0or  11829  ldiv  12027  ltmul1  12043  mulge0b  12064  lt2msq  12079  nnsub  12259  nn0sub  12533  zrevaddcl  12618  zltp1le  12623  zdiv  12645  nneo  12659  zeo2  12662  zmax  12948  zbtwnre  12949  qrevaddcl  12974  xrlttri  13143  xrleltne  13149  xralrple  13210  xltneg  13222  xleadd1  13260  xlemul1  13295  supxrunb1  13324  supxrunb2  13325  ioo0  13376  iccid  13396  ico0  13397  ioc0  13398  icc0  13399  difreicc  13490  iccsplit  13491  zltaddlt1le  13511  0fz1  13551  uzsplit  13603  fzm1  13614  fzrevral  13619  ssfzo12bi  13769  elfznelfzob  13782  flge  13817  modid2  13910  modmuladd  13928  ssnn0fi  14000  seqf1olem1  14056  hashen  14362  hashdom  14394  hash2exprb  14486  pr2pwpr  14494  hashtpg  14500  hash3tpexb  14509  len0nnbi  14566  ccats1pfxeqbi  14757  reuccatpfxs1  14762  repsdf2  14793  scshwfzeqfzo  14841  relexpindlem  15078  shftlem  15083  shftuz  15084  abslt  15344  absle  15345  rexico  15383  cau3lem  15384  reusq0  15494  rlim2lt  15526  rlim3  15527  o1lo1  15566  rlimdm  15580  climshft  15605  o1dif  15659  isercolllem2  15695  isercoll  15697  zsum  15747  fsum  15749  fsum00  15828  incexclem  15868  zprod  15969  fprod  15973  dvdsval2  16291  moddvds  16299  negdvdsb  16308  dvdsnegb  16309  dvdscmulr  16320  dvdsmulcr  16321  dvdssub2  16337  dvdsaddre2b  16343  fzo0dvdseq  16359  mod2eq1n2dvds  16383  ltoddhalfle  16397  sumodd  16424  bitsf1ocnv  16480  sadcaddlem  16493  bitsuz  16510  dvdsgcdb  16581  gcdzeq  16588  dvdssqlem  16602  lcmeq0  16636  lcmdvdsb  16649  lcmfeq0b  16666  lcmf  16669  lcmfdvdsb  16679  coprmgcdb  16685  cncongr  16705  isprm2lem  16717  dvdsprime  16723  dvdsprm  16740  isprm7  16745  coprm  16748  euclemma  16750  rpexp  16759  prmdvdsncoprmbd  16764  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  pythagtrip  16872  pc2dvds  16917  pcprmpw2  16920  pcprmpw  16921  vdwapun  17012  ramtcl2  17049  firest  17463  mrieqv2d  17673  isacs2  17687  isssc  17855  setciso  18126  posasymb  18353  pleval2  18369  pltval3  18371  lublecllem  18392  joinle  18418  meetle  18432  latdisd  18531  lubun  18549  clatleglb  18552  letsr  18627  intopsn  18690  gsumval2a  18721  frmdss2  18899  isgrpid2  19020  isgrpinv  19037  f1ghm0to0  19287  symg1bas  19433  oddvdsnn0  19586  oddvds  19589  odeq  19592  odeq1  19602  gexdvds  19626  pgpfi  19647  pgpssslw  19656  fislw  19667  sylow3lem2  19670  lsmelvalm  19693  lsmlub  19706  lsmss1b  19708  lsmss2b  19710  efgs1b  19778  cyggenod  19926  cyggexb  19941  dprdfeq0  20066  ablsimpgfind  20154  ringinvnz1ne0  20352  ringinvnzdiv  20353  unitmulclb  20432  dvreq1  20462  isnzr2  20570  0ringnnzr  20577  0ring01eqbi  20584  rngciso  20690  ringciso  20724  rrgeq0  20752  domneq0  20760  drngmul0orOLD  20813  isabvd  20863  issrngd  20906  lssats2  21069  lspsneq0  21081  lsmelval2  21154  lvecvs0or  21180  lspsneq  21194  lspsneu  21195  lidl1el  21298  lidldvgen  21406  pzriprnglem10  21544  pzriprnglem11  21545  znunit  21617  psgndif  21656  ipeq0  21692  ocvsscon  21729  pjdm2  21765  obselocv  21782  islinds4  21889  psdmul  22233  ply1coe1eq  22365  cply1coe0bi  22367  mat1dimelbas  22533  cramer  22753  toponcomb  22991  tgss3  23048  clsval2  23112  isopn3  23128  elcls3  23145  opncldf1  23146  neiint  23166  neips  23175  opnneissb  23176  opnssneib  23177  opnnei  23182  tpnei  23183  opnneiid  23188  restcld  23234  restopnb  23237  tgcn  23314  tgcnp  23315  subbascn  23316  iscnp4  23325  cnpnei  23326  cncls2  23335  cncls  23336  cnntr  23337  lmss  23360  hausnei2  23415  lpcls  23426  ordtt1  23441  cmpsub  23462  tgcmp  23463  1stcelcls  23523  locfincmp  23588  kgencn2  23619  ptpjpre1  23633  upxp  23685  txcn  23688  txlm  23710  tgqtop  23774  kqfvima  23792  isr0  23799  regr1lem2  23802  hmeoopn  23828  hmeocld  23829  ptuncnv  23869  fbunfip  23931  fgss2  23936  ufilb  23968  ufprim  23971  trufil  23972  cfinufil  23990  ufildr  23993  elfm2  24010  elfm3  24012  rnelfm  24015  fmfnfmlem4  24019  fmco  24023  flimtopon  24032  flimopn  24037  fbflim2  24039  flimrest  24045  flffbas  24057  cnpflf  24063  fclstopon  24074  fclsnei  24081  fclsbas  24083  fclsfnflim  24089  fclscmp  24092  ufilcmp  24094  isfcf  24096  fcfnei  24097  cnpfcf  24103  alexsubb  24108  alexsubALT  24113  cldsubg  24173  tgphaus  24179  tgpt0  24181  tsmsgsum  24201  tsmsres  24206  xbln0  24476  blssexps  24488  blssex  24489  isxms2  24510  prdsbl  24553  neibl  24563  metss  24570  met2ndc  24585  metrest  24586  metcnp3  24602  tngngp3  24718  nmoeq0  24798  xrsxmet  24872  reconn  24891  iccpnfcnv  25008  fgcfil  25335  iscau4  25343  cfilres  25360  iunmbl2  25621  ismbf3d  25718  mbfaddlem  25724  i1faddlem  25757  i1fmullem  25758  ellimc3  25943  dvfsumlem2  26091  tdeglem4  26122  deg1nn0clb  26152  deg1lt0  26153  dvdsq1p  26225  plypf1  26274  0dgrb  26308  plymul0or  26344  taylthlem2  26439  ulmshft  26455  ulmcaulem  26459  ulmcau  26460  cosord  26598  eff1olem  26615  lognegb  26657  eflogeq  26669  logdivlt  26688  efopn  26725  cxpeq0  26745  cxpeq  26824  angpieqvd  26898  dcubic  26913  asinsinb  26964  acoscosb  26965  atantanb  26991  rlimcnp  27032  isppw  27180  isppw2  27181  vmappw  27182  isnsqf  27201  ppieq0  27242  fsumdvdsdiag  27250  dvdsppwf1o  27252  fsumfldivdiag  27256  chpeq0  27274  chteq0  27275  dchrptlem1  27330  lgsdir2lem4  27394  lgsne0  27401  lgsqr  27417  lgsdchrval  27420  gausslemma2dlem1a  27431  lgsquadlem1  27446  m1lgs  27454  2sqreultblem  27514  2sqreunnltblem  27517  nodenselem8  27757  ltlesnd  27841  oldlim  27982  ltslpss  28003  leadds1  28084  ltnegs  28140  negleft  28153  negright  28154  muls0ord  28280  abslts  28344  onlts  28362  n0subs  28458  n0ltsp1le  28460  z12sge0  28578  iscgrglt  28685  brbtwn  29102  brcgr  29103  brbtwn2  29108  axcontlem7  29173  uhgr0vb  29275  edglnl  29346  ausgrusgrb  29368  ushgredgedg  29432  ushgredgedgloop  29434  usgr0vb  29440  usgr1v  29459  nbupgr  29547  nbumgrvtx  29549  nbuhgr2vtx1edgb  29555  edgusgrnbfin  29576  nb3grprlem1  29583  uvtxnbvtxm1  29609  cusgrfilem2  29659  uhgr0edg0rgrb  29777  cusgrm1rusgr  29785  spthonepeq  29954  usgr2pth  29966  wlkiswwlks  30078  wlkiswwlkupgr  30080  wlklnwwlkn  30086  wlklnwwlknupgr  30088  wwlksnextbi  30096  wwlksnredwwlkn0  30098  wwlksnextwrd  30099  wwlksnextprop  30114  usgrwwlks2on  30160  umgrwwlks2on  30161  elwspths2on  30164  elwspths2onw  30165  usgr2wspthons3  30169  elwwlks2  30171  elwspths2spth  30172  clwlkclwwlklem3  30205  loopclwwlkn1b  30246  clwwlknon1sn  30304  clwwlknonwwlknonb  30310  umgr3v3e3cycl  30388  eupth2lem3lem4  30435  frgr0v  30466  frgr3vlem2  30478  2clwwlk2clwwlk  30554  wlkl0  30571  grpoinvf  30737  nvmul0or  30855  nvz  30874  diporthcom  30921  ubthlem3  31077  hvmul0or  31230  his6  31304  hial0  31307  hial02  31308  orthcom  31313  normgt0  31332  ocin  31501  occon3  31502  shsel3  31520  shlub  31619  chssoc  31701  h1de2bi  31759  spansncol  31773  elspansn4  31778  spansnss2  31780  sumspansn  31854  lnopcnbd  32241  lnfncnbd  32262  riesz1  32270  elpjrn  32395  cvcon3  32489  dmdmd  32505  dmdbr3  32510  dmdbr4  32511  dmdbr5  32513  mdslmd1i  32534  atcveq0  32553  chcv1  32560  atssma  32583  atcv0eq  32584  atcv1  32585  bian1dOLD  32660  disjeq1f  32775  br8d  32812  fpwrelmap  32937  xaddeq0  32957  eliccelico  32981  elicoelioo  32982  indf1ofs  33046  isarchiofld  33381  unitdivcld  34200  xrge0iifcnv  34232  lmxrge0  34251  eulerpartlemgh  34677  dstfrvunirn  34774  fnrelpredd  35389  rankfilimb  35402  fineqvnttrclse  35424  loop1cycl  35492  cusgracyclt3v  35511  cvmliftmolem2  35637  cvmlift2lem12  35669  satfvsucsuc  35720  satfdm  35724  fmlasuc  35741  satffunlem1lem2  35758  satffunlem2lem2  35761  mthmb  35936  climuzcnv  36026  br8  36111  br6  36112  br4  36113  funbreq  36125  axextbdist  36153  dfrdg4  36306  cgrcom  36345  cgrcoml  36351  cgrdegen  36359  btwncom  36369  brsegle  36463  brsegle2  36464  colinbtwnle  36473  btwnoutside  36480  broutsideof3  36481  outsidele  36487  lineunray  36502  lineelsb2  36503  elhf2  36530  elicc3  36682  nn0prpwlem  36687  opnbnd  36690  cldbnd  36691  opnregcld  36695  cldregopn  36696  fnessref  36722  refssfne  36723  neibastop2  36726  fnemeet2  36732  fnejoin2  36734  fgmin  36735  ontgval  36796  ordtop  36801  ordcmp  36812  nndivsub  36822  bj-cbval  37123  bj-cbvex  37124  bj-19.21t  37241  bj-19.23t  37242  bj-19.42t  37245  bj-sbft  37258  bj-nnf-cbval  37260  bj-cbv2hv  37287  bj-equsal1t  37312  bj-19.21t0  37320  bj-ceqsalt0  37374  bj-ceqsalt1  37375  bj-xpnzexb  37451  bj-axreprepsep  37565  cgsex2gd  37634  bj-idreseq  37659  bj-imdiridlem  37682  bj-finsumval0  37782  bj-fvimacnv0  37783  bj-isrvec2  37797  bj-bary1  37809  dfgcd3  37821  isbasisrelowllem1  37854  isbasisrelowllem2  37855  finxpsuclem  37896  wl-lem-exsb  38074  wl-mo3t  38084  matunitlindf  38122  poimirlem6  38130  poimirlem7  38131  poimirlem16  38140  poimirlem19  38143  poimirlem22  38146  poimirlem23  38147  poimirlem24  38148  cnambfre  38172  itg2addnc  38178  brabg2  38221  istotbnd3  38275  sstotbnd2  38278  sstotbnd  38279  sstotbnd3  38280  ssbnd  38292  ismtybnd  38311  reheibor  38343  grpoeqdivid  38385  grpokerinj  38397  rngosn3  38428  rngoueqz  38444  1idl  38530  0rngo  38531  divrngidl  38532  igenval2  38570  ispridlc  38574  isdmn3  38578  relcnveq3  38831  iss2  38848  elrelscnveq3  39131  funALTVeq  39289  disjeq  39338  prtlem10  39494  prter2  39510  dral1-o  39533  lshpinN  39618  lsatcveq0  39661  lsatcv0eq  39676  lsatcv1  39677  islshpcv  39682  lkr0f  39723  lkrshp4  39737  lshpkrlem1  39739  lshpset2N  39748  lfl1dim  39750  lfl1dim2N  39751  lub0N  39818  glb0N  39822  oplecon3b  39829  cmtcomN  39878  cmtbr3N  39883  cmtbr4N  39884  cvrnbtwn2  39904  cvrnbtwn3  39905  cvrcon3b  39906  cvrnbtwn4  39908  cvrcmp  39912  atcvreq0  39943  atnle  39946  atlatle  39949  cvlexchb1  39959  cvlcvr1  39968  hlrelat2  40032  exatleN  40033  cvrval3  40042  cvrval4N  40043  cvrexch  40049  atcvr0eq  40055  lnnat  40056  atcvrj0  40057  atcvrj2b  40061  atltcvr  40064  atbtwn  40075  ps-1  40106  3at  40119  islln2a  40146  llncmp  40151  islpln2a  40177  lplncmp  40191  islvol2aN  40221  4at  40242  lvolcmp  40246  pmaple  40390  lncmp  40412  paddss  40474  llnexchb2lem  40497  2polcon4bN  40547  ispsubcl2N  40576  lhpat3  40675  lautcvr  40721  ltrnid  40764  trlval2  40792  trlatn0  40801  ltrnideq  40804  trlnidatb  40806  cdlemeg49lebilem  41168  trlord  41198  cdlemg1a  41199  cdlemg1cex  41217  tendoid0  41454  dva1dim  41614  cdlemm10N  41747  diarnN  41758  cdlemn  41841  dihlspsnssN  41961  dihatexv  41967  dochkrshp  42015  dochkrshp4  42018  djhlsmcl  42043  lcfl6  42129  lcfl8  42131  lcfrvalsnN  42170  lcfrlem9  42179  mapdval2N  42259  mapdordlem2  42266  mapd1o  42277  mapd0  42294  mapdheq2biN  42359  nnproddivdvdsd  42622  primrootspoweq0  42728  aks6d1c1p1  42729  aks6d1c5lem1  42758  sticksstones11  42778  sticksstones22  42790  grpods  42816  unitscyglem2  42818  eqresfnbd  42856  expeq1d  42938  expeqidd  42939  dvdsexpnn  42947  zdivgd  42951  sn-remul0ord  43022  mulgt0b1d  43099  frlmfzowrdb  43131  frlmsnic  43163  evlselvlem  43175  prjspreln0  43196  elrfi  43280  diophrw  43345  eldioph2b  43349  diophin  43358  rexrabdioph  43376  rmxycomplete  43499  coprmdvdsb  43567  jm2.19  43575  jm2.26  43584  jm2.27  43590  limsuc2  43623  dgraa0p  43731  rngunsnply  43751  fiuneneq  43774  unielss  43800  oaabsb  43876  nnoeomeqom  43894  cantnfresb  43906  tfsconcatrn  43924  tfsconcat0b  43928  tfsconcatrev  43930  oadif1lem  43961  oadif1  43962  fzunt  44036  fzuntd  44037  fzunt1d  44038  fzuntgd  44039  pwelg  44141  nzss  44898  dvconstbi  44915  expgrowth  44916  bcc0  44921  axc11next  44987  pm14.24  45013  sbiota1  45015  sbcim2g  45119  sineq0ALT  45517  mapss2  45787  fsneqrn  45792  mapssbi  45794  rnmptbd2lem  45828  infnsuprnmpt  45830  rnmptbdlem  45835  xralrple2  45935  infxrunb2  45948  xralrple4  45953  xralrple3  45954  xrralrecnnle  45963  xrralrecnnge  45970  reclt0  45971  supxrunb3  45979  supxrleubrnmpt  45985  xrre4  45990  unb2ltle  45994  rexabslelem  45997  suprleubrnmpt  46001  infxrunb3rnmpt  46007  uzub  46010  supminfrnmpt  46024  iccintsng  46104  sqrlearg  46134  uzinico  46140  preimaiocmnf  46141  limcresiooub  46221  limclr  46234  climeldmeq  46244  limsuppnflem  46289  limsupmnflem  46299  limsupmnfuzlem  46305  limsupre3lem  46311  limsupre3uzlem  46314  liminfreuzlem  46381  dvnmul  46522  dvmptfprodlem  46523  ismbl3  46565  ismbl4  46572  fourierdlem50  46735  fourierdlem89  46774  fourierdlem91  46776  dfsalgen2  46920  sge0repnf  46965  sge0lefi  46977  sge0resplit  46985  sge0fodjrnlem  46995  voliunsge0lem  47051  hspdifhsp  47195  isvonmbl  47217  ovnovollem3  47237  vonvolmbl  47240  pimrecltpos  47287  preimaicomnf  47290  pimrecltneg  47303  issmflem  47306  issmfle  47324  issmfgt  47335  smfaddlem1  47342  issmfge  47349  smfresal  47367  smflimmpt  47389  smfinflem  47396  smflimsuplem7  47405  smflimsupmpt  47408  sigarcol  47443  confun  47538  or2expropbi  47633  fsetsniunop  47648  fcoresf1b  47669  f1cof1b  47676  funfocofob  47677  rexsb  47698  euoreqb  47708  ralbinrald  47721  rlimdmafv  47776  fafv2elrnb  47834  tz6.12c-afv2  47841  dfatbrafv2b  47844  fnbrafv2b  47847  rlimdmafv2  47857  f1oresf1o2  47890  el1fzopredsuc  47925  2ffzoeq  47927  nnmul2b  47930  modlt0b  47968  nndivides2  47983  imasetpreimafvbijlemfo  48016  iccpartiun  48045  ichnfb  48076  ich2exprop  48082  sprsymrelfolem2  48104  paireqne  48122  prprelprb  48128  reupr  48133  nprmmul2  48139  nprmmul3  48140  requad01  48248  requad1  48249  requad2  48250  dfodd6  48264  dfeven4  48265  evensumeven  48334  sbgoldbalt  48408  clnbgrel  48455  dfclnbgr6  48483  dfnbgr6  48484  isubgredg  48493  isuspgrim0  48521  isuspgrim  48523  gricushgr  48544  uhgrimisgrgriclem  48557  clnbgrgrim  48561  grimedg  48562  usgrgrtrirex  48577  uspgrlimlem2  48616  uspgrlim  48619  gpgedgiov  48692  gpgedg2ov  48693  gpgedg2iv  48694  gpgnbgrvtx0  48701  gpgnbgrvtx1  48702  isassintop  48837  uzlidlring  48862  rngcisoALTV  48904  ringcisoALTV  48938  domnmsuppn0  48996  lindslininds  49091  snlindsntor  49098  isldepslvec2  49112  affinecomb1  49329  prelrrx2b  49341  rrx2plord2  49349  eenglngeehlnm  49366  rrx2vlinest  49368  line2xlem  49380  line2x  49381  line2y  49382  itsclc0xyqsolb  49397  itsclquadb  49403  mpbiran3d  49423  opnneieqv  49537  iscnrm3lem2  49561  fullthinc2  50077  thincciso  50079