Theorem impbid 212

Description: Deduce an equivalence from two implications. Deduction associated with impbi 208 and impbii 209. (Contributed by NM, 24-Jan-1993.) Revised to 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  640  impbida  800  dedlem0b  1045  dedlema  1046  dedlemb  1047  albi  1816  alexbii  1831  equequ1  2024  equequ2  2025  spsbbi  2073  elequ1  2115  elequ2  2123  sbequ12  2252  sbft  2271  cbv2w  2343  exsb  2365  dral1v  2375  dral1vOLD  2376  cbv2  2411  cbv2h  2414  ax12b  2432  dral1  2447  dral1ALT  2448  eupickb  2638  eupickbi  2639  2eu2  2656  ralbi  3109  rexbi  3110  ralbida  3276  ceqsalt  3523  rspcebdv  3629  rspceb2dv  3639  ceqex  3665  elabgt  3685  mob2  3737  reu6  3748  sbciegftOLD  3843  sbcg  3883  2reu2  3920  csbiebt  3951  dfss2  3994  sseq1  4034  ssdifsym  4293  reupick  4348  reupick2  4350  ab0OLD  4403  uneqdifeq  4516  prnebg  4880  preqsnd  4883  prel12g  4888  iuneqconst  5026  disjeq2  5137  disjeq1  5140  disjss3  5165  reusv2lem2  5417  reusv2lem3  5418  alxfr  5425  ralxfrd  5426  ralxfrd2  5430  copsexgw  5510  copsexg  5511  snopeqop  5525  euotd  5532  poeq2  5611  sotric  5637  sotrieq  5638  freq2  5668  seeq1  5670  seeq2  5671  iss  6064  tz7.7  6421  ordtri1  6428  ordelinel  6496  iotavalOLD  6547  funeq  6598  funssres  6622  f0dom0  6805  tz6.12cOLD  6947  fnbrfvb  6973  ssimaex  7007  fvimacnv  7086  elpreima  7091  feldmfvelcdm  7120  eldmrexrnb  7126  fsn  7169  fnsnb  7200  fmptsng  7202  fmptsnd  7203  fprb  7231  tpres  7238  fconst2g  7240  fconst5  7243  elunirn  7288  f1ocnvfvb  7315  f1prex  7320  foeqcnvco  7336  f1eqcocnv  7337  fliftfun  7348  soisores  7363  isofr  7378  isose  7379  isopo  7382  isoso  7384  f1oiso2  7388  eusvobj2  7440  oprabidw  7479  oprabid  7480  f1opw2  7705  oneqmin  7836  ordsucOLD  7850  ordelsuc  7856  ordsucelsuc  7858  ordunisuc2  7881  limsuc  7886  fndmexb  7946  f1ovv  7998  mptcnfimad  8027  op1steq  8074  opreuopreu  8075  funeldmdif  8089  fvn0elsuppb  8222  extmptsuppeq  8229  rntpos  8280  smoiso2  8425  seqomlem2  8507  oaord  8603  oawordex  8613  oaordex  8614  omord2  8623  om00  8631  oeord  8644  nnaord  8675  nnmord  8688  nnawordex  8693  nnaordex  8694  nnaordex2  8695  eldifsucnn  8720  erexb  8788  swoord1  8795  swoord2  8796  iiner  8847  eceqoveq  8880  mapsnd  8944  ralxpmap  8954  omxpenlem  9139  domtriord  9189  mapxpen  9209  mapunen  9212  ssenen  9217  enfi  9253  nneneq  9272  nndomog  9279  nneneqOLD  9284  nndomogOLD  9289  onomeneq  9291  onomeneqOLD  9292  en1eqsnbi  9338  fodomfib  9397  fodomfibOLD  9399  f1opwfi  9426  fsuppunbi  9458  elfiun  9499  suplub2  9530  ordiso2  9584  ordiso  9585  oieu  9608  brwdom2  9642  brwdom3  9651  cantnflem1  9758  ttrclselem2  9795  cardidm  10028  carddom2  10046  pm54.43  10070  pr2neOLD  10074  acnen  10122  acnen2  10124  alephord  10144  alephinit  10164  dfac5  10198  infdif2  10278  fictb  10313  coflim  10330  fincssdom  10392  fin23lem25  10393  isf32lem9  10430  isf34lem4  10446  fin1a2lem11  10479  axdc3lem2  10520  ficard  10634  fpwwe2lem11  10710  fpwwe2  10712  indpi  10976  nqereq  11004  1idpr  11098  ltapr  11114  leltne  11379  ltlen  11391  ltadd2  11394  addlsub  11706  addid0  11709  ltord1  11816  mul0or  11930  ldiv  12128  ltmul1  12144  mulge0b  12165  lt2msq  12180  nnsub  12337  nn0sub  12603  zrevaddcl  12688  zltp1le  12693  zdiv  12713  nneo  12727  zeo2  12730  zmax  13010  zbtwnre  13011  qrevaddcl  13036  xrlttri  13201  xrleltne  13207  xralrple  13267  xltneg  13279  xleadd1  13317  xlemul1  13352  supxrunb1  13381  supxrunb2  13382  ioo0  13432  iccid  13452  ico0  13453  ioc0  13454  icc0  13455  difreicc  13544  iccsplit  13545  zltaddlt1le  13565  0fz1  13604  uzsplit  13656  fzm1  13664  fzrevral  13669  ssfzo12bi  13811  elfznelfzob  13823  flge  13856  modid2  13949  modmuladd  13964  ssnn0fi  14036  seqf1olem1  14092  hashen  14396  hashdom  14428  hash2exprb  14520  pr2pwpr  14528  hashtpg  14534  hash3tpexb  14543  len0nnbi  14599  ccats1pfxeqbi  14790  reuccatpfxs1  14795  repsdf2  14826  scshwfzeqfzo  14875  relexpindlem  15112  shftlem  15117  shftuz  15118  abslt  15363  absle  15364  rexico  15402  cau3lem  15403  reusq0  15511  rlim2lt  15543  rlim3  15544  o1lo1  15583  rlimdm  15597  climshft  15622  o1dif  15676  isercolllem2  15714  isercoll  15716  zsum  15766  fsum  15768  fsum00  15846  incexclem  15884  zprod  15985  fprod  15989  dvdsval2  16305  moddvds  16313  negdvdsb  16321  dvdsnegb  16322  dvdscmulr  16333  dvdsmulcr  16334  dvdssub2  16349  dvdsaddre2b  16355  fzo0dvdseq  16371  mod2eq1n2dvds  16395  ltoddhalfle  16409  sumodd  16436  bitsf1ocnv  16490  sadcaddlem  16503  bitsuz  16520  dvdsgcdb  16592  gcdzeq  16599  dvdssqlem  16613  lcmeq0  16647  lcmdvdsb  16660  lcmfeq0b  16677  lcmf  16680  lcmfdvdsb  16690  coprmgcdb  16696  cncongr  16716  isprm2lem  16728  dvdsprime  16734  dvdsprm  16750  isprm7  16755  coprm  16758  euclemma  16760  rpexp  16769  prmdvdsncoprmbd  16774  prmdiveq  16833  hashgcdlem  16835  odzdvds  16842  pythagtrip  16881  pc2dvds  16926  pcprmpw2  16929  pcprmpw  16930  vdwapun  17021  ramtcl2  17058  firest  17492  mrieqv2d  17697  isacs2  17711  isssc  17881  setciso  18158  posasymb  18389  pleval2  18407  pltval3  18409  lublecllem  18430  joinle  18456  meetle  18470  latdisd  18567  lubun  18585  clatleglb  18588  letsr  18663  intopsn  18692  gsumval2a  18723  frmdss2  18898  isgrpid2  19016  isgrpinv  19033  f1ghm0to0  19285  symg1bas  19432  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  20323  ringinvnzdiv  20324  unitmulclb  20407  dvreq1  20437  isnzr2  20544  0ringnnzr  20551  0ring01eqbi  20558  rngciso  20660  ringciso  20694  rrgeq0  20722  domneq0  20730  drngmul0orOLD  20783  isabvd  20835  issrngd  20878  lssats2  21021  lspsneq0  21033  lsmelval2  21107  lvecvs0or  21133  lspsneq  21147  lspsneu  21148  lidl1el  21259  lidldvgen  21367  pzriprnglem10  21524  pzriprnglem11  21525  znunit  21605  psgndif  21643  ipeq0  21679  ocvsscon  21716  pjdm2  21754  obselocv  21771  islinds4  21878  psdmul  22193  ply1coe1eq  22325  cply1coe0bi  22327  mat1dimelbas  22498  cramer  22718  toponcomb  22956  tgss3  23014  clsval2  23079  isopn3  23095  elcls3  23112  opncldf1  23113  neiint  23133  neips  23142  opnneissb  23143  opnssneib  23144  opnnei  23149  tpnei  23150  opnneiid  23155  restcld  23201  restopnb  23204  tgcn  23281  tgcnp  23282  subbascn  23283  iscnp4  23292  cnpnei  23293  cncls2  23302  cncls  23303  cnntr  23304  lmss  23327  hausnei2  23382  lpcls  23393  ordtt1  23408  cmpsub  23429  tgcmp  23430  1stcelcls  23490  locfincmp  23555  kgencn2  23586  ptpjpre1  23600  upxp  23652  txcn  23655  txlm  23677  tgqtop  23741  kqfvima  23759  isr0  23766  regr1lem2  23769  hmeoopn  23795  hmeocld  23796  ptuncnv  23836  fbunfip  23898  fgss2  23903  ufilb  23935  ufprim  23938  trufil  23939  cfinufil  23957  ufildr  23960  elfm2  23977  elfm3  23979  rnelfm  23982  fmfnfmlem4  23986  fmco  23990  flimtopon  23999  flimopn  24004  fbflim2  24006  flimrest  24012  flffbas  24024  cnpflf  24030  fclstopon  24041  fclsnei  24048  fclsbas  24050  fclsfnflim  24056  fclscmp  24059  ufilcmp  24061  isfcf  24063  fcfnei  24064  cnpfcf  24070  alexsubb  24075  alexsubALT  24080  cldsubg  24140  tgphaus  24146  tgpt0  24148  tsmsgsum  24168  tsmsres  24173  xbln0  24445  blssexps  24457  blssex  24458  isxms2  24479  prdsbl  24525  neibl  24535  metss  24542  met2ndc  24557  metrest  24558  metcnp3  24574  tngngp3  24698  nmoeq0  24778  xrsxmet  24850  reconn  24869  iccpnfcnv  24994  fgcfil  25324  iscau4  25332  cfilres  25349  iunmbl2  25611  ismbf3d  25708  mbfaddlem  25714  i1faddlem  25747  i1fmullem  25748  ellimc3  25934  dvfsumlem2  26087  tdeglem4  26119  deg1nn0clb  26149  deg1lt0  26150  dvdsq1p  26222  plypf1  26271  0dgrb  26305  plymul0or  26340  taylthlem2  26434  ulmshft  26451  ulmcaulem  26455  ulmcau  26456  cosord  26591  eff1olem  26608  lognegb  26650  eflogeq  26662  logdivlt  26681  efopn  26718  cxpeq0  26738  cxpeq  26818  angpieqvd  26892  dcubic  26907  asinsinb  26958  acoscosb  26959  atantanb  26985  rlimcnp  27026  isppw  27175  isppw2  27176  vmappw  27177  isnsqf  27196  ppieq0  27237  fsumdvdsdiag  27245  dvdsppwf1o  27247  fsumfldivdiag  27251  chpeq0  27270  chteq0  27271  dchrptlem1  27326  lgsdir2lem4  27390  lgsne0  27397  lgsqr  27413  lgsdchrval  27416  gausslemma2dlem1a  27427  lgsquadlem1  27442  m1lgs  27450  2sqreultblem  27510  2sqreunnltblem  27513  nodenselem8  27754  sltlend  27834  oldlim  27943  sltlpss  27963  sleadd1  28040  sltneg  28095  muls0ord  28229  absslt  28291  n0subs  28378  iscgrglt  28540  brbtwn  28932  brcgr  28933  brbtwn2  28938  axcontlem7  29003  uhgr0vb  29107  edglnl  29178  ausgrusgrb  29200  ushgredgedg  29264  ushgredgedgloop  29266  usgr0vb  29272  usgr1v  29291  nbupgr  29379  nbumgrvtx  29381  nbuhgr2vtx1edgb  29387  edgusgrnbfin  29408  nb3grprlem1  29415  uvtxnbvtxm1  29441  cusgrfilem2  29492  uhgr0edg0rgrb  29610  cusgrm1rusgr  29618  spthonepeq  29788  usgr2pth  29800  wlkiswwlks  29909  wlkiswwlkupgr  29911  wlklnwwlkn  29917  wlklnwwlknupgr  29919  wwlksnextbi  29927  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  wwlksnextprop  29945  umgrwwlks2on  29990  elwspths2on  29993  usgr2wspthons3  29997  elwwlks2  29999  elwspths2spth  30000  clwlkclwwlklem3  30033  loopclwwlkn1b  30074  clwwlknon1sn  30132  clwwlknonwwlknonb  30138  umgr3v3e3cycl  30216  eupth2lem3lem4  30263  frgr0v  30294  frgr3vlem2  30306  2clwwlk2clwwlk  30382  wlkl0  30399  grpoinvf  30564  nvmul0or  30682  nvz  30701  diporthcom  30748  ubthlem3  30904  hvmul0or  31057  his6  31131  hial0  31134  hial02  31135  orthcom  31140  normgt0  31159  ocin  31328  occon3  31329  shsel3  31347  shlub  31446  chssoc  31528  h1de2bi  31586  spansncol  31600  elspansn4  31605  spansnss2  31607  sumspansn  31681  lnopcnbd  32068  lnfncnbd  32089  riesz1  32097  elpjrn  32222  cvcon3  32316  dmdmd  32332  dmdbr3  32337  dmdbr4  32338  dmdbr5  32340  mdslmd1i  32361  atcveq0  32380  chcv1  32387  atssma  32410  atcv0eq  32411  atcv1  32412  bian1dOLD  32485  disjeq1f  32595  br8d  32632  fpwrelmap  32747  xaddeq0  32760  eliccelico  32782  elicoelioo  32783  isarchiofld  33312  unitdivcld  33847  xrge0iifcnv  33879  lmxrge0  33898  indf1ofs  33990  eulerpartlemgh  34343  dstfrvunirn  34439  fnrelpredd  35065  loop1cycl  35105  cusgracyclt3v  35124  cvmliftmolem2  35250  cvmlift2lem12  35282  satfvsucsuc  35333  satfdm  35337  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem2  35374  mthmb  35549  climuzcnv  35639  br8  35718  br6  35719  br4  35720  funbreq  35733  axextbdist  35764  dfrdg4  35915  cgrcom  35954  cgrcoml  35960  cgrdegen  35968  btwncom  35978  brsegle  36072  brsegle2  36073  colinbtwnle  36082  btwnoutside  36089  broutsideof3  36090  outsidele  36096  lineunray  36111  lineelsb2  36112  elhf2  36139  elicc3  36283  nn0prpwlem  36288  opnbnd  36291  cldbnd  36292  opnregcld  36296  cldregopn  36297  fnessref  36323  refssfne  36324  neibastop2  36327  fnemeet2  36333  fnejoin2  36335  fgmin  36336  ontgval  36397  ordtop  36402  ordcmp  36413  nndivsub  36423  bj-19.21t  36735  bj-19.23t  36736  bj-19.42t  36739  bj-sbft  36741  bj-cbv2hv  36763  bj-equsal1t  36788  bj-19.21t0  36796  bj-ceqsalt0  36850  bj-ceqsalt1  36851  bj-xpnzexb  36927  bj-idreseq  37128  bj-imdiridlem  37151  bj-finsumval0  37251  bj-fvimacnv0  37252  bj-isrvec2  37266  bj-bary1  37278  dfgcd3  37290  isbasisrelowllem1  37321  isbasisrelowllem2  37322  finxpsuclem  37363  wl-lem-exsb  37520  wl-mo3t  37530  wl-ax11-lem1  37539  matunitlindf  37578  poimirlem6  37586  poimirlem7  37587  poimirlem16  37596  poimirlem19  37599  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  cnambfre  37628  itg2addnc  37634  brabg2  37677  istotbnd3  37731  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  ssbnd  37748  ismtybnd  37767  reheibor  37799  grpoeqdivid  37841  grpokerinj  37853  rngosn3  37884  rngoueqz  37900  1idl  37986  0rngo  37987  divrngidl  37988  igenval2  38026  ispridlc  38030  isdmn3  38034  relcnveq3  38277  iss2  38300  elrelscnveq3  38447  funALTVeq  38656  disjeq  38690  prtlem10  38821  prter2  38837  dral1-o  38860  lshpinN  38945  lsatcveq0  38988  lsatcv0eq  39003  lsatcv1  39004  islshpcv  39009  lkr0f  39050  lkrshp4  39064  lshpkrlem1  39066  lshpset2N  39075  lfl1dim  39077  lfl1dim2N  39078  lub0N  39145  glb0N  39149  oplecon3b  39156  cmtcomN  39205  cmtbr3N  39210  cmtbr4N  39211  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrcon3b  39233  cvrnbtwn4  39235  cvrcmp  39239  atcvreq0  39270  atnle  39273  atlatle  39276  cvlexchb1  39286  cvlcvr1  39295  hlrelat2  39360  exatleN  39361  cvrval3  39370  cvrval4N  39371  cvrexch  39377  atcvr0eq  39383  lnnat  39384  atcvrj0  39385  atcvrj2b  39389  atltcvr  39392  atbtwn  39403  ps-1  39434  3at  39447  islln2a  39474  llncmp  39479  islpln2a  39505  lplncmp  39519  islvol2aN  39549  4at  39570  lvolcmp  39574  pmaple  39718  lncmp  39740  paddss  39802  llnexchb2lem  39825  2polcon4bN  39875  ispsubcl2N  39904  lhpat3  40003  lautcvr  40049  ltrnid  40092  trlval2  40120  trlatn0  40129  ltrnideq  40132  trlnidatb  40134  cdlemeg49lebilem  40496  trlord  40526  cdlemg1a  40527  cdlemg1cex  40545  tendoid0  40782  dva1dim  40942  cdlemm10N  41075  diarnN  41086  cdlemn  41169  dihlspsnssN  41289  dihatexv  41295  dochkrshp  41343  dochkrshp4  41346  djhlsmcl  41371  lcfl6  41457  lcfl8  41459  lcfrvalsnN  41498  lcfrlem9  41507  mapdval2N  41587  mapdordlem2  41594  mapd1o  41605  mapd0  41622  mapdheq2biN  41687  nnproddivdvdsd  41957  primrootspoweq0  42063  aks6d1c1p1  42064  aks6d1c5lem1  42093  sticksstones11  42113  sticksstones22  42125  grpods  42151  unitscyglem2  42153  fnsnbt  42225  eqresfnbd  42227  expeq1d  42311  expeqidd  42312  dvdsexpnn  42320  zdivgd  42324  mulgt0b2d  42436  frlmfzowrdb  42459  frlmsnic  42495  evlselvlem  42541  prjspreln0  42564  elrfi  42650  diophrw  42715  eldioph2b  42719  diophin  42728  rexrabdioph  42750  rmxycomplete  42874  coprmdvdsb  42942  jm2.19  42950  jm2.26  42959  jm2.27  42965  limsuc2  42998  dgraa0p  43106  rngunsnply  43130  fiuneneq  43153  unielss  43179  oaabsb  43256  nnoeomeqom  43274  cantnfresb  43286  tfsconcatrn  43304  tfsconcat0b  43308  tfsconcatrev  43310  oadif1lem  43341  oadif1  43342  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  pwelg  43522  nzss  44286  dvconstbi  44303  expgrowth  44304  bcc0  44309  axc11next  44375  pm14.24  44401  sbiota1  44403  sbcim2g  44509  sineq0ALT  44908  pwssfi  44947  mapss2  45112  fsneq  45113  fsneqrn  45118  mapssbi  45120  ssmapsn  45123  rnmptbd2lem  45157  infnsuprnmpt  45159  rnmptbdlem  45164  xralrple2  45269  infxrunb2  45283  xralrple4  45288  xralrple3  45289  xrralrecnnle  45298  xrralrecnnge  45305  reclt0  45306  supxrunb3  45314  supxrleubrnmpt  45321  xrre4  45326  unb2ltle  45330  rexabslelem  45333  suprleubrnmpt  45337  infxrunb3rnmpt  45343  uzub  45346  supminfrnmpt  45360  iccintsng  45441  sqrlearg  45471  uzinico  45478  preimaiocmnf  45479  limcresiooub  45563  limclr  45576  climeldmeq  45586  limsuppnflem  45631  limsupmnflem  45641  limsupmnfuzlem  45647  limsupre3lem  45653  limsupre3uzlem  45656  liminfreuzlem  45723  dvnmul  45864  dvmptfprodlem  45865  ismbl3  45907  ismbl4  45914  fourierdlem50  46077  fourierdlem89  46116  fourierdlem91  46118  dfsalgen2  46262  sge0repnf  46307  sge0lefi  46319  sge0resplit  46327  sge0fodjrnlem  46337  voliunsge0lem  46393  hspdifhsp  46537  isvonmbl  46559  ovnovollem3  46579  vonvolmbl  46582  pimrecltpos  46629  preimaicomnf  46632  pimrecltneg  46645  issmflem  46648  issmfle  46666  issmfgt  46677  smfaddlem1  46684  issmfge  46691  smfresal  46709  smflimmpt  46731  smfinflem  46738  smflimsuplem7  46747  smflimsupmpt  46750  sigarcol  46785  confun  46854  or2expropbi  46949  fsetsniunop  46964  fcoresf1b  46985  f1cof1b  46992  funfocofob  46993  rexsb  47014  euoreqb  47024  ralbinrald  47037  rlimdmafv  47092  fafv2elrnb  47150  tz6.12c-afv2  47157  dfatbrafv2b  47160  fnbrafv2b  47163  rlimdmafv2  47173  f1oresf1o2  47206  el1fzopredsuc  47240  2ffzoeq  47242  imasetpreimafvbijlemfo  47279  iccpartiun  47308  ichnfb  47339  ich2exprop  47345  sprsymrelfolem2  47367  paireqne  47385  prprelprb  47391  reupr  47396  requad01  47495  requad1  47496  requad2  47497  dfodd6  47511  dfeven4  47512  evensumeven  47581  sbgoldbalt  47655  clnbgrel  47701  dfclnbgr6  47728  dfnbgr6  47729  isuspgrim0  47756  isuspgrim  47759  gricushgr  47770  uhgrimisgrgriclem  47782  clnbgrgrim  47786  grimedg  47787  usgrgrtrirex  47799  uspgrlimlem2  47813  uspgrlim  47816  isassintop  47933  uzlidlring  47958  rngcisoALTV  48000  ringcisoALTV  48034  domnmsuppn0  48094  lindslininds  48193  snlindsntor  48200  isldepslvec2  48214  affinecomb1  48436  prelrrx2b  48448  rrx2plord2  48456  eenglngeehlnm  48473  rrx2vlinest  48475  line2xlem  48487  line2x  48488  line2y  48489  itsclc0xyqsolb  48504  itsclquadb  48510  mpbiran3d  48530  opnneieqv  48590  iscnrm3lem2  48614  fullthinc2  48714  thincciso  48716