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  anbiim  648  impbida  807  dedlem0b  1051  dedlema  1052  dedlemb  1053  albi  1826  alexbii  1841  equequ1  2033  equequ2  2034  spsbbi  2085  elequ1  2128  elequ2  2136  sbequ12  2265  sbft  2283  cbv2w  2347  exsb  2369  dral1v  2379  cbv2  2413  cbv2h  2416  ax12b  2434  dral1  2449  dral1ALT  2450  eupickb  2641  eupickbi  2642  2eu2  2658  ralbi  3096  rexbi  3097  ralbida  3252  ceqsalt  3466  rspcebdv  3556  rspceb2dv  3566  ceqex  3592  elabgtOLD  3613  mob2  3658  reu6  3669  sbcg  3797  2reu2  3832  csbiebt  3862  dfss2  3903  reupick  4260  reupick2  4262  uneqdifeq  4423  prnebg  4790  preqsnd  4793  prel12g  4798  iuneqconst  4936  disjeq2  5046  disjeq1  5049  disjss3  5074  reusv2lem2  5331  reusv2lem3  5332  alxfr  5339  ralxfrd  5340  ralxfrd2  5344  copsexgw  5433  copsexgwOLD  5434  copsexg  5435  snopeqop  5450  euotd  5457  poeq2  5533  sotric  5559  sotrieq  5560  freq2  5589  seeq1  5591  seeq2  5592  iss  5994  tz7.7  6340  ordtri1  6347  ordelinel  6417  funeq  6509  funssres  6533  f0dom0  6715  fnbrfvb  6881  ssimaex  6916  fsneq  6980  fvimacnv  6998  elpreima  7003  feldmfvelcdm  7031  eldmrexrnb  7037  fsn  7081  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  8125  extmptsuppeq  8132  rntpos  8183  smoiso2  8303  seqomlem2  8384  oaord  8476  oawordex  8486  oaordex  8487  omord2  8496  om00  8504  oeord  8518  nnaord  8549  nnmord  8562  nnawordex  8567  nnaordex  8568  nnaordex2  8569  eldifsucnn  8594  erexb  8663  swoord1  8670  swoord2  8671  ecelqsdmb  8727  iiner  8730  eceqoveq  8763  mapsnd  8828  ralxpmap  8838  omxpenlem  9010  domtriord  9055  mapxpen  9075  mapunen  9078  ssenen  9083  enfi  9115  nneneq  9134  nndomog  9141  onomeneq  9142  en1eqsnbi  9180  fodomfib  9233  fodomfibOLD  9235  f1opwfi  9260  fsuppunbi  9296  elfiun  9337  suplub2  9368  ordiso2  9424  ordiso  9425  oieu  9448  brwdom2  9482  brwdom3  9491  cantnflem1  9605  ttrclselem2  9642  cardidm  9878  carddom2  9896  pm54.43  9920  acnen  9970  acnen2  9972  alephord  9992  alephinit  10012  dfac5  10046  infdif2  10126  fictb  10161  coflim  10178  fincssdom  10240  fin23lem25  10241  isf32lem9  10278  isf34lem4  10294  fin1a2lem11  10327  axdc3lem2  10368  ficard  10482  fpwwe2lem11  10559  fpwwe2  10561  indpi  10825  nqereq  10853  1idpr  10947  ltapr  10963  leltne  11230  ltlen  11242  ltadd2  11245  addlsub  11561  addid0  11564  ltord1  11671  mul0or  11785  ldiv  11984  ltmul1  12000  mulge0b  12021  lt2msq  12036  nnsub  12216  nn0sub  12482  zrevaddcl  12567  zltp1le  12572  zdiv  12594  nneo  12608  zeo2  12611  zmax  12890  zbtwnre  12891  qrevaddcl  12916  xrlttri  13085  xrleltne  13091  xralrple  13152  xltneg  13164  xleadd1  13202  xlemul1  13237  supxrunb1  13266  supxrunb2  13267  ioo0  13318  iccid  13338  ico0  13339  ioc0  13340  icc0  13341  difreicc  13432  iccsplit  13433  zltaddlt1le  13453  0fz1  13493  uzsplit  13545  fzm1  13556  fzrevral  13561  ssfzo12bi  13711  elfznelfzob  13724  flge  13759  modid2  13852  modmuladd  13870  ssnn0fi  13942  seqf1olem1  13998  hashen  14304  hashdom  14336  hash2exprb  14428  pr2pwpr  14436  hashtpg  14442  hash3tpexb  14451  len0nnbi  14508  ccats1pfxeqbi  14699  reuccatpfxs1  14704  repsdf2  14735  scshwfzeqfzo  14783  relexpindlem  15020  shftlem  15025  shftuz  15026  abslt  15272  absle  15273  rexico  15311  cau3lem  15312  reusq0  15422  rlim2lt  15454  rlim3  15455  o1lo1  15494  rlimdm  15508  climshft  15533  o1dif  15587  isercolllem2  15623  isercoll  15625  zsum  15675  fsum  15677  fsum00  15756  incexclem  15796  zprod  15897  fprod  15901  dvdsval2  16219  moddvds  16227  negdvdsb  16236  dvdsnegb  16237  dvdscmulr  16248  dvdsmulcr  16249  dvdssub2  16265  dvdsaddre2b  16271  fzo0dvdseq  16287  mod2eq1n2dvds  16311  ltoddhalfle  16325  sumodd  16352  bitsf1ocnv  16408  sadcaddlem  16421  bitsuz  16438  dvdsgcdb  16509  gcdzeq  16516  dvdssqlem  16530  lcmeq0  16564  lcmdvdsb  16577  lcmfeq0b  16594  lcmf  16597  lcmfdvdsb  16607  coprmgcdb  16613  cncongr  16633  isprm2lem  16645  dvdsprime  16651  dvdsprm  16668  isprm7  16673  coprm  16676  euclemma  16678  rpexp  16687  prmdvdsncoprmbd  16692  prmdiveq  16751  hashgcdlem  16753  odzdvds  16761  pythagtrip  16800  pc2dvds  16845  pcprmpw2  16848  pcprmpw  16849  vdwapun  16940  ramtcl2  16977  firest  17390  mrieqv2d  17600  isacs2  17614  isssc  17782  setciso  18053  posasymb  18280  pleval2  18296  pltval3  18298  lublecllem  18319  joinle  18345  meetle  18359  latdisd  18458  lubun  18476  clatleglb  18479  letsr  18554  intopsn  18617  gsumval2a  18648  frmdss2  18826  isgrpid2  18947  isgrpinv  18964  f1ghm0to0  19215  symg1bas  19361  oddvdsnn0  19514  oddvds  19517  odeq  19520  odeq1  19530  gexdvds  19554  pgpfi  19575  pgpssslw  19584  fislw  19595  sylow3lem2  19598  lsmelvalm  19621  lsmlub  19634  lsmss1b  19636  lsmss2b  19638  efgs1b  19706  cyggenod  19854  cyggexb  19869  dprdfeq0  19994  ablsimpgfind  20082  ringinvnz1ne0  20276  ringinvnzdiv  20277  unitmulclb  20356  dvreq1  20386  isnzr2  20494  0ringnnzr  20501  0ring01eqbi  20508  rngciso  20614  ringciso  20648  rrgeq0  20676  domneq0  20684  drngmul0orOLD  20737  isabvd  20788  issrngd  20831  lssats2  20994  lspsneq0  21006  lsmelval2  21079  lvecvs0or  21105  lspsneq  21119  lspsneu  21120  lidl1el  21223  lidldvgen  21331  pzriprnglem10  21469  pzriprnglem11  21470  znunit  21542  psgndif  21581  ipeq0  21617  ocvsscon  21654  pjdm2  21690  obselocv  21707  islinds4  21814  psdmul  22158  ply1coe1eq  22290  cply1coe0bi  22292  mat1dimelbas  22458  cramer  22678  toponcomb  22916  tgss3  22973  clsval2  23037  isopn3  23053  elcls3  23070  opncldf1  23071  neiint  23091  neips  23100  opnneissb  23101  opnssneib  23102  opnnei  23107  tpnei  23108  opnneiid  23113  restcld  23159  restopnb  23162  tgcn  23239  tgcnp  23240  subbascn  23241  iscnp4  23250  cnpnei  23251  cncls2  23260  cncls  23261  cnntr  23262  lmss  23285  hausnei2  23340  lpcls  23351  ordtt1  23366  cmpsub  23387  tgcmp  23388  1stcelcls  23448  locfincmp  23513  kgencn2  23544  ptpjpre1  23558  upxp  23610  txcn  23613  txlm  23635  tgqtop  23699  kqfvima  23717  isr0  23724  regr1lem2  23727  hmeoopn  23753  hmeocld  23754  ptuncnv  23794  fbunfip  23856  fgss2  23861  ufilb  23893  ufprim  23896  trufil  23897  cfinufil  23915  ufildr  23918  elfm2  23935  elfm3  23937  rnelfm  23940  fmfnfmlem4  23944  fmco  23948  flimtopon  23957  flimopn  23962  fbflim2  23964  flimrest  23970  flffbas  23982  cnpflf  23988  fclstopon  23999  fclsnei  24006  fclsbas  24008  fclsfnflim  24014  fclscmp  24017  ufilcmp  24019  isfcf  24021  fcfnei  24022  cnpfcf  24028  alexsubb  24033  alexsubALT  24038  cldsubg  24098  tgphaus  24104  tgpt0  24106  tsmsgsum  24126  tsmsres  24131  xbln0  24401  blssexps  24413  blssex  24414  isxms2  24435  prdsbl  24478  neibl  24488  metss  24495  met2ndc  24510  metrest  24511  metcnp3  24527  tngngp3  24643  nmoeq0  24723  xrsxmet  24797  reconn  24816  iccpnfcnv  24933  fgcfil  25260  iscau4  25268  cfilres  25285  iunmbl2  25546  ismbf3d  25643  mbfaddlem  25649  i1faddlem  25682  i1fmullem  25683  ellimc3  25868  dvfsumlem2  26016  tdeglem4  26047  deg1nn0clb  26077  deg1lt0  26078  dvdsq1p  26150  plypf1  26199  0dgrb  26233  plymul0or  26269  taylthlem2  26361  ulmshft  26377  ulmcaulem  26381  ulmcau  26382  cosord  26517  eff1olem  26534  lognegb  26576  eflogeq  26588  logdivlt  26607  efopn  26644  cxpeq0  26664  cxpeq  26743  angpieqvd  26817  dcubic  26832  asinsinb  26883  acoscosb  26884  atantanb  26910  rlimcnp  26951  isppw  27099  isppw2  27100  vmappw  27101  isnsqf  27120  ppieq0  27161  fsumdvdsdiag  27169  dvdsppwf1o  27171  fsumfldivdiag  27175  chpeq0  27193  chteq0  27194  dchrptlem1  27249  lgsdir2lem4  27313  lgsne0  27320  lgsqr  27336  lgsdchrval  27339  gausslemma2dlem1a  27350  lgsquadlem1  27365  m1lgs  27373  2sqreultblem  27433  2sqreunnltblem  27436  nodenselem8  27677  ltlesnd  27761  oldlim  27901  ltslpss  27922  leadds1  28003  ltnegs  28059  negleft  28072  negright  28073  muls0ord  28199  abslts  28263  onlts  28281  n0subs  28377  n0ltsp1le  28379  z12sge0  28497  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  29547  uhgr0edg0rgrb  29665  cusgrm1rusgr  29673  spthonepeq  29842  usgr2pth  29854  wlkiswwlks  29966  wlkiswwlkupgr  29968  wlklnwwlkn  29974  wlklnwwlknupgr  29976  wwlksnextbi  29984  wwlksnredwwlkn0  29986  wwlksnextwrd  29987  wwlksnextprop  30002  usgrwwlks2on  30048  umgrwwlks2on  30049  elwspths2on  30052  elwspths2onw  30053  usgr2wspthons3  30057  elwwlks2  30059  elwspths2spth  30060  clwlkclwwlklem3  30093  loopclwwlkn1b  30134  clwwlknon1sn  30192  clwwlknonwwlknonb  30198  umgr3v3e3cycl  30276  eupth2lem3lem4  30323  frgr0v  30354  frgr3vlem2  30366  2clwwlk2clwwlk  30442  wlkl0  30459  grpoinvf  30625  nvmul0or  30743  nvz  30762  diporthcom  30809  ubthlem3  30965  hvmul0or  31118  his6  31192  hial0  31195  hial02  31196  orthcom  31201  normgt0  31220  ocin  31389  occon3  31390  shsel3  31408  shlub  31507  chssoc  31589  h1de2bi  31647  spansncol  31661  elspansn4  31666  spansnss2  31668  sumspansn  31742  lnopcnbd  32129  lnfncnbd  32150  riesz1  32158  elpjrn  32283  cvcon3  32377  dmdmd  32393  dmdbr3  32398  dmdbr4  32399  dmdbr5  32401  mdslmd1i  32422  atcveq0  32441  chcv1  32448  atssma  32471  atcv0eq  32472  atcv1  32473  bian1dOLD  32548  disjeq1f  32666  br8d  32704  fpwrelmap  32829  xaddeq0  32849  eliccelico  32873  elicoelioo  32874  indf1ofs  32949  isarchiofld  33284  unitdivcld  34097  xrge0iifcnv  34129  lmxrge0  34148  eulerpartlemgh  34574  dstfrvunirn  34671  fnrelpredd  35287  rankfilimb  35298  fineqvnttrclse  35320  loop1cycl  35380  cusgracyclt3v  35399  cvmliftmolem2  35525  cvmlift2lem12  35557  satfvsucsuc  35608  satfdm  35612  fmlasuc  35629  satffunlem1lem2  35646  satffunlem2lem2  35649  mthmb  35824  climuzcnv  35914  br8  35999  br6  36000  br4  36001  funbreq  36013  axextbdist  36041  dfrdg4  36194  cgrcom  36233  cgrcoml  36239  cgrdegen  36247  btwncom  36257  brsegle  36351  brsegle2  36352  colinbtwnle  36361  btwnoutside  36368  broutsideof3  36369  outsidele  36375  lineunray  36390  lineelsb2  36391  elhf2  36418  elicc3  36560  nn0prpwlem  36565  opnbnd  36568  cldbnd  36569  opnregcld  36573  cldregopn  36574  fnessref  36600  refssfne  36601  neibastop2  36604  fnemeet2  36610  fnejoin2  36612  fgmin  36613  ontgval  36674  ordtop  36679  ordcmp  36690  nndivsub  36700  bj-cbval  37001  bj-cbvex  37002  bj-19.21t  37119  bj-19.23t  37120  bj-19.42t  37123  bj-sbft  37136  bj-nnf-cbval  37138  bj-cbv2hv  37165  bj-equsal1t  37190  bj-19.21t0  37198  bj-ceqsalt0  37252  bj-ceqsalt1  37253  bj-xpnzexb  37329  bj-axreprepsep  37443  cgsex2gd  37512  bj-idreseq  37537  bj-imdiridlem  37560  bj-finsumval0  37660  bj-fvimacnv0  37661  bj-isrvec2  37675  bj-bary1  37687  dfgcd3  37699  isbasisrelowllem1  37732  isbasisrelowllem2  37733  finxpsuclem  37774  wl-lem-exsb  37952  wl-mo3t  37962  matunitlindf  38000  poimirlem6  38008  poimirlem7  38009  poimirlem16  38018  poimirlem19  38021  poimirlem22  38024  poimirlem23  38025  poimirlem24  38026  cnambfre  38050  itg2addnc  38056  brabg2  38099  istotbnd3  38153  sstotbnd2  38156  sstotbnd  38157  sstotbnd3  38158  ssbnd  38170  ismtybnd  38189  reheibor  38221  grpoeqdivid  38263  grpokerinj  38275  rngosn3  38306  rngoueqz  38322  1idl  38408  0rngo  38409  divrngidl  38410  igenval2  38448  ispridlc  38452  isdmn3  38456  relcnveq3  38709  iss2  38726  elrelscnveq3  39009  funALTVeq  39167  disjeq  39216  prtlem10  39372  prter2  39388  dral1-o  39411  lshpinN  39496  lsatcveq0  39539  lsatcv0eq  39554  lsatcv1  39555  islshpcv  39560  lkr0f  39601  lkrshp4  39615  lshpkrlem1  39617  lshpset2N  39626  lfl1dim  39628  lfl1dim2N  39629  lub0N  39696  glb0N  39700  oplecon3b  39707  cmtcomN  39756  cmtbr3N  39761  cmtbr4N  39762  cvrnbtwn2  39782  cvrnbtwn3  39783  cvrcon3b  39784  cvrnbtwn4  39786  cvrcmp  39790  atcvreq0  39821  atnle  39824  atlatle  39827  cvlexchb1  39837  cvlcvr1  39846  hlrelat2  39910  exatleN  39911  cvrval3  39920  cvrval4N  39921  cvrexch  39927  atcvr0eq  39933  lnnat  39934  atcvrj0  39935  atcvrj2b  39939  atltcvr  39942  atbtwn  39953  ps-1  39984  3at  39997  islln2a  40024  llncmp  40029  islpln2a  40055  lplncmp  40069  islvol2aN  40099  4at  40120  lvolcmp  40124  pmaple  40268  lncmp  40290  paddss  40352  llnexchb2lem  40375  2polcon4bN  40425  ispsubcl2N  40454  lhpat3  40553  lautcvr  40599  ltrnid  40642  trlval2  40670  trlatn0  40679  ltrnideq  40682  trlnidatb  40684  cdlemeg49lebilem  41046  trlord  41076  cdlemg1a  41077  cdlemg1cex  41095  tendoid0  41332  dva1dim  41492  cdlemm10N  41625  diarnN  41636  cdlemn  41719  dihlspsnssN  41839  dihatexv  41845  dochkrshp  41893  dochkrshp4  41896  djhlsmcl  41921  lcfl6  42007  lcfl8  42009  lcfrvalsnN  42048  lcfrlem9  42057  mapdval2N  42137  mapdordlem2  42144  mapd1o  42155  mapd0  42172  mapdheq2biN  42237  nnproddivdvdsd  42500  primrootspoweq0  42606  aks6d1c1p1  42607  aks6d1c5lem1  42636  sticksstones11  42656  sticksstones22  42668  grpods  42694  unitscyglem2  42696  eqresfnbd  42734  expeq1d  42816  expeqidd  42817  dvdsexpnn  42825  zdivgd  42829  sn-remul0ord  42900  mulgt0b1d  42977  frlmfzowrdb  43009  frlmsnic  43041  evlselvlem  43053  prjspreln0  43074  elrfi  43158  diophrw  43223  eldioph2b  43227  diophin  43236  rexrabdioph  43254  rmxycomplete  43377  coprmdvdsb  43445  jm2.19  43453  jm2.26  43462  jm2.27  43468  limsuc2  43501  dgraa0p  43609  rngunsnply  43629  fiuneneq  43652  unielss  43678  oaabsb  43754  nnoeomeqom  43772  cantnfresb  43784  tfsconcatrn  43802  tfsconcat0b  43806  tfsconcatrev  43808  oadif1lem  43839  oadif1  43840  fzunt  43914  fzuntd  43915  fzunt1d  43916  fzuntgd  43917  pwelg  44019  nzss  44776  dvconstbi  44793  expgrowth  44794  bcc0  44799  axc11next  44865  pm14.24  44891  sbiota1  44893  sbcim2g  44997  sineq0ALT  45395  mapss2  45665  fsneqrn  45670  mapssbi  45672  rnmptbd2lem  45706  infnsuprnmpt  45708  rnmptbdlem  45713  xralrple2  45813  infxrunb2  45826  xralrple4  45831  xralrple3  45832  xrralrecnnle  45841  xrralrecnnge  45848  reclt0  45849  supxrunb3  45857  supxrleubrnmpt  45863  xrre4  45868  unb2ltle  45872  rexabslelem  45875  suprleubrnmpt  45879  infxrunb3rnmpt  45885  uzub  45888  supminfrnmpt  45902  iccintsng  45982  sqrlearg  46012  uzinico  46018  preimaiocmnf  46019  limcresiooub  46099  limclr  46112  climeldmeq  46122  limsuppnflem  46167  limsupmnflem  46177  limsupmnfuzlem  46183  limsupre3lem  46189  limsupre3uzlem  46192  liminfreuzlem  46259  dvnmul  46400  dvmptfprodlem  46401  ismbl3  46443  ismbl4  46450  fourierdlem50  46613  fourierdlem89  46652  fourierdlem91  46654  dfsalgen2  46798  sge0repnf  46843  sge0lefi  46855  sge0resplit  46863  sge0fodjrnlem  46873  voliunsge0lem  46929  hspdifhsp  47073  isvonmbl  47095  ovnovollem3  47115  vonvolmbl  47118  pimrecltpos  47165  preimaicomnf  47168  pimrecltneg  47181  issmflem  47184  issmfle  47202  issmfgt  47213  smfaddlem1  47220  issmfge  47227  smfresal  47245  smflimmpt  47267  smfinflem  47274  smflimsuplem7  47283  smflimsupmpt  47286  sigarcol  47321  confun  47416  or2expropbi  47511  fsetsniunop  47526  fcoresf1b  47547  f1cof1b  47554  funfocofob  47555  rexsb  47576  euoreqb  47586  ralbinrald  47599  rlimdmafv  47654  fafv2elrnb  47712  tz6.12c-afv2  47719  dfatbrafv2b  47722  fnbrafv2b  47725  rlimdmafv2  47735  f1oresf1o2  47768  el1fzopredsuc  47803  2ffzoeq  47805  nnmul2b  47808  modlt0b  47846  nndivides2  47861  imasetpreimafvbijlemfo  47894  iccpartiun  47923  ichnfb  47954  ich2exprop  47960  sprsymrelfolem2  47982  paireqne  48000  prprelprb  48006  reupr  48011  nprmmul2  48017  nprmmul3  48018  requad01  48126  requad1  48127  requad2  48128  dfodd6  48142  dfeven4  48143  evensumeven  48212  sbgoldbalt  48286  clnbgrel  48333  dfclnbgr6  48361  dfnbgr6  48362  isubgredg  48371  isuspgrim0  48399  isuspgrim  48401  gricushgr  48422  uhgrimisgrgriclem  48435  clnbgrgrim  48439  grimedg  48440  usgrgrtrirex  48455  uspgrlimlem2  48494  uspgrlim  48497  gpgedgiov  48570  gpgedg2ov  48571  gpgedg2iv  48572  gpgnbgrvtx0  48579  gpgnbgrvtx1  48580  isassintop  48715  uzlidlring  48740  rngcisoALTV  48782  ringcisoALTV  48816  domnmsuppn0  48874  lindslininds  48969  snlindsntor  48976  isldepslvec2  48990  affinecomb1  49207  prelrrx2b  49219  rrx2plord2  49227  eenglngeehlnm  49244  rrx2vlinest  49246  line2xlem  49258  line2x  49259  line2y  49260  itsclc0xyqsolb  49275  itsclquadb  49281  mpbiran3d  49301  opnneieqv  49415  iscnrm3lem2  49439  fullthinc2  49955  thincciso  49957