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  3464  rspcebdv  3559  rspceb2dv  3569  ceqex  3595  elabgtOLD  3616  mob2  3662  reu6  3673  sbciegftOLD  3767  sbcg  3802  2reu2  3837  csbiebt  3867  dfss2  3908  reupick  4270  reupick2  4272  uneqdifeq  4433  prnebg  4800  preqsnd  4803  prel12g  4808  iuneqconst  4946  disjeq2  5057  disjeq1  5060  disjss3  5085  reusv2lem2  5336  reusv2lem3  5337  alxfr  5344  ralxfrd  5345  ralxfrd2  5349  copsexgw  5438  copsexg  5439  snopeqop  5454  euotd  5461  poeq2  5536  sotric  5562  sotrieq  5563  freq2  5592  seeq1  5594  seeq2  5595  iss  5994  tz7.7  6343  ordtri1  6350  ordelinel  6420  funeq  6512  funssres  6536  f0dom0  6718  fnbrfvb  6884  ssimaex  6919  fvimacnv  6999  elpreima  7004  feldmfvelcdm  7032  eldmrexrnb  7038  fsn  7082  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fprb  7142  tpres  7149  fconst2g  7151  fconst5  7154  elunirn  7199  f1ocnvfvb  7227  f1prex  7232  foeqcnvco  7248  f1eqcocnv  7249  fliftfun  7260  soisores  7275  isofr  7290  isose  7291  isopo  7294  isoso  7296  f1oiso2  7300  eusvobj2  7352  oprabidw  7391  oprabid  7392  f1opw2  7615  oneqmin  7747  ordelsuc  7764  ordsucelsuc  7766  ordunisuc2  7788  limsuc  7793  fndmexb  7850  resf1ext2b  7879  f1ovv  7904  mptcnfimad  7932  op1steq  7979  opreuopreu  7980  funeldmdif  7994  fvn0elsuppb  8124  extmptsuppeq  8131  rntpos  8182  smoiso2  8302  seqomlem2  8383  oaord  8475  oawordex  8485  oaordex  8486  omord2  8495  om00  8503  oeord  8517  nnaord  8548  nnmord  8561  nnawordex  8566  nnaordex  8567  nnaordex2  8568  eldifsucnn  8593  erexb  8662  swoord1  8669  swoord2  8670  ecelqsdmb  8726  iiner  8729  eceqoveq  8762  mapsnd  8827  ralxpmap  8837  omxpenlem  9009  domtriord  9054  mapxpen  9074  mapunen  9077  ssenen  9082  enfi  9114  nneneq  9133  nndomog  9140  onomeneq  9141  en1eqsnbi  9179  fodomfib  9232  fodomfibOLD  9234  f1opwfi  9259  fsuppunbi  9295  elfiun  9336  suplub2  9367  ordiso2  9423  ordiso  9424  oieu  9447  brwdom2  9481  brwdom3  9490  cantnflem1  9601  ttrclselem2  9638  cardidm  9874  carddom2  9892  pm54.43  9916  acnen  9966  acnen2  9968  alephord  9988  alephinit  10008  dfac5  10042  infdif2  10122  fictb  10157  coflim  10174  fincssdom  10236  fin23lem25  10237  isf32lem9  10274  isf34lem4  10290  fin1a2lem11  10323  axdc3lem2  10364  ficard  10478  fpwwe2lem11  10555  fpwwe2  10557  indpi  10821  nqereq  10849  1idpr  10943  ltapr  10959  leltne  11226  ltlen  11238  ltadd2  11241  addlsub  11557  addid0  11560  ltord1  11667  mul0or  11781  ldiv  11980  ltmul1  11996  mulge0b  12017  lt2msq  12032  nnsub  12212  nn0sub  12478  zrevaddcl  12563  zltp1le  12568  zdiv  12590  nneo  12604  zeo2  12607  zmax  12886  zbtwnre  12887  qrevaddcl  12912  xrlttri  13081  xrleltne  13087  xralrple  13148  xltneg  13160  xleadd1  13198  xlemul1  13233  supxrunb1  13262  supxrunb2  13263  ioo0  13314  iccid  13334  ico0  13335  ioc0  13336  icc0  13337  difreicc  13428  iccsplit  13429  zltaddlt1le  13449  0fz1  13489  uzsplit  13541  fzm1  13552  fzrevral  13557  ssfzo12bi  13707  elfznelfzob  13720  flge  13755  modid2  13848  modmuladd  13866  ssnn0fi  13938  seqf1olem1  13994  hashen  14300  hashdom  14332  hash2exprb  14424  pr2pwpr  14432  hashtpg  14438  hash3tpexb  14447  len0nnbi  14504  ccats1pfxeqbi  14695  reuccatpfxs1  14700  repsdf2  14731  scshwfzeqfzo  14779  relexpindlem  15016  shftlem  15021  shftuz  15022  abslt  15268  absle  15269  rexico  15307  cau3lem  15308  reusq0  15418  rlim2lt  15450  rlim3  15451  o1lo1  15490  rlimdm  15504  climshft  15529  o1dif  15583  isercolllem2  15619  isercoll  15621  zsum  15671  fsum  15673  fsum00  15752  incexclem  15792  zprod  15893  fprod  15897  dvdsval2  16215  moddvds  16223  negdvdsb  16232  dvdsnegb  16233  dvdscmulr  16244  dvdsmulcr  16245  dvdssub2  16261  dvdsaddre2b  16267  fzo0dvdseq  16283  mod2eq1n2dvds  16307  ltoddhalfle  16321  sumodd  16348  bitsf1ocnv  16404  sadcaddlem  16417  bitsuz  16434  dvdsgcdb  16505  gcdzeq  16512  dvdssqlem  16526  lcmeq0  16560  lcmdvdsb  16573  lcmfeq0b  16590  lcmf  16593  lcmfdvdsb  16603  coprmgcdb  16609  cncongr  16629  isprm2lem  16641  dvdsprime  16647  dvdsprm  16664  isprm7  16669  coprm  16672  euclemma  16674  rpexp  16683  prmdvdsncoprmbd  16688  prmdiveq  16747  hashgcdlem  16749  odzdvds  16757  pythagtrip  16796  pc2dvds  16841  pcprmpw2  16844  pcprmpw  16845  vdwapun  16936  ramtcl2  16973  firest  17386  mrieqv2d  17596  isacs2  17610  isssc  17778  setciso  18049  posasymb  18276  pleval2  18292  pltval3  18294  lublecllem  18315  joinle  18341  meetle  18355  latdisd  18454  lubun  18472  clatleglb  18475  letsr  18550  intopsn  18613  gsumval2a  18644  frmdss2  18822  isgrpid2  18943  isgrpinv  18960  f1ghm0to0  19211  symg1bas  19357  oddvdsnn0  19510  oddvds  19513  odeq  19516  odeq1  19526  gexdvds  19550  pgpfi  19571  pgpssslw  19580  fislw  19591  sylow3lem2  19594  lsmelvalm  19617  lsmlub  19630  lsmss1b  19632  lsmss2b  19634  efgs1b  19702  cyggenod  19850  cyggexb  19865  dprdfeq0  19990  ablsimpgfind  20078  ringinvnz1ne0  20272  ringinvnzdiv  20273  unitmulclb  20352  dvreq1  20382  isnzr2  20486  0ringnnzr  20493  0ring01eqbi  20500  rngciso  20606  ringciso  20640  rrgeq0  20668  domneq0  20676  drngmul0orOLD  20729  isabvd  20780  issrngd  20823  lssats2  20986  lspsneq0  20998  lsmelval2  21072  lvecvs0or  21098  lspsneq  21112  lspsneu  21113  lidl1el  21216  lidldvgen  21324  pzriprnglem10  21480  pzriprnglem11  21481  znunit  21553  psgndif  21592  ipeq0  21628  ocvsscon  21665  pjdm2  21701  obselocv  21718  islinds4  21825  psdmul  22142  ply1coe1eq  22275  cply1coe0bi  22277  mat1dimelbas  22446  cramer  22666  toponcomb  22904  tgss3  22961  clsval2  23025  isopn3  23041  elcls3  23058  opncldf1  23059  neiint  23079  neips  23088  opnneissb  23089  opnssneib  23090  opnnei  23095  tpnei  23096  opnneiid  23101  restcld  23147  restopnb  23150  tgcn  23227  tgcnp  23228  subbascn  23229  iscnp4  23238  cnpnei  23239  cncls2  23248  cncls  23249  cnntr  23250  lmss  23273  hausnei2  23328  lpcls  23339  ordtt1  23354  cmpsub  23375  tgcmp  23376  1stcelcls  23436  locfincmp  23501  kgencn2  23532  ptpjpre1  23546  upxp  23598  txcn  23601  txlm  23623  tgqtop  23687  kqfvima  23705  isr0  23712  regr1lem2  23715  hmeoopn  23741  hmeocld  23742  ptuncnv  23782  fbunfip  23844  fgss2  23849  ufilb  23881  ufprim  23884  trufil  23885  cfinufil  23903  ufildr  23906  elfm2  23923  elfm3  23925  rnelfm  23928  fmfnfmlem4  23932  fmco  23936  flimtopon  23945  flimopn  23950  fbflim2  23952  flimrest  23958  flffbas  23970  cnpflf  23976  fclstopon  23987  fclsnei  23994  fclsbas  23996  fclsfnflim  24002  fclscmp  24005  ufilcmp  24007  isfcf  24009  fcfnei  24010  cnpfcf  24016  alexsubb  24021  alexsubALT  24026  cldsubg  24086  tgphaus  24092  tgpt0  24094  tsmsgsum  24114  tsmsres  24119  xbln0  24389  blssexps  24401  blssex  24402  isxms2  24423  prdsbl  24466  neibl  24476  metss  24483  met2ndc  24498  metrest  24499  metcnp3  24515  tngngp3  24631  nmoeq0  24711  xrsxmet  24785  reconn  24804  iccpnfcnv  24921  fgcfil  25248  iscau4  25256  cfilres  25273  iunmbl2  25534  ismbf3d  25631  mbfaddlem  25637  i1faddlem  25670  i1fmullem  25671  ellimc3  25856  dvfsumlem2  26004  tdeglem4  26035  deg1nn0clb  26065  deg1lt0  26066  dvdsq1p  26138  plypf1  26187  0dgrb  26221  plymul0or  26257  taylthlem2  26351  ulmshft  26368  ulmcaulem  26372  ulmcau  26373  cosord  26508  eff1olem  26525  lognegb  26567  eflogeq  26579  logdivlt  26598  efopn  26635  cxpeq0  26655  cxpeq  26734  angpieqvd  26808  dcubic  26823  asinsinb  26874  acoscosb  26875  atantanb  26901  rlimcnp  26942  isppw  27091  isppw2  27092  vmappw  27093  isnsqf  27112  ppieq0  27153  fsumdvdsdiag  27161  dvdsppwf1o  27163  fsumfldivdiag  27167  chpeq0  27185  chteq0  27186  dchrptlem1  27241  lgsdir2lem4  27305  lgsne0  27312  lgsqr  27328  lgsdchrval  27331  gausslemma2dlem1a  27342  lgsquadlem1  27357  m1lgs  27365  2sqreultblem  27425  2sqreunnltblem  27428  nodenselem8  27669  ltlesnd  27753  oldlim  27893  ltslpss  27914  leadds1  27995  ltnegs  28051  negleft  28064  negright  28065  muls0ord  28191  abslts  28255  onlts  28273  n0subs  28369  n0ltsp1le  28371  z12sge0  28489  iscgrglt  28596  brbtwn  28982  brcgr  28983  brbtwn2  28988  axcontlem7  29053  uhgr0vb  29155  edglnl  29226  ausgrusgrb  29248  ushgredgedg  29312  ushgredgedgloop  29314  usgr0vb  29320  usgr1v  29339  nbupgr  29427  nbumgrvtx  29429  nbuhgr2vtx1edgb  29435  edgusgrnbfin  29456  nb3grprlem1  29463  uvtxnbvtxm1  29489  cusgrfilem2  29540  uhgr0edg0rgrb  29658  cusgrm1rusgr  29666  spthonepeq  29835  usgr2pth  29847  wlkiswwlks  29959  wlkiswwlkupgr  29961  wlklnwwlkn  29967  wlklnwwlknupgr  29969  wwlksnextbi  29977  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  wwlksnextprop  29995  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2on  30045  elwspths2onw  30046  usgr2wspthons3  30050  elwwlks2  30052  elwspths2spth  30053  clwlkclwwlklem3  30086  loopclwwlkn1b  30127  clwwlknon1sn  30185  clwwlknonwwlknonb  30191  umgr3v3e3cycl  30269  eupth2lem3lem4  30316  frgr0v  30347  frgr3vlem2  30359  2clwwlk2clwwlk  30435  wlkl0  30452  grpoinvf  30618  nvmul0or  30736  nvz  30755  diporthcom  30802  ubthlem3  30958  hvmul0or  31111  his6  31185  hial0  31188  hial02  31189  orthcom  31194  normgt0  31213  ocin  31382  occon3  31383  shsel3  31401  shlub  31500  chssoc  31582  h1de2bi  31640  spansncol  31654  elspansn4  31659  spansnss2  31661  sumspansn  31735  lnopcnbd  32122  lnfncnbd  32143  riesz1  32151  elpjrn  32276  cvcon3  32370  dmdmd  32386  dmdbr3  32391  dmdbr4  32392  dmdbr5  32394  mdslmd1i  32415  atcveq0  32434  chcv1  32441  atssma  32464  atcv0eq  32465  atcv1  32466  bian1dOLD  32541  disjeq1f  32658  br8d  32696  fpwrelmap  32821  xaddeq0  32841  eliccelico  32865  elicoelioo  32866  indf1ofs  32941  isarchiofld  33275  unitdivcld  34061  xrge0iifcnv  34093  lmxrge0  34112  eulerpartlemgh  34538  dstfrvunirn  34635  fnrelpredd  35250  rankfilimb  35261  fineqvnttrclse  35284  loop1cycl  35335  cusgracyclt3v  35354  cvmliftmolem2  35480  cvmlift2lem12  35512  satfvsucsuc  35563  satfdm  35567  fmlasuc  35584  satffunlem1lem2  35601  satffunlem2lem2  35604  mthmb  35779  climuzcnv  35869  br8  35954  br6  35955  br4  35956  funbreq  35968  axextbdist  35996  dfrdg4  36149  cgrcom  36188  cgrcoml  36194  cgrdegen  36202  btwncom  36212  brsegle  36306  brsegle2  36307  colinbtwnle  36316  btwnoutside  36323  broutsideof3  36324  outsidele  36330  lineunray  36345  lineelsb2  36346  elhf2  36373  elicc3  36515  nn0prpwlem  36520  opnbnd  36523  cldbnd  36524  opnregcld  36528  cldregopn  36529  fnessref  36555  refssfne  36556  neibastop2  36559  fnemeet2  36565  fnejoin2  36567  fgmin  36568  ontgval  36629  ordtop  36634  ordcmp  36645  nndivsub  36655  bj-cbval  36956  bj-cbvex  36957  bj-19.21t  37074  bj-19.23t  37075  bj-19.42t  37078  bj-sbft  37091  bj-nnf-cbval  37093  bj-cbv2hv  37120  bj-equsal1t  37145  bj-19.21t0  37153  bj-ceqsalt0  37207  bj-ceqsalt1  37208  bj-xpnzexb  37284  bj-axreprepsep  37398  cgsex2gd  37467  bj-idreseq  37492  bj-imdiridlem  37515  bj-finsumval0  37615  bj-fvimacnv0  37616  bj-isrvec2  37630  bj-bary1  37642  dfgcd3  37654  isbasisrelowllem1  37685  isbasisrelowllem2  37686  finxpsuclem  37727  wl-lem-exsb  37905  wl-mo3t  37915  matunitlindf  37953  poimirlem6  37961  poimirlem7  37962  poimirlem16  37971  poimirlem19  37974  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  cnambfre  38003  itg2addnc  38009  brabg2  38052  istotbnd3  38106  sstotbnd2  38109  sstotbnd  38110  sstotbnd3  38111  ssbnd  38123  ismtybnd  38142  reheibor  38174  grpoeqdivid  38216  grpokerinj  38228  rngosn3  38259  rngoueqz  38275  1idl  38361  0rngo  38362  divrngidl  38363  igenval2  38401  ispridlc  38405  isdmn3  38409  relcnveq3  38662  iss2  38679  elrelscnveq3  38962  funALTVeq  39120  disjeq  39169  prtlem10  39325  prter2  39341  dral1-o  39364  lshpinN  39449  lsatcveq0  39492  lsatcv0eq  39507  lsatcv1  39508  islshpcv  39513  lkr0f  39554  lkrshp4  39568  lshpkrlem1  39570  lshpset2N  39579  lfl1dim  39581  lfl1dim2N  39582  lub0N  39649  glb0N  39653  oplecon3b  39660  cmtcomN  39709  cmtbr3N  39714  cmtbr4N  39715  cvrnbtwn2  39735  cvrnbtwn3  39736  cvrcon3b  39737  cvrnbtwn4  39739  cvrcmp  39743  atcvreq0  39774  atnle  39777  atlatle  39780  cvlexchb1  39790  cvlcvr1  39799  hlrelat2  39863  exatleN  39864  cvrval3  39873  cvrval4N  39874  cvrexch  39880  atcvr0eq  39886  lnnat  39887  atcvrj0  39888  atcvrj2b  39892  atltcvr  39895  atbtwn  39906  ps-1  39937  3at  39950  islln2a  39977  llncmp  39982  islpln2a  40008  lplncmp  40022  islvol2aN  40052  4at  40073  lvolcmp  40077  pmaple  40221  lncmp  40243  paddss  40305  llnexchb2lem  40328  2polcon4bN  40378  ispsubcl2N  40407  lhpat3  40506  lautcvr  40552  ltrnid  40595  trlval2  40623  trlatn0  40632  ltrnideq  40635  trlnidatb  40637  cdlemeg49lebilem  40999  trlord  41029  cdlemg1a  41030  cdlemg1cex  41048  tendoid0  41285  dva1dim  41445  cdlemm10N  41578  diarnN  41589  cdlemn  41672  dihlspsnssN  41792  dihatexv  41798  dochkrshp  41846  dochkrshp4  41849  djhlsmcl  41874  lcfl6  41960  lcfl8  41962  lcfrvalsnN  42001  lcfrlem9  42010  mapdval2N  42090  mapdordlem2  42097  mapd1o  42108  mapd0  42125  mapdheq2biN  42190  nnproddivdvdsd  42453  primrootspoweq0  42559  aks6d1c1p1  42560  aks6d1c5lem1  42589  sticksstones11  42609  sticksstones22  42621  grpods  42647  unitscyglem2  42649  eqresfnbd  42687  expeq1d  42770  expeqidd  42771  dvdsexpnn  42779  zdivgd  42783  sn-remul0ord  42854  mulgt0b1d  42931  frlmfzowrdb  42963  frlmsnic  42999  evlselvlem  43033  prjspreln0  43056  elrfi  43140  diophrw  43205  eldioph2b  43209  diophin  43218  rexrabdioph  43240  rmxycomplete  43363  coprmdvdsb  43431  jm2.19  43439  jm2.26  43448  jm2.27  43454  limsuc2  43487  dgraa0p  43595  rngunsnply  43615  fiuneneq  43638  unielss  43664  oaabsb  43740  nnoeomeqom  43758  cantnfresb  43770  tfsconcatrn  43788  tfsconcat0b  43792  tfsconcatrev  43794  oadif1lem  43825  oadif1  43826  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  pwelg  44005  nzss  44762  dvconstbi  44779  expgrowth  44780  bcc0  44785  axc11next  44851  pm14.24  44877  sbiota1  44879  sbcim2g  44983  sineq0ALT  45381  mapss2  45652  fsneq  45653  fsneqrn  45658  mapssbi  45660  rnmptbd2lem  45695  infnsuprnmpt  45697  rnmptbdlem  45702  xralrple2  45802  infxrunb2  45815  xralrple4  45820  xralrple3  45821  xrralrecnnle  45830  xrralrecnnge  45837  reclt0  45838  supxrunb3  45846  supxrleubrnmpt  45852  xrre4  45857  unb2ltle  45861  rexabslelem  45864  suprleubrnmpt  45868  infxrunb3rnmpt  45874  uzub  45877  supminfrnmpt  45891  iccintsng  45971  sqrlearg  46001  uzinico  46007  preimaiocmnf  46008  limcresiooub  46088  limclr  46101  climeldmeq  46111  limsuppnflem  46156  limsupmnflem  46166  limsupmnfuzlem  46172  limsupre3lem  46178  limsupre3uzlem  46181  liminfreuzlem  46248  dvnmul  46389  dvmptfprodlem  46390  ismbl3  46432  ismbl4  46439  fourierdlem50  46602  fourierdlem89  46641  fourierdlem91  46643  dfsalgen2  46787  sge0repnf  46832  sge0lefi  46844  sge0resplit  46852  sge0fodjrnlem  46862  voliunsge0lem  46918  hspdifhsp  47062  isvonmbl  47084  ovnovollem3  47104  vonvolmbl  47107  pimrecltpos  47154  preimaicomnf  47157  pimrecltneg  47170  issmflem  47173  issmfle  47191  issmfgt  47202  smfaddlem1  47209  issmfge  47216  smfresal  47234  smflimmpt  47256  smfinflem  47263  smflimsuplem7  47272  smflimsupmpt  47275  sigarcol  47310  confun  47399  or2expropbi  47494  fsetsniunop  47509  fcoresf1b  47530  f1cof1b  47537  funfocofob  47538  rexsb  47559  euoreqb  47569  ralbinrald  47582  rlimdmafv  47637  fafv2elrnb  47695  tz6.12c-afv2  47702  dfatbrafv2b  47705  fnbrafv2b  47708  rlimdmafv2  47718  f1oresf1o2  47751  el1fzopredsuc  47786  2ffzoeq  47788  nnmul2b  47791  modlt0b  47829  nndivides2  47844  imasetpreimafvbijlemfo  47877  iccpartiun  47906  ichnfb  47937  ich2exprop  47943  sprsymrelfolem2  47965  paireqne  47983  prprelprb  47989  reupr  47994  nprmmul2  48000  nprmmul3  48001  requad01  48109  requad1  48110  requad2  48111  dfodd6  48125  dfeven4  48126  evensumeven  48195  sbgoldbalt  48269  clnbgrel  48316  dfclnbgr6  48344  dfnbgr6  48345  isubgredg  48354  isuspgrim0  48382  isuspgrim  48384  gricushgr  48405  uhgrimisgrgriclem  48418  clnbgrgrim  48422  grimedg  48423  usgrgrtrirex  48438  uspgrlimlem2  48477  uspgrlim  48480  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  isassintop  48698  uzlidlring  48723  rngcisoALTV  48765  ringcisoALTV  48799  domnmsuppn0  48857  lindslininds  48952  snlindsntor  48959  isldepslvec2  48973  affinecomb1  49190  prelrrx2b  49202  rrx2plord2  49210  eenglngeehlnm  49227  rrx2vlinest  49229  line2xlem  49241  line2x  49242  line2y  49243  itsclc0xyqsolb  49258  itsclquadb  49264  mpbiran3d  49284  opnneieqv  49398  iscnrm3lem2  49422  fullthinc2  49938  thincciso  49940