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  641  impbida  800  dedlem0b  1044  dedlema  1045  dedlemb  1046  albi  1818  alexbii  1833  equequ1  2025  equequ2  2026  spsbbi  2074  elequ1  2116  elequ2  2124  sbequ12  2252  sbft  2270  cbv2w  2335  exsb  2357  dral1v  2367  cbv2  2401  cbv2h  2404  ax12b  2422  dral1  2437  dral1ALT  2438  eupickb  2628  eupickbi  2629  2eu2  2646  ralbi  3085  rexbi  3086  ralbida  3248  ceqsalt  3481  rspcebdv  3582  rspceb2dv  3592  ceqex  3618  elabgtOLD  3639  mob2  3686  reu6  3697  sbciegftOLD  3791  sbcg  3826  2reu2  3861  csbiebt  3891  dfss2  3932  ssdifsym  4237  reupick  4292  reupick2  4294  uneqdifeq  4456  prnebg  4820  preqsnd  4823  prel12g  4828  iuneqconst  4967  disjeq2  5078  disjeq1  5081  disjss3  5106  reusv2lem2  5354  reusv2lem3  5355  alxfr  5362  ralxfrd  5363  ralxfrd2  5367  copsexgw  5450  copsexg  5451  snopeqop  5466  euotd  5473  poeq2  5550  sotric  5576  sotrieq  5577  freq2  5606  seeq1  5608  seeq2  5609  iss  6006  tz7.7  6358  ordtri1  6365  ordelinel  6435  iotavalOLD  6485  funeq  6536  funssres  6560  f0dom0  6744  tz6.12cOLD  6885  fnbrfvb  6911  ssimaex  6946  fvimacnv  7025  elpreima  7030  feldmfvelcdm  7058  eldmrexrnb  7064  fsn  7107  fnsnbg  7138  fnsnbOLD  7140  fmptsng  7142  fmptsnd  7143  fprb  7168  tpres  7175  fconst2g  7177  fconst5  7180  elunirn  7225  f1ocnvfvb  7254  f1prex  7259  foeqcnvco  7275  f1eqcocnv  7276  fliftfun  7287  soisores  7302  isofr  7317  isose  7318  isopo  7321  isoso  7323  f1oiso2  7327  eusvobj2  7379  oprabidw  7418  oprabid  7419  f1opw2  7644  oneqmin  7776  ordsucOLD  7789  ordelsuc  7795  ordsucelsuc  7797  ordunisuc2  7820  limsuc  7825  fndmexb  7882  resf1ext2b  7911  f1ovv  7936  mptcnfimad  7965  op1steq  8012  opreuopreu  8013  funeldmdif  8027  fvn0elsuppb  8160  extmptsuppeq  8167  rntpos  8218  smoiso2  8338  seqomlem2  8419  oaord  8511  oawordex  8521  oaordex  8522  omord2  8531  om00  8539  oeord  8552  nnaord  8583  nnmord  8596  nnawordex  8601  nnaordex  8602  nnaordex2  8603  eldifsucnn  8628  erexb  8696  swoord1  8703  swoord2  8704  ecelqsdmb  8759  iiner  8762  eceqoveq  8795  mapsnd  8859  ralxpmap  8869  omxpenlem  9042  domtriord  9087  mapxpen  9107  mapunen  9110  ssenen  9115  enfi  9151  nneneq  9170  nndomog  9177  onomeneq  9178  en1eqsnbi  9221  fodomfib  9280  fodomfibOLD  9282  f1opwfi  9307  fsuppunbi  9340  elfiun  9381  suplub2  9412  ordiso2  9468  ordiso  9469  oieu  9492  brwdom2  9526  brwdom3  9535  cantnflem1  9642  ttrclselem2  9679  cardidm  9912  carddom2  9930  pm54.43  9954  pr2neOLD  9958  acnen  10006  acnen2  10008  alephord  10028  alephinit  10048  dfac5  10082  infdif2  10162  fictb  10197  coflim  10214  fincssdom  10276  fin23lem25  10277  isf32lem9  10314  isf34lem4  10330  fin1a2lem11  10363  axdc3lem2  10404  ficard  10518  fpwwe2lem11  10594  fpwwe2  10596  indpi  10860  nqereq  10888  1idpr  10982  ltapr  10998  leltne  11263  ltlen  11275  ltadd2  11278  addlsub  11594  addid0  11597  ltord1  11704  mul0or  11818  ldiv  12016  ltmul1  12032  mulge0b  12053  lt2msq  12068  nnsub  12230  nn0sub  12492  zrevaddcl  12578  zltp1le  12583  zdiv  12604  nneo  12618  zeo2  12621  zmax  12904  zbtwnre  12905  qrevaddcl  12930  xrlttri  13099  xrleltne  13105  xralrple  13165  xltneg  13177  xleadd1  13215  xlemul1  13250  supxrunb1  13279  supxrunb2  13280  ioo0  13331  iccid  13351  ico0  13352  ioc0  13353  icc0  13354  difreicc  13445  iccsplit  13446  zltaddlt1le  13466  0fz1  13505  uzsplit  13557  fzm1  13568  fzrevral  13573  ssfzo12bi  13722  elfznelfzob  13734  flge  13767  modid2  13860  modmuladd  13878  ssnn0fi  13950  seqf1olem1  14006  hashen  14312  hashdom  14344  hash2exprb  14436  pr2pwpr  14444  hashtpg  14450  hash3tpexb  14459  len0nnbi  14516  ccats1pfxeqbi  14707  reuccatpfxs1  14712  repsdf2  14743  scshwfzeqfzo  14792  relexpindlem  15029  shftlem  15034  shftuz  15035  abslt  15281  absle  15282  rexico  15320  cau3lem  15321  reusq0  15431  rlim2lt  15463  rlim3  15464  o1lo1  15503  rlimdm  15517  climshft  15542  o1dif  15596  isercolllem2  15632  isercoll  15634  zsum  15684  fsum  15686  fsum00  15764  incexclem  15802  zprod  15903  fprod  15907  dvdsval2  16225  moddvds  16233  negdvdsb  16242  dvdsnegb  16243  dvdscmulr  16254  dvdsmulcr  16255  dvdssub2  16271  dvdsaddre2b  16277  fzo0dvdseq  16293  mod2eq1n2dvds  16317  ltoddhalfle  16331  sumodd  16358  bitsf1ocnv  16414  sadcaddlem  16427  bitsuz  16444  dvdsgcdb  16515  gcdzeq  16522  dvdssqlem  16536  lcmeq0  16570  lcmdvdsb  16583  lcmfeq0b  16600  lcmf  16603  lcmfdvdsb  16613  coprmgcdb  16619  cncongr  16639  isprm2lem  16651  dvdsprime  16657  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  17600  isacs2  17614  isssc  17782  setciso  18053  posasymb  18280  pleval2  18296  pltval3  18298  lublecllem  18319  joinle  18345  meetle  18359  latdisd  18456  lubun  18474  clatleglb  18477  letsr  18552  intopsn  18581  gsumval2a  18612  frmdss2  18790  isgrpid2  18908  isgrpinv  18925  f1ghm0to0  19177  symg1bas  19321  oddvdsnn0  19474  oddvds  19477  odeq  19480  odeq1  19490  gexdvds  19514  pgpfi  19535  pgpssslw  19544  fislw  19555  sylow3lem2  19558  lsmelvalm  19581  lsmlub  19594  lsmss1b  19596  lsmss2b  19598  efgs1b  19666  cyggenod  19814  cyggexb  19829  dprdfeq0  19954  ablsimpgfind  20042  ringinvnz1ne0  20209  ringinvnzdiv  20210  unitmulclb  20290  dvreq1  20320  isnzr2  20427  0ringnnzr  20434  0ring01eqbi  20441  rngciso  20547  ringciso  20581  rrgeq0  20609  domneq0  20617  drngmul0orOLD  20670  isabvd  20721  issrngd  20764  lssats2  20906  lspsneq0  20918  lsmelval2  20992  lvecvs0or  21018  lspsneq  21032  lspsneu  21033  lidl1el  21136  lidldvgen  21244  pzriprnglem10  21400  pzriprnglem11  21401  znunit  21473  psgndif  21511  ipeq0  21547  ocvsscon  21584  pjdm2  21620  obselocv  21637  islinds4  21744  psdmul  22053  ply1coe1eq  22187  cply1coe0bi  22189  mat1dimelbas  22358  cramer  22578  toponcomb  22816  tgss3  22873  clsval2  22937  isopn3  22953  elcls3  22970  opncldf1  22971  neiint  22991  neips  23000  opnneissb  23001  opnssneib  23002  opnnei  23007  tpnei  23008  opnneiid  23013  restcld  23059  restopnb  23062  tgcn  23139  tgcnp  23140  subbascn  23141  iscnp4  23150  cnpnei  23151  cncls2  23160  cncls  23161  cnntr  23162  lmss  23185  hausnei2  23240  lpcls  23251  ordtt1  23266  cmpsub  23287  tgcmp  23288  1stcelcls  23348  locfincmp  23413  kgencn2  23444  ptpjpre1  23458  upxp  23510  txcn  23513  txlm  23535  tgqtop  23599  kqfvima  23617  isr0  23624  regr1lem2  23627  hmeoopn  23653  hmeocld  23654  ptuncnv  23694  fbunfip  23756  fgss2  23761  ufilb  23793  ufprim  23796  trufil  23797  cfinufil  23815  ufildr  23818  elfm2  23835  elfm3  23837  rnelfm  23840  fmfnfmlem4  23844  fmco  23848  flimtopon  23857  flimopn  23862  fbflim2  23864  flimrest  23870  flffbas  23882  cnpflf  23888  fclstopon  23899  fclsnei  23906  fclsbas  23908  fclsfnflim  23914  fclscmp  23917  ufilcmp  23919  isfcf  23921  fcfnei  23922  cnpfcf  23928  alexsubb  23933  alexsubALT  23938  cldsubg  23998  tgphaus  24004  tgpt0  24006  tsmsgsum  24026  tsmsres  24031  xbln0  24302  blssexps  24314  blssex  24315  isxms2  24336  prdsbl  24379  neibl  24389  metss  24396  met2ndc  24411  metrest  24412  metcnp3  24428  tngngp3  24544  nmoeq0  24624  xrsxmet  24698  reconn  24717  iccpnfcnv  24842  fgcfil  25171  iscau4  25179  cfilres  25196  iunmbl2  25458  ismbf3d  25555  mbfaddlem  25561  i1faddlem  25594  i1fmullem  25595  ellimc3  25780  dvfsumlem2  25933  tdeglem4  25965  deg1nn0clb  25995  deg1lt0  25996  dvdsq1p  26068  plypf1  26117  0dgrb  26151  plymul0or  26188  taylthlem2  26282  ulmshft  26299  ulmcaulem  26303  ulmcau  26304  cosord  26440  eff1olem  26457  lognegb  26499  eflogeq  26511  logdivlt  26530  efopn  26567  cxpeq0  26587  cxpeq  26667  angpieqvd  26741  dcubic  26756  asinsinb  26807  acoscosb  26808  atantanb  26834  rlimcnp  26875  isppw  27024  isppw2  27025  vmappw  27026  isnsqf  27045  ppieq0  27086  fsumdvdsdiag  27094  dvdsppwf1o  27096  fsumfldivdiag  27100  chpeq0  27119  chteq0  27120  dchrptlem1  27175  lgsdir2lem4  27239  lgsne0  27246  lgsqr  27262  lgsdchrval  27265  gausslemma2dlem1a  27276  lgsquadlem1  27291  m1lgs  27299  2sqreultblem  27359  2sqreunnltblem  27362  nodenselem8  27603  sltlend  27683  oldlim  27798  sltlpss  27819  sleadd1  27896  sltneg  27951  muls0ord  28088  absslt  28151  onslt  28168  n0subs  28253  n0sltp1le  28255  zs12ge0  28342  iscgrglt  28441  brbtwn  28826  brcgr  28827  brbtwn2  28832  axcontlem7  28897  uhgr0vb  28999  edglnl  29070  ausgrusgrb  29092  ushgredgedg  29156  ushgredgedgloop  29158  usgr0vb  29164  usgr1v  29183  nbupgr  29271  nbumgrvtx  29273  nbuhgr2vtx1edgb  29279  edgusgrnbfin  29300  nb3grprlem1  29307  uvtxnbvtxm1  29333  cusgrfilem2  29384  uhgr0edg0rgrb  29502  cusgrm1rusgr  29510  spthonepeq  29682  usgr2pth  29694  wlkiswwlks  29806  wlkiswwlkupgr  29808  wlklnwwlkn  29814  wlklnwwlknupgr  29816  wwlksnextbi  29824  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  wwlksnextprop  29842  umgrwwlks2on  29887  elwspths2on  29890  usgr2wspthons3  29894  elwwlks2  29896  elwspths2spth  29897  clwlkclwwlklem3  29930  loopclwwlkn1b  29971  clwwlknon1sn  30029  clwwlknonwwlknonb  30035  umgr3v3e3cycl  30113  eupth2lem3lem4  30160  frgr0v  30191  frgr3vlem2  30203  2clwwlk2clwwlk  30279  wlkl0  30296  grpoinvf  30461  nvmul0or  30579  nvz  30598  diporthcom  30645  ubthlem3  30801  hvmul0or  30954  his6  31028  hial0  31031  hial02  31032  orthcom  31037  normgt0  31056  ocin  31225  occon3  31226  shsel3  31244  shlub  31343  chssoc  31425  h1de2bi  31483  spansncol  31497  elspansn4  31502  spansnss2  31504  sumspansn  31578  lnopcnbd  31965  lnfncnbd  31986  riesz1  31994  elpjrn  32119  cvcon3  32213  dmdmd  32229  dmdbr3  32234  dmdbr4  32235  dmdbr5  32237  mdslmd1i  32258  atcveq0  32277  chcv1  32284  atssma  32307  atcv0eq  32308  atcv1  32309  bian1dOLD  32386  disjeq1f  32502  br8d  32538  fpwrelmap  32656  xaddeq0  32676  eliccelico  32700  elicoelioo  32701  indf1ofs  32789  isarchiofld  33295  unitdivcld  33891  xrge0iifcnv  33923  lmxrge0  33942  eulerpartlemgh  34369  dstfrvunirn  34466  fnrelpredd  35079  loop1cycl  35124  cusgracyclt3v  35143  cvmliftmolem2  35269  cvmlift2lem12  35301  satfvsucsuc  35352  satfdm  35356  fmlasuc  35373  satffunlem1lem2  35390  satffunlem2lem2  35393  mthmb  35568  climuzcnv  35658  br8  35743  br6  35744  br4  35745  funbreq  35757  axextbdist  35788  dfrdg4  35939  cgrcom  35978  cgrcoml  35984  cgrdegen  35992  btwncom  36002  brsegle  36096  brsegle2  36097  colinbtwnle  36106  btwnoutside  36113  broutsideof3  36114  outsidele  36120  lineunray  36135  lineelsb2  36136  elhf2  36163  elicc3  36305  nn0prpwlem  36310  opnbnd  36313  cldbnd  36314  opnregcld  36318  cldregopn  36319  fnessref  36345  refssfne  36346  neibastop2  36349  fnemeet2  36355  fnejoin2  36357  fgmin  36358  ontgval  36419  ordtop  36424  ordcmp  36435  nndivsub  36445  bj-19.21t  36757  bj-19.23t  36758  bj-19.42t  36761  bj-sbft  36763  bj-cbv2hv  36785  bj-equsal1t  36810  bj-19.21t0  36818  bj-ceqsalt0  36872  bj-ceqsalt1  36873  bj-xpnzexb  36949  bj-idreseq  37150  bj-imdiridlem  37173  bj-finsumval0  37273  bj-fvimacnv0  37274  bj-isrvec2  37288  bj-bary1  37300  dfgcd3  37312  isbasisrelowllem1  37343  isbasisrelowllem2  37344  finxpsuclem  37385  wl-lem-exsb  37554  wl-mo3t  37564  wl-ax11-lem1  37573  matunitlindf  37612  poimirlem6  37620  poimirlem7  37621  poimirlem16  37630  poimirlem19  37633  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  cnambfre  37662  itg2addnc  37668  brabg2  37711  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  ssbnd  37782  ismtybnd  37801  reheibor  37833  grpoeqdivid  37875  grpokerinj  37887  rngosn3  37918  rngoueqz  37934  1idl  38020  0rngo  38021  divrngidl  38022  igenval2  38060  ispridlc  38064  isdmn3  38068  relcnveq3  38309  iss2  38326  elrelscnveq3  38482  funALTVeq  38692  disjeq  38726  prtlem10  38858  prter2  38874  dral1-o  38897  lshpinN  38982  lsatcveq0  39025  lsatcv0eq  39040  lsatcv1  39041  islshpcv  39046  lkr0f  39087  lkrshp4  39101  lshpkrlem1  39103  lshpset2N  39112  lfl1dim  39114  lfl1dim2N  39115  lub0N  39182  glb0N  39186  oplecon3b  39193  cmtcomN  39242  cmtbr3N  39247  cmtbr4N  39248  cvrnbtwn2  39268  cvrnbtwn3  39269  cvrcon3b  39270  cvrnbtwn4  39272  cvrcmp  39276  atcvreq0  39307  atnle  39310  atlatle  39313  cvlexchb1  39323  cvlcvr1  39332  hlrelat2  39397  exatleN  39398  cvrval3  39407  cvrval4N  39408  cvrexch  39414  atcvr0eq  39420  lnnat  39421  atcvrj0  39422  atcvrj2b  39426  atltcvr  39429  atbtwn  39440  ps-1  39471  3at  39484  islln2a  39511  llncmp  39516  islpln2a  39542  lplncmp  39556  islvol2aN  39586  4at  39607  lvolcmp  39611  pmaple  39755  lncmp  39777  paddss  39839  llnexchb2lem  39862  2polcon4bN  39912  ispsubcl2N  39941  lhpat3  40040  lautcvr  40086  ltrnid  40129  trlval2  40157  trlatn0  40166  ltrnideq  40169  trlnidatb  40171  cdlemeg49lebilem  40533  trlord  40563  cdlemg1a  40564  cdlemg1cex  40582  tendoid0  40819  dva1dim  40979  cdlemm10N  41112  diarnN  41123  cdlemn  41206  dihlspsnssN  41326  dihatexv  41332  dochkrshp  41380  dochkrshp4  41383  djhlsmcl  41408  lcfl6  41494  lcfl8  41496  lcfrvalsnN  41535  lcfrlem9  41544  mapdval2N  41624  mapdordlem2  41631  mapd1o  41642  mapd0  41659  mapdheq2biN  41724  nnproddivdvdsd  41988  primrootspoweq0  42094  aks6d1c1p1  42095  aks6d1c5lem1  42124  sticksstones11  42144  sticksstones22  42156  grpods  42182  unitscyglem2  42184  eqresfnbd  42220  expeq1d  42312  expeqidd  42313  dvdsexpnn  42321  zdivgd  42325  sn-remul0ord  42396  mulgt0b1d  42460  frlmfzowrdb  42492  frlmsnic  42528  evlselvlem  42574  prjspreln0  42597  elrfi  42682  diophrw  42747  eldioph2b  42751  diophin  42760  rexrabdioph  42782  rmxycomplete  42906  coprmdvdsb  42974  jm2.19  42982  jm2.26  42991  jm2.27  42997  limsuc2  43030  dgraa0p  43138  rngunsnply  43158  fiuneneq  43181  unielss  43207  oaabsb  43283  nnoeomeqom  43301  cantnfresb  43313  tfsconcatrn  43331  tfsconcat0b  43335  tfsconcatrev  43337  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  pwelg  43549  nzss  44306  dvconstbi  44323  expgrowth  44324  bcc0  44329  axc11next  44395  pm14.24  44421  sbiota1  44423  sbcim2g  44528  sineq0ALT  44926  mapss2  45199  fsneq  45200  fsneqrn  45205  mapssbi  45207  rnmptbd2lem  45242  infnsuprnmpt  45244  rnmptbdlem  45249  xralrple2  45350  infxrunb2  45364  xralrple4  45369  xralrple3  45370  xrralrecnnle  45379  xrralrecnnge  45386  reclt0  45387  supxrunb3  45395  supxrleubrnmpt  45402  xrre4  45407  unb2ltle  45411  rexabslelem  45414  suprleubrnmpt  45418  infxrunb3rnmpt  45424  uzub  45427  supminfrnmpt  45441  iccintsng  45521  sqrlearg  45551  uzinico  45557  preimaiocmnf  45558  limcresiooub  45640  limclr  45653  climeldmeq  45663  limsuppnflem  45708  limsupmnflem  45718  limsupmnfuzlem  45724  limsupre3lem  45730  limsupre3uzlem  45733  liminfreuzlem  45800  dvnmul  45941  dvmptfprodlem  45942  ismbl3  45984  ismbl4  45991  fourierdlem50  46154  fourierdlem89  46193  fourierdlem91  46195  dfsalgen2  46339  sge0repnf  46384  sge0lefi  46396  sge0resplit  46404  sge0fodjrnlem  46414  voliunsge0lem  46470  hspdifhsp  46614  isvonmbl  46636  ovnovollem3  46656  vonvolmbl  46659  pimrecltpos  46706  preimaicomnf  46709  pimrecltneg  46722  issmflem  46725  issmfle  46743  issmfgt  46754  smfaddlem1  46761  issmfge  46768  smfresal  46786  smflimmpt  46808  smfinflem  46815  smflimsuplem7  46824  smflimsupmpt  46827  sigarcol  46862  confun  46940  or2expropbi  47035  fsetsniunop  47050  fcoresf1b  47071  f1cof1b  47078  funfocofob  47079  rexsb  47100  euoreqb  47110  ralbinrald  47123  rlimdmafv  47178  fafv2elrnb  47236  tz6.12c-afv2  47243  dfatbrafv2b  47246  fnbrafv2b  47249  rlimdmafv2  47259  f1oresf1o2  47292  el1fzopredsuc  47326  2ffzoeq  47328  modlt0b  47364  imasetpreimafvbijlemfo  47406  iccpartiun  47435  ichnfb  47466  ich2exprop  47472  sprsymrelfolem2  47494  paireqne  47512  prprelprb  47518  reupr  47523  requad01  47622  requad1  47623  requad2  47624  dfodd6  47638  dfeven4  47639  evensumeven  47708  sbgoldbalt  47782  clnbgrel  47829  dfclnbgr6  47856  dfnbgr6  47857  isubgredg  47866  isuspgrim0  47894  isuspgrim  47896  gricushgr  47917  uhgrimisgrgriclem  47930  clnbgrgrim  47934  grimedg  47935  usgrgrtrirex  47949  uspgrlimlem2  47988  uspgrlim  47991  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  isassintop  48198  uzlidlring  48223  rngcisoALTV  48265  ringcisoALTV  48299  domnmsuppn0  48357  lindslininds  48453  snlindsntor  48460  isldepslvec2  48474  affinecomb1  48691  prelrrx2b  48703  rrx2plord2  48711  eenglngeehlnm  48728  rrx2vlinest  48730  line2xlem  48742  line2x  48743  line2y  48744  itsclc0xyqsolb  48759  itsclquadb  48765  mpbiran3d  48785  opnneieqv  48899  iscnrm3lem2  48923  fullthinc2  49440  thincciso  49442