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  2341  exsb  2363  dral1v  2373  cbv2  2407  cbv2h  2410  ax12b  2428  dral1  2443  dral1ALT  2444  eupickb  2635  eupickbi  2636  2eu2  2653  ralbi  3092  rexbi  3093  ralbida  3248  ceqsalt  3463  rspcebdv  3558  rspceb2dv  3568  ceqex  3594  elabgtOLD  3615  mob2  3661  reu6  3672  sbciegftOLD  3766  sbcg  3801  2reu2  3836  csbiebt  3866  dfss2  3907  reupick  4269  reupick2  4271  uneqdifeq  4432  prnebg  4799  preqsnd  4802  prel12g  4807  iuneqconst  4945  disjeq2  5056  disjeq1  5059  disjss3  5084  reusv2lem2  5341  reusv2lem3  5342  alxfr  5349  ralxfrd  5350  ralxfrd2  5354  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  snopeqop  5460  euotd  5467  poeq2  5543  sotric  5569  sotrieq  5570  freq2  5599  seeq1  5601  seeq2  5602  iss  6000  tz7.7  6349  ordtri1  6356  ordelinel  6426  funeq  6518  funssres  6542  f0dom0  6724  fnbrfvb  6890  ssimaex  6925  fvimacnv  7005  elpreima  7010  feldmfvelcdm  7038  eldmrexrnb  7044  fsn  7088  fnsnbg  7119  fnsnbOLD  7121  fmptsng  7123  fmptsnd  7124  fprb  7149  tpres  7156  fconst2g  7158  fconst5  7161  elunirn  7206  f1ocnvfvb  7234  f1prex  7239  foeqcnvco  7255  f1eqcocnv  7256  fliftfun  7267  soisores  7282  isofr  7297  isose  7298  isopo  7301  isoso  7303  f1oiso2  7307  eusvobj2  7359  oprabidw  7398  oprabid  7399  f1opw2  7622  oneqmin  7754  ordelsuc  7771  ordsucelsuc  7773  ordunisuc2  7795  limsuc  7800  fndmexb  7857  resf1ext2b  7886  f1ovv  7911  mptcnfimad  7939  op1steq  7986  opreuopreu  7987  funeldmdif  8001  fvn0elsuppb  8131  extmptsuppeq  8138  rntpos  8189  smoiso2  8309  seqomlem2  8390  oaord  8482  oawordex  8492  oaordex  8493  omord2  8502  om00  8510  oeord  8524  nnaord  8555  nnmord  8568  nnawordex  8573  nnaordex  8574  nnaordex2  8575  eldifsucnn  8600  erexb  8669  swoord1  8676  swoord2  8677  ecelqsdmb  8733  iiner  8736  eceqoveq  8769  mapsnd  8834  ralxpmap  8844  omxpenlem  9016  domtriord  9061  mapxpen  9081  mapunen  9084  ssenen  9089  enfi  9121  nneneq  9140  nndomog  9147  onomeneq  9148  en1eqsnbi  9186  fodomfib  9239  fodomfibOLD  9241  f1opwfi  9266  fsuppunbi  9302  elfiun  9343  suplub2  9374  ordiso2  9430  ordiso  9431  oieu  9454  brwdom2  9488  brwdom3  9497  cantnflem1  9610  ttrclselem2  9647  cardidm  9883  carddom2  9901  pm54.43  9925  acnen  9975  acnen2  9977  alephord  9997  alephinit  10017  dfac5  10051  infdif2  10131  fictb  10166  coflim  10183  fincssdom  10245  fin23lem25  10246  isf32lem9  10283  isf34lem4  10299  fin1a2lem11  10332  axdc3lem2  10373  ficard  10487  fpwwe2lem11  10564  fpwwe2  10566  indpi  10830  nqereq  10858  1idpr  10952  ltapr  10968  leltne  11235  ltlen  11247  ltadd2  11250  addlsub  11566  addid0  11569  ltord1  11676  mul0or  11790  ldiv  11989  ltmul1  12005  mulge0b  12026  lt2msq  12041  nnsub  12221  nn0sub  12487  zrevaddcl  12572  zltp1le  12577  zdiv  12599  nneo  12613  zeo2  12616  zmax  12895  zbtwnre  12896  qrevaddcl  12921  xrlttri  13090  xrleltne  13096  xralrple  13157  xltneg  13169  xleadd1  13207  xlemul1  13242  supxrunb1  13271  supxrunb2  13272  ioo0  13323  iccid  13343  ico0  13344  ioc0  13345  icc0  13346  difreicc  13437  iccsplit  13438  zltaddlt1le  13458  0fz1  13498  uzsplit  13550  fzm1  13561  fzrevral  13566  ssfzo12bi  13716  elfznelfzob  13729  flge  13764  modid2  13857  modmuladd  13875  ssnn0fi  13947  seqf1olem1  14003  hashen  14309  hashdom  14341  hash2exprb  14433  pr2pwpr  14441  hashtpg  14447  hash3tpexb  14456  len0nnbi  14513  ccats1pfxeqbi  14704  reuccatpfxs1  14709  repsdf2  14740  scshwfzeqfzo  14788  relexpindlem  15025  shftlem  15030  shftuz  15031  abslt  15277  absle  15278  rexico  15316  cau3lem  15317  reusq0  15427  rlim2lt  15459  rlim3  15460  o1lo1  15499  rlimdm  15513  climshft  15538  o1dif  15592  isercolllem2  15628  isercoll  15630  zsum  15680  fsum  15682  fsum00  15761  incexclem  15801  zprod  15902  fprod  15906  dvdsval2  16224  moddvds  16232  negdvdsb  16241  dvdsnegb  16242  dvdscmulr  16253  dvdsmulcr  16254  dvdssub2  16270  dvdsaddre2b  16276  fzo0dvdseq  16292  mod2eq1n2dvds  16316  ltoddhalfle  16330  sumodd  16357  bitsf1ocnv  16413  sadcaddlem  16426  bitsuz  16443  dvdsgcdb  16514  gcdzeq  16521  dvdssqlem  16535  lcmeq0  16569  lcmdvdsb  16582  lcmfeq0b  16599  lcmf  16602  lcmfdvdsb  16612  coprmgcdb  16618  cncongr  16638  isprm2lem  16650  dvdsprime  16656  dvdsprm  16673  isprm7  16678  coprm  16681  euclemma  16683  rpexp  16692  prmdvdsncoprmbd  16697  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  pythagtrip  16805  pc2dvds  16850  pcprmpw2  16853  pcprmpw  16854  vdwapun  16945  ramtcl2  16982  firest  17395  mrieqv2d  17605  isacs2  17619  isssc  17787  setciso  18058  posasymb  18285  pleval2  18301  pltval3  18303  lublecllem  18324  joinle  18350  meetle  18364  latdisd  18463  lubun  18481  clatleglb  18484  letsr  18559  intopsn  18622  gsumval2a  18653  frmdss2  18831  isgrpid2  18952  isgrpinv  18969  f1ghm0to0  19220  symg1bas  19366  oddvdsnn0  19519  oddvds  19522  odeq  19525  odeq1  19535  gexdvds  19559  pgpfi  19580  pgpssslw  19589  fislw  19600  sylow3lem2  19603  lsmelvalm  19626  lsmlub  19639  lsmss1b  19641  lsmss2b  19643  efgs1b  19711  cyggenod  19859  cyggexb  19874  dprdfeq0  19999  ablsimpgfind  20087  ringinvnz1ne0  20281  ringinvnzdiv  20282  unitmulclb  20361  dvreq1  20391  isnzr2  20495  0ringnnzr  20502  0ring01eqbi  20509  rngciso  20615  ringciso  20649  rrgeq0  20677  domneq0  20685  drngmul0orOLD  20738  isabvd  20789  issrngd  20832  lssats2  20995  lspsneq0  21007  lsmelval2  21080  lvecvs0or  21106  lspsneq  21120  lspsneu  21121  lidl1el  21224  lidldvgen  21332  pzriprnglem10  21470  pzriprnglem11  21471  znunit  21543  psgndif  21582  ipeq0  21618  ocvsscon  21655  pjdm2  21691  obselocv  21708  islinds4  21815  psdmul  22132  ply1coe1eq  22265  cply1coe0bi  22267  mat1dimelbas  22436  cramer  22656  toponcomb  22894  tgss3  22951  clsval2  23015  isopn3  23031  elcls3  23048  opncldf1  23049  neiint  23069  neips  23078  opnneissb  23079  opnssneib  23080  opnnei  23085  tpnei  23086  opnneiid  23091  restcld  23137  restopnb  23140  tgcn  23217  tgcnp  23218  subbascn  23219  iscnp4  23228  cnpnei  23229  cncls2  23238  cncls  23239  cnntr  23240  lmss  23263  hausnei2  23318  lpcls  23329  ordtt1  23344  cmpsub  23365  tgcmp  23366  1stcelcls  23426  locfincmp  23491  kgencn2  23522  ptpjpre1  23536  upxp  23588  txcn  23591  txlm  23613  tgqtop  23677  kqfvima  23695  isr0  23702  regr1lem2  23705  hmeoopn  23731  hmeocld  23732  ptuncnv  23772  fbunfip  23834  fgss2  23839  ufilb  23871  ufprim  23874  trufil  23875  cfinufil  23893  ufildr  23896  elfm2  23913  elfm3  23915  rnelfm  23918  fmfnfmlem4  23922  fmco  23926  flimtopon  23935  flimopn  23940  fbflim2  23942  flimrest  23948  flffbas  23960  cnpflf  23966  fclstopon  23977  fclsnei  23984  fclsbas  23986  fclsfnflim  23992  fclscmp  23995  ufilcmp  23997  isfcf  23999  fcfnei  24000  cnpfcf  24006  alexsubb  24011  alexsubALT  24016  cldsubg  24076  tgphaus  24082  tgpt0  24084  tsmsgsum  24104  tsmsres  24109  xbln0  24379  blssexps  24391  blssex  24392  isxms2  24413  prdsbl  24456  neibl  24466  metss  24473  met2ndc  24488  metrest  24489  metcnp3  24505  tngngp3  24621  nmoeq0  24701  xrsxmet  24775  reconn  24794  iccpnfcnv  24911  fgcfil  25238  iscau4  25246  cfilres  25263  iunmbl2  25524  ismbf3d  25621  mbfaddlem  25627  i1faddlem  25660  i1fmullem  25661  ellimc3  25846  dvfsumlem2  25994  tdeglem4  26025  deg1nn0clb  26055  deg1lt0  26056  dvdsq1p  26128  plypf1  26177  0dgrb  26211  plymul0or  26247  taylthlem2  26339  ulmshft  26355  ulmcaulem  26359  ulmcau  26360  cosord  26495  eff1olem  26512  lognegb  26554  eflogeq  26566  logdivlt  26585  efopn  26622  cxpeq0  26642  cxpeq  26721  angpieqvd  26795  dcubic  26810  asinsinb  26861  acoscosb  26862  atantanb  26888  rlimcnp  26929  isppw  27077  isppw2  27078  vmappw  27079  isnsqf  27098  ppieq0  27139  fsumdvdsdiag  27147  dvdsppwf1o  27149  fsumfldivdiag  27153  chpeq0  27171  chteq0  27172  dchrptlem1  27227  lgsdir2lem4  27291  lgsne0  27298  lgsqr  27314  lgsdchrval  27317  gausslemma2dlem1a  27328  lgsquadlem1  27343  m1lgs  27351  2sqreultblem  27411  2sqreunnltblem  27414  nodenselem8  27655  ltlesnd  27739  oldlim  27879  ltslpss  27900  leadds1  27981  ltnegs  28037  negleft  28050  negright  28051  muls0ord  28177  abslts  28241  onlts  28259  n0subs  28355  n0ltsp1le  28357  z12sge0  28475  iscgrglt  28582  brbtwn  28968  brcgr  28969  brbtwn2  28974  axcontlem7  29039  uhgr0vb  29141  edglnl  29212  ausgrusgrb  29234  ushgredgedg  29298  ushgredgedgloop  29300  usgr0vb  29306  usgr1v  29325  nbupgr  29413  nbumgrvtx  29415  nbuhgr2vtx1edgb  29421  edgusgrnbfin  29442  nb3grprlem1  29449  uvtxnbvtxm1  29475  cusgrfilem2  29525  uhgr0edg0rgrb  29643  cusgrm1rusgr  29651  spthonepeq  29820  usgr2pth  29832  wlkiswwlks  29944  wlkiswwlkupgr  29946  wlklnwwlkn  29952  wlklnwwlknupgr  29954  wwlksnextbi  29962  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  wwlksnextprop  29980  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2on  30030  elwspths2onw  30031  usgr2wspthons3  30035  elwwlks2  30037  elwspths2spth  30038  clwlkclwwlklem3  30071  loopclwwlkn1b  30112  clwwlknon1sn  30170  clwwlknonwwlknonb  30176  umgr3v3e3cycl  30254  eupth2lem3lem4  30301  frgr0v  30332  frgr3vlem2  30344  2clwwlk2clwwlk  30420  wlkl0  30437  grpoinvf  30603  nvmul0or  30721  nvz  30740  diporthcom  30787  ubthlem3  30943  hvmul0or  31096  his6  31170  hial0  31173  hial02  31174  orthcom  31179  normgt0  31198  ocin  31367  occon3  31368  shsel3  31386  shlub  31485  chssoc  31567  h1de2bi  31625  spansncol  31639  elspansn4  31644  spansnss2  31646  sumspansn  31720  lnopcnbd  32107  lnfncnbd  32128  riesz1  32136  elpjrn  32261  cvcon3  32355  dmdmd  32371  dmdbr3  32376  dmdbr4  32377  dmdbr5  32379  mdslmd1i  32400  atcveq0  32419  chcv1  32426  atssma  32449  atcv0eq  32450  atcv1  32451  bian1dOLD  32526  disjeq1f  32643  br8d  32681  fpwrelmap  32806  xaddeq0  32826  eliccelico  32850  elicoelioo  32851  indf1ofs  32926  isarchiofld  33260  unitdivcld  34045  xrge0iifcnv  34077  lmxrge0  34096  eulerpartlemgh  34522  dstfrvunirn  34619  fnrelpredd  35234  rankfilimb  35245  fineqvnttrclse  35268  loop1cycl  35319  cusgracyclt3v  35338  cvmliftmolem2  35464  cvmlift2lem12  35496  satfvsucsuc  35547  satfdm  35551  fmlasuc  35568  satffunlem1lem2  35585  satffunlem2lem2  35588  mthmb  35763  climuzcnv  35853  br8  35938  br6  35939  br4  35940  funbreq  35952  axextbdist  35980  dfrdg4  36133  cgrcom  36172  cgrcoml  36178  cgrdegen  36186  btwncom  36196  brsegle  36290  brsegle2  36291  colinbtwnle  36300  btwnoutside  36307  broutsideof3  36308  outsidele  36314  lineunray  36329  lineelsb2  36330  elhf2  36357  elicc3  36499  nn0prpwlem  36504  opnbnd  36507  cldbnd  36508  opnregcld  36512  cldregopn  36513  fnessref  36539  refssfne  36540  neibastop2  36543  fnemeet2  36549  fnejoin2  36551  fgmin  36552  ontgval  36613  ordtop  36618  ordcmp  36629  nndivsub  36639  bj-cbval  36940  bj-cbvex  36941  bj-19.21t  37058  bj-19.23t  37059  bj-19.42t  37062  bj-sbft  37075  bj-nnf-cbval  37077  bj-cbv2hv  37104  bj-equsal1t  37129  bj-19.21t0  37137  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-xpnzexb  37268  bj-axreprepsep  37382  cgsex2gd  37451  bj-idreseq  37476  bj-imdiridlem  37499  bj-finsumval0  37599  bj-fvimacnv0  37600  bj-isrvec2  37614  bj-bary1  37626  dfgcd3  37638  isbasisrelowllem1  37671  isbasisrelowllem2  37672  finxpsuclem  37713  wl-lem-exsb  37891  wl-mo3t  37901  matunitlindf  37939  poimirlem6  37947  poimirlem7  37948  poimirlem16  37957  poimirlem19  37960  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  cnambfre  37989  itg2addnc  37995  brabg2  38038  istotbnd3  38092  sstotbnd2  38095  sstotbnd  38096  sstotbnd3  38097  ssbnd  38109  ismtybnd  38128  reheibor  38160  grpoeqdivid  38202  grpokerinj  38214  rngosn3  38245  rngoueqz  38261  1idl  38347  0rngo  38348  divrngidl  38349  igenval2  38387  ispridlc  38391  isdmn3  38395  relcnveq3  38648  iss2  38665  elrelscnveq3  38948  funALTVeq  39106  disjeq  39155  prtlem10  39311  prter2  39327  dral1-o  39350  lshpinN  39435  lsatcveq0  39478  lsatcv0eq  39493  lsatcv1  39494  islshpcv  39499  lkr0f  39540  lkrshp4  39554  lshpkrlem1  39556  lshpset2N  39565  lfl1dim  39567  lfl1dim2N  39568  lub0N  39635  glb0N  39639  oplecon3b  39646  cmtcomN  39695  cmtbr3N  39700  cmtbr4N  39701  cvrnbtwn2  39721  cvrnbtwn3  39722  cvrcon3b  39723  cvrnbtwn4  39725  cvrcmp  39729  atcvreq0  39760  atnle  39763  atlatle  39766  cvlexchb1  39776  cvlcvr1  39785  hlrelat2  39849  exatleN  39850  cvrval3  39859  cvrval4N  39860  cvrexch  39866  atcvr0eq  39872  lnnat  39873  atcvrj0  39874  atcvrj2b  39878  atltcvr  39881  atbtwn  39892  ps-1  39923  3at  39936  islln2a  39963  llncmp  39968  islpln2a  39994  lplncmp  40008  islvol2aN  40038  4at  40059  lvolcmp  40063  pmaple  40207  lncmp  40229  paddss  40291  llnexchb2lem  40314  2polcon4bN  40364  ispsubcl2N  40393  lhpat3  40492  lautcvr  40538  ltrnid  40581  trlval2  40609  trlatn0  40618  ltrnideq  40621  trlnidatb  40623  cdlemeg49lebilem  40985  trlord  41015  cdlemg1a  41016  cdlemg1cex  41034  tendoid0  41271  dva1dim  41431  cdlemm10N  41564  diarnN  41575  cdlemn  41658  dihlspsnssN  41778  dihatexv  41784  dochkrshp  41832  dochkrshp4  41835  djhlsmcl  41860  lcfl6  41946  lcfl8  41948  lcfrvalsnN  41987  lcfrlem9  41996  mapdval2N  42076  mapdordlem2  42083  mapd1o  42094  mapd0  42111  mapdheq2biN  42176  nnproddivdvdsd  42439  primrootspoweq0  42545  aks6d1c1p1  42546  aks6d1c5lem1  42575  sticksstones11  42595  sticksstones22  42607  grpods  42633  unitscyglem2  42635  eqresfnbd  42673  expeq1d  42756  expeqidd  42757  dvdsexpnn  42765  zdivgd  42769  sn-remul0ord  42840  mulgt0b1d  42917  frlmfzowrdb  42949  frlmsnic  42985  evlselvlem  43019  prjspreln0  43042  elrfi  43126  diophrw  43191  eldioph2b  43195  diophin  43204  rexrabdioph  43222  rmxycomplete  43345  coprmdvdsb  43413  jm2.19  43421  jm2.26  43430  jm2.27  43436  limsuc2  43469  dgraa0p  43577  rngunsnply  43597  fiuneneq  43620  unielss  43646  oaabsb  43722  nnoeomeqom  43740  cantnfresb  43752  tfsconcatrn  43770  tfsconcat0b  43774  tfsconcatrev  43776  oadif1lem  43807  oadif1  43808  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  pwelg  43987  nzss  44744  dvconstbi  44761  expgrowth  44762  bcc0  44767  axc11next  44833  pm14.24  44859  sbiota1  44861  sbcim2g  44965  sineq0ALT  45363  mapss2  45634  fsneq  45635  fsneqrn  45640  mapssbi  45642  rnmptbd2lem  45677  infnsuprnmpt  45679  rnmptbdlem  45684  xralrple2  45784  infxrunb2  45797  xralrple4  45802  xralrple3  45803  xrralrecnnle  45812  xrralrecnnge  45819  reclt0  45820  supxrunb3  45828  supxrleubrnmpt  45834  xrre4  45839  unb2ltle  45843  rexabslelem  45846  suprleubrnmpt  45850  infxrunb3rnmpt  45856  uzub  45859  supminfrnmpt  45873  iccintsng  45953  sqrlearg  45983  uzinico  45989  preimaiocmnf  45990  limcresiooub  46070  limclr  46083  climeldmeq  46093  limsuppnflem  46138  limsupmnflem  46148  limsupmnfuzlem  46154  limsupre3lem  46160  limsupre3uzlem  46163  liminfreuzlem  46230  dvnmul  46371  dvmptfprodlem  46372  ismbl3  46414  ismbl4  46421  fourierdlem50  46584  fourierdlem89  46623  fourierdlem91  46625  dfsalgen2  46769  sge0repnf  46814  sge0lefi  46826  sge0resplit  46834  sge0fodjrnlem  46844  voliunsge0lem  46900  hspdifhsp  47044  isvonmbl  47066  ovnovollem3  47086  vonvolmbl  47089  pimrecltpos  47136  preimaicomnf  47139  pimrecltneg  47152  issmflem  47155  issmfle  47173  issmfgt  47184  smfaddlem1  47191  issmfge  47198  smfresal  47216  smflimmpt  47238  smfinflem  47245  smflimsuplem7  47254  smflimsupmpt  47257  sigarcol  47292  confun  47387  or2expropbi  47482  fsetsniunop  47497  fcoresf1b  47518  f1cof1b  47525  funfocofob  47526  rexsb  47547  euoreqb  47557  ralbinrald  47570  rlimdmafv  47625  fafv2elrnb  47683  tz6.12c-afv2  47690  dfatbrafv2b  47693  fnbrafv2b  47696  rlimdmafv2  47706  f1oresf1o2  47739  el1fzopredsuc  47774  2ffzoeq  47776  nnmul2b  47779  modlt0b  47817  nndivides2  47832  imasetpreimafvbijlemfo  47865  iccpartiun  47894  ichnfb  47925  ich2exprop  47931  sprsymrelfolem2  47953  paireqne  47971  prprelprb  47977  reupr  47982  nprmmul2  47988  nprmmul3  47989  requad01  48097  requad1  48098  requad2  48099  dfodd6  48113  dfeven4  48114  evensumeven  48183  sbgoldbalt  48257  clnbgrel  48304  dfclnbgr6  48332  dfnbgr6  48333  isubgredg  48342  isuspgrim0  48370  isuspgrim  48372  gricushgr  48393  uhgrimisgrgriclem  48406  clnbgrgrim  48410  grimedg  48411  usgrgrtrirex  48426  uspgrlimlem2  48465  uspgrlim  48468  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  isassintop  48686  uzlidlring  48711  rngcisoALTV  48753  ringcisoALTV  48787  domnmsuppn0  48845  lindslininds  48940  snlindsntor  48947  isldepslvec2  48961  affinecomb1  49178  prelrrx2b  49190  rrx2plord2  49198  eenglngeehlnm  49215  rrx2vlinest  49217  line2xlem  49229  line2x  49230  line2y  49231  itsclc0xyqsolb  49246  itsclquadb  49252  mpbiran3d  49272  opnneieqv  49386  iscnrm3lem2  49410  fullthinc2  49926  thincciso  49928