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  2024  equequ2  2025  spsbbi  2073  elequ1  2115  elequ2  2123  sbequ12  2251  sbft  2270  cbv2w  2338  exsb  2361  dral1v  2371  dral1vOLD  2372  cbv2  2407  cbv2h  2410  ax12b  2428  dral1  2443  dral1ALT  2444  eupickb  2634  eupickbi  2635  2eu2  2652  ralbi  3092  rexbi  3093  ralbida  3253  ceqsalt  3494  rspcebdv  3595  rspceb2dv  3605  ceqex  3631  elabgt  3651  mob2  3698  reu6  3709  sbciegftOLD  3803  sbcg  3838  2reu2  3873  csbiebt  3903  dfss2  3944  ssdifsym  4249  reupick  4304  reupick2  4306  uneqdifeq  4468  prnebg  4832  preqsnd  4835  prel12g  4840  iuneqconst  4979  disjeq2  5090  disjeq1  5093  disjss3  5118  reusv2lem2  5369  reusv2lem3  5370  alxfr  5377  ralxfrd  5378  ralxfrd2  5382  copsexgw  5465  copsexg  5466  snopeqop  5481  euotd  5488  poeq2  5565  sotric  5591  sotrieq  5592  freq2  5622  seeq1  5624  seeq2  5625  iss  6022  tz7.7  6378  ordtri1  6385  ordelinel  6454  iotavalOLD  6504  funeq  6555  funssres  6579  f0dom0  6761  tz6.12cOLD  6902  fnbrfvb  6928  ssimaex  6963  fvimacnv  7042  elpreima  7047  feldmfvelcdm  7075  eldmrexrnb  7081  fsn  7124  fnsnbg  7155  fnsnbOLD  7157  fmptsng  7159  fmptsnd  7160  fprb  7185  tpres  7192  fconst2g  7194  fconst5  7197  elunirn  7242  f1ocnvfvb  7271  f1prex  7276  foeqcnvco  7292  f1eqcocnv  7293  fliftfun  7304  soisores  7319  isofr  7334  isose  7335  isopo  7338  isoso  7340  f1oiso2  7344  eusvobj2  7395  oprabidw  7434  oprabid  7435  f1opw2  7660  oneqmin  7792  ordsucOLD  7806  ordelsuc  7812  ordsucelsuc  7814  ordunisuc2  7837  limsuc  7842  fndmexb  7900  resf1ext2b  7929  f1ovv  7954  mptcnfimad  7983  op1steq  8030  opreuopreu  8031  funeldmdif  8045  fvn0elsuppb  8178  extmptsuppeq  8185  rntpos  8236  smoiso2  8381  seqomlem2  8463  oaord  8557  oawordex  8567  oaordex  8568  omord2  8577  om00  8585  oeord  8598  nnaord  8629  nnmord  8642  nnawordex  8647  nnaordex  8648  nnaordex2  8649  eldifsucnn  8674  erexb  8742  swoord1  8749  swoord2  8750  iiner  8801  eceqoveq  8834  mapsnd  8898  ralxpmap  8908  omxpenlem  9085  domtriord  9135  mapxpen  9155  mapunen  9158  ssenen  9163  enfi  9199  nneneq  9218  nndomog  9225  nndomogOLD  9233  onomeneq  9235  onomeneqOLD  9236  en1eqsnbi  9280  fodomfib  9339  fodomfibOLD  9341  f1opwfi  9366  fsuppunbi  9399  elfiun  9440  suplub2  9471  ordiso2  9527  ordiso  9528  oieu  9551  brwdom2  9585  brwdom3  9594  cantnflem1  9701  ttrclselem2  9738  cardidm  9971  carddom2  9989  pm54.43  10013  pr2neOLD  10017  acnen  10065  acnen2  10067  alephord  10087  alephinit  10107  dfac5  10141  infdif2  10221  fictb  10256  coflim  10273  fincssdom  10335  fin23lem25  10336  isf32lem9  10373  isf34lem4  10389  fin1a2lem11  10422  axdc3lem2  10463  ficard  10577  fpwwe2lem11  10653  fpwwe2  10655  indpi  10919  nqereq  10947  1idpr  11041  ltapr  11057  leltne  11322  ltlen  11334  ltadd2  11337  addlsub  11651  addid0  11654  ltord1  11761  mul0or  11875  ldiv  12073  ltmul1  12089  mulge0b  12110  lt2msq  12125  nnsub  12282  nn0sub  12549  zrevaddcl  12635  zltp1le  12640  zdiv  12661  nneo  12675  zeo2  12678  zmax  12959  zbtwnre  12960  qrevaddcl  12985  xrlttri  13153  xrleltne  13159  xralrple  13219  xltneg  13231  xleadd1  13269  xlemul1  13304  supxrunb1  13333  supxrunb2  13334  ioo0  13385  iccid  13405  ico0  13406  ioc0  13407  icc0  13408  difreicc  13499  iccsplit  13500  zltaddlt1le  13520  0fz1  13559  uzsplit  13611  fzm1  13622  fzrevral  13627  ssfzo12bi  13775  elfznelfzob  13787  flge  13820  modid2  13913  modmuladd  13929  ssnn0fi  14001  seqf1olem1  14057  hashen  14363  hashdom  14395  hash2exprb  14487  pr2pwpr  14495  hashtpg  14501  hash3tpexb  14510  len0nnbi  14567  ccats1pfxeqbi  14758  reuccatpfxs1  14763  repsdf2  14794  scshwfzeqfzo  14843  relexpindlem  15080  shftlem  15085  shftuz  15086  abslt  15331  absle  15332  rexico  15370  cau3lem  15371  reusq0  15479  rlim2lt  15511  rlim3  15512  o1lo1  15551  rlimdm  15565  climshft  15590  o1dif  15644  isercolllem2  15680  isercoll  15682  zsum  15732  fsum  15734  fsum00  15812  incexclem  15850  zprod  15951  fprod  15955  dvdsval2  16273  moddvds  16281  negdvdsb  16290  dvdsnegb  16291  dvdscmulr  16302  dvdsmulcr  16303  dvdssub2  16318  dvdsaddre2b  16324  fzo0dvdseq  16340  mod2eq1n2dvds  16364  ltoddhalfle  16378  sumodd  16405  bitsf1ocnv  16461  sadcaddlem  16474  bitsuz  16491  dvdsgcdb  16562  gcdzeq  16569  dvdssqlem  16583  lcmeq0  16617  lcmdvdsb  16630  lcmfeq0b  16647  lcmf  16650  lcmfdvdsb  16660  coprmgcdb  16666  cncongr  16686  isprm2lem  16698  dvdsprime  16704  dvdsprm  16720  isprm7  16725  coprm  16728  euclemma  16730  rpexp  16739  prmdvdsncoprmbd  16744  prmdiveq  16803  hashgcdlem  16805  odzdvds  16813  pythagtrip  16852  pc2dvds  16897  pcprmpw2  16900  pcprmpw  16901  vdwapun  16992  ramtcl2  17029  firest  17444  mrieqv2d  17649  isacs2  17663  isssc  17831  setciso  18102  posasymb  18329  pleval2  18345  pltval3  18347  lublecllem  18368  joinle  18394  meetle  18408  latdisd  18505  lubun  18523  clatleglb  18526  letsr  18601  intopsn  18630  gsumval2a  18661  frmdss2  18839  isgrpid2  18957  isgrpinv  18974  f1ghm0to0  19226  symg1bas  19370  oddvdsnn0  19523  oddvds  19526  odeq  19529  odeq1  19539  gexdvds  19563  pgpfi  19584  pgpssslw  19593  fislw  19604  sylow3lem2  19607  lsmelvalm  19630  lsmlub  19643  lsmss1b  19645  lsmss2b  19647  efgs1b  19715  cyggenod  19863  cyggexb  19878  dprdfeq0  20003  ablsimpgfind  20091  ringinvnz1ne0  20258  ringinvnzdiv  20259  unitmulclb  20339  dvreq1  20369  isnzr2  20476  0ringnnzr  20483  0ring01eqbi  20490  rngciso  20596  ringciso  20630  rrgeq0  20658  domneq0  20666  drngmul0orOLD  20719  isabvd  20770  issrngd  20813  lssats2  20955  lspsneq0  20967  lsmelval2  21041  lvecvs0or  21067  lspsneq  21081  lspsneu  21082  lidl1el  21185  lidldvgen  21293  pzriprnglem10  21449  pzriprnglem11  21450  znunit  21522  psgndif  21560  ipeq0  21596  ocvsscon  21633  pjdm2  21669  obselocv  21686  islinds4  21793  psdmul  22102  ply1coe1eq  22236  cply1coe0bi  22238  mat1dimelbas  22407  cramer  22627  toponcomb  22865  tgss3  22922  clsval2  22986  isopn3  23002  elcls3  23019  opncldf1  23020  neiint  23040  neips  23049  opnneissb  23050  opnssneib  23051  opnnei  23056  tpnei  23057  opnneiid  23062  restcld  23108  restopnb  23111  tgcn  23188  tgcnp  23189  subbascn  23190  iscnp4  23199  cnpnei  23200  cncls2  23209  cncls  23210  cnntr  23211  lmss  23234  hausnei2  23289  lpcls  23300  ordtt1  23315  cmpsub  23336  tgcmp  23337  1stcelcls  23397  locfincmp  23462  kgencn2  23493  ptpjpre1  23507  upxp  23559  txcn  23562  txlm  23584  tgqtop  23648  kqfvima  23666  isr0  23673  regr1lem2  23676  hmeoopn  23702  hmeocld  23703  ptuncnv  23743  fbunfip  23805  fgss2  23810  ufilb  23842  ufprim  23845  trufil  23846  cfinufil  23864  ufildr  23867  elfm2  23884  elfm3  23886  rnelfm  23889  fmfnfmlem4  23893  fmco  23897  flimtopon  23906  flimopn  23911  fbflim2  23913  flimrest  23919  flffbas  23931  cnpflf  23937  fclstopon  23948  fclsnei  23955  fclsbas  23957  fclsfnflim  23963  fclscmp  23966  ufilcmp  23968  isfcf  23970  fcfnei  23971  cnpfcf  23977  alexsubb  23982  alexsubALT  23987  cldsubg  24047  tgphaus  24053  tgpt0  24055  tsmsgsum  24075  tsmsres  24080  xbln0  24351  blssexps  24363  blssex  24364  isxms2  24385  prdsbl  24428  neibl  24438  metss  24445  met2ndc  24460  metrest  24461  metcnp3  24477  tngngp3  24593  nmoeq0  24673  xrsxmet  24747  reconn  24766  iccpnfcnv  24891  fgcfil  25221  iscau4  25229  cfilres  25246  iunmbl2  25508  ismbf3d  25605  mbfaddlem  25611  i1faddlem  25644  i1fmullem  25645  ellimc3  25830  dvfsumlem2  25983  tdeglem4  26015  deg1nn0clb  26045  deg1lt0  26046  dvdsq1p  26118  plypf1  26167  0dgrb  26201  plymul0or  26238  taylthlem2  26332  ulmshft  26349  ulmcaulem  26353  ulmcau  26354  cosord  26490  eff1olem  26507  lognegb  26549  eflogeq  26561  logdivlt  26580  efopn  26617  cxpeq0  26637  cxpeq  26717  angpieqvd  26791  dcubic  26806  asinsinb  26857  acoscosb  26858  atantanb  26884  rlimcnp  26925  isppw  27074  isppw2  27075  vmappw  27076  isnsqf  27095  ppieq0  27136  fsumdvdsdiag  27144  dvdsppwf1o  27146  fsumfldivdiag  27150  chpeq0  27169  chteq0  27170  dchrptlem1  27225  lgsdir2lem4  27289  lgsne0  27296  lgsqr  27312  lgsdchrval  27315  gausslemma2dlem1a  27326  lgsquadlem1  27341  m1lgs  27349  2sqreultblem  27409  2sqreunnltblem  27412  nodenselem8  27653  sltlend  27733  oldlim  27842  sltlpss  27862  sleadd1  27939  sltneg  27994  muls0ord  28128  absslt  28190  n0subs  28277  iscgrglt  28439  brbtwn  28824  brcgr  28825  brbtwn2  28830  axcontlem7  28895  uhgr0vb  28997  edglnl  29068  ausgrusgrb  29090  ushgredgedg  29154  ushgredgedgloop  29156  usgr0vb  29162  usgr1v  29181  nbupgr  29269  nbumgrvtx  29271  nbuhgr2vtx1edgb  29277  edgusgrnbfin  29298  nb3grprlem1  29305  uvtxnbvtxm1  29331  cusgrfilem2  29382  uhgr0edg0rgrb  29500  cusgrm1rusgr  29508  spthonepeq  29680  usgr2pth  29692  wlkiswwlks  29804  wlkiswwlkupgr  29806  wlklnwwlkn  29812  wlklnwwlknupgr  29814  wwlksnextbi  29822  wwlksnredwwlkn0  29824  wwlksnextwrd  29825  wwlksnextprop  29840  umgrwwlks2on  29885  elwspths2on  29888  usgr2wspthons3  29892  elwwlks2  29894  elwspths2spth  29895  clwlkclwwlklem3  29928  loopclwwlkn1b  29969  clwwlknon1sn  30027  clwwlknonwwlknonb  30033  umgr3v3e3cycl  30111  eupth2lem3lem4  30158  frgr0v  30189  frgr3vlem2  30201  2clwwlk2clwwlk  30277  wlkl0  30294  grpoinvf  30459  nvmul0or  30577  nvz  30596  diporthcom  30643  ubthlem3  30799  hvmul0or  30952  his6  31026  hial0  31029  hial02  31030  orthcom  31035  normgt0  31054  ocin  31223  occon3  31224  shsel3  31242  shlub  31341  chssoc  31423  h1de2bi  31481  spansncol  31495  elspansn4  31500  spansnss2  31502  sumspansn  31576  lnopcnbd  31963  lnfncnbd  31984  riesz1  31992  elpjrn  32117  cvcon3  32211  dmdmd  32227  dmdbr3  32232  dmdbr4  32233  dmdbr5  32235  mdslmd1i  32256  atcveq0  32275  chcv1  32282  atssma  32305  atcv0eq  32306  atcv1  32307  bian1dOLD  32384  disjeq1f  32500  br8d  32536  fpwrelmap  32656  xaddeq0  32676  eliccelico  32700  elicoelioo  32701  indf1ofs  32789  isarchiofld  33285  unitdivcld  33878  xrge0iifcnv  33910  lmxrge0  33929  eulerpartlemgh  34356  dstfrvunirn  34453  fnrelpredd  35066  loop1cycl  35105  cusgracyclt3v  35124  cvmliftmolem2  35250  cvmlift2lem12  35282  satfvsucsuc  35333  satfdm  35337  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem2  35374  mthmb  35549  climuzcnv  35639  br8  35719  br6  35720  br4  35721  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  36281  nn0prpwlem  36286  opnbnd  36289  cldbnd  36290  opnregcld  36294  cldregopn  36295  fnessref  36321  refssfne  36322  neibastop2  36325  fnemeet2  36331  fnejoin2  36333  fgmin  36334  ontgval  36395  ordtop  36400  ordcmp  36411  nndivsub  36421  bj-19.21t  36733  bj-19.23t  36734  bj-19.42t  36737  bj-sbft  36739  bj-cbv2hv  36761  bj-equsal1t  36786  bj-19.21t0  36794  bj-ceqsalt0  36848  bj-ceqsalt1  36849  bj-xpnzexb  36925  bj-idreseq  37126  bj-imdiridlem  37149  bj-finsumval0  37249  bj-fvimacnv0  37250  bj-isrvec2  37264  bj-bary1  37276  dfgcd3  37288  isbasisrelowllem1  37319  isbasisrelowllem2  37320  finxpsuclem  37361  wl-lem-exsb  37530  wl-mo3t  37540  wl-ax11-lem1  37549  matunitlindf  37588  poimirlem6  37596  poimirlem7  37597  poimirlem16  37606  poimirlem19  37609  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  cnambfre  37638  itg2addnc  37644  brabg2  37687  istotbnd3  37741  sstotbnd2  37744  sstotbnd  37745  sstotbnd3  37746  ssbnd  37758  ismtybnd  37777  reheibor  37809  grpoeqdivid  37851  grpokerinj  37863  rngosn3  37894  rngoueqz  37910  1idl  37996  0rngo  37997  divrngidl  37998  igenval2  38036  ispridlc  38040  isdmn3  38044  relcnveq3  38285  iss2  38308  elrelscnveq3  38455  funALTVeq  38664  disjeq  38698  prtlem10  38829  prter2  38845  dral1-o  38868  lshpinN  38953  lsatcveq0  38996  lsatcv0eq  39011  lsatcv1  39012  islshpcv  39017  lkr0f  39058  lkrshp4  39072  lshpkrlem1  39074  lshpset2N  39083  lfl1dim  39085  lfl1dim2N  39086  lub0N  39153  glb0N  39157  oplecon3b  39164  cmtcomN  39213  cmtbr3N  39218  cmtbr4N  39219  cvrnbtwn2  39239  cvrnbtwn3  39240  cvrcon3b  39241  cvrnbtwn4  39243  cvrcmp  39247  atcvreq0  39278  atnle  39281  atlatle  39284  cvlexchb1  39294  cvlcvr1  39303  hlrelat2  39368  exatleN  39369  cvrval3  39378  cvrval4N  39379  cvrexch  39385  atcvr0eq  39391  lnnat  39392  atcvrj0  39393  atcvrj2b  39397  atltcvr  39400  atbtwn  39411  ps-1  39442  3at  39455  islln2a  39482  llncmp  39487  islpln2a  39513  lplncmp  39527  islvol2aN  39557  4at  39578  lvolcmp  39582  pmaple  39726  lncmp  39748  paddss  39810  llnexchb2lem  39833  2polcon4bN  39883  ispsubcl2N  39912  lhpat3  40011  lautcvr  40057  ltrnid  40100  trlval2  40128  trlatn0  40137  ltrnideq  40140  trlnidatb  40142  cdlemeg49lebilem  40504  trlord  40534  cdlemg1a  40535  cdlemg1cex  40553  tendoid0  40790  dva1dim  40950  cdlemm10N  41083  diarnN  41094  cdlemn  41177  dihlspsnssN  41297  dihatexv  41303  dochkrshp  41351  dochkrshp4  41354  djhlsmcl  41379  lcfl6  41465  lcfl8  41467  lcfrvalsnN  41506  lcfrlem9  41515  mapdval2N  41595  mapdordlem2  41602  mapd1o  41613  mapd0  41630  mapdheq2biN  41695  nnproddivdvdsd  41959  primrootspoweq0  42065  aks6d1c1p1  42066  aks6d1c5lem1  42095  sticksstones11  42115  sticksstones22  42127  grpods  42153  unitscyglem2  42155  eqresfnbd  42230  expeq1d  42320  expeqidd  42321  dvdsexpnn  42329  zdivgd  42333  mulgt0b2d  42450  frlmfzowrdb  42474  frlmsnic  42510  evlselvlem  42556  prjspreln0  42579  elrfi  42664  diophrw  42729  eldioph2b  42733  diophin  42742  rexrabdioph  42764  rmxycomplete  42888  coprmdvdsb  42956  jm2.19  42964  jm2.26  42973  jm2.27  42979  limsuc2  43012  dgraa0p  43120  rngunsnply  43140  fiuneneq  43163  unielss  43189  oaabsb  43265  nnoeomeqom  43283  cantnfresb  43295  tfsconcatrn  43313  tfsconcat0b  43317  tfsconcatrev  43319  oadif1lem  43350  oadif1  43351  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  pwelg  43531  nzss  44289  dvconstbi  44306  expgrowth  44307  bcc0  44312  axc11next  44378  pm14.24  44404  sbiota1  44406  sbcim2g  44511  sineq0ALT  44909  mapss2  45177  fsneq  45178  fsneqrn  45183  mapssbi  45185  rnmptbd2lem  45220  infnsuprnmpt  45222  rnmptbdlem  45227  xralrple2  45329  infxrunb2  45343  xralrple4  45348  xralrple3  45349  xrralrecnnle  45358  xrralrecnnge  45365  reclt0  45366  supxrunb3  45374  supxrleubrnmpt  45381  xrre4  45386  unb2ltle  45390  rexabslelem  45393  suprleubrnmpt  45397  infxrunb3rnmpt  45403  uzub  45406  supminfrnmpt  45420  iccintsng  45500  sqrlearg  45530  uzinico  45536  preimaiocmnf  45537  limcresiooub  45619  limclr  45632  climeldmeq  45642  limsuppnflem  45687  limsupmnflem  45697  limsupmnfuzlem  45703  limsupre3lem  45709  limsupre3uzlem  45712  liminfreuzlem  45779  dvnmul  45920  dvmptfprodlem  45921  ismbl3  45963  ismbl4  45970  fourierdlem50  46133  fourierdlem89  46172  fourierdlem91  46174  dfsalgen2  46318  sge0repnf  46363  sge0lefi  46375  sge0resplit  46383  sge0fodjrnlem  46393  voliunsge0lem  46449  hspdifhsp  46593  isvonmbl  46615  ovnovollem3  46635  vonvolmbl  46638  pimrecltpos  46685  preimaicomnf  46688  pimrecltneg  46701  issmflem  46704  issmfle  46722  issmfgt  46733  smfaddlem1  46740  issmfge  46747  smfresal  46765  smflimmpt  46787  smfinflem  46794  smflimsuplem7  46803  smflimsupmpt  46806  sigarcol  46841  confun  46916  or2expropbi  47011  fsetsniunop  47026  fcoresf1b  47047  f1cof1b  47054  funfocofob  47055  rexsb  47076  euoreqb  47086  ralbinrald  47099  rlimdmafv  47154  fafv2elrnb  47212  tz6.12c-afv2  47219  dfatbrafv2b  47222  fnbrafv2b  47225  rlimdmafv2  47235  f1oresf1o2  47268  el1fzopredsuc  47302  2ffzoeq  47304  imasetpreimafvbijlemfo  47367  iccpartiun  47396  ichnfb  47427  ich2exprop  47433  sprsymrelfolem2  47455  paireqne  47473  prprelprb  47479  reupr  47484  requad01  47583  requad1  47584  requad2  47585  dfodd6  47599  dfeven4  47600  evensumeven  47669  sbgoldbalt  47743  clnbgrel  47790  dfclnbgr6  47817  dfnbgr6  47818  isubgredg  47827  isuspgrim0  47855  isuspgrim  47857  gricushgr  47878  uhgrimisgrgriclem  47891  clnbgrgrim  47895  grimedg  47896  usgrgrtrirex  47910  uspgrlimlem2  47949  uspgrlim  47952  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  isassintop  48133  uzlidlring  48158  rngcisoALTV  48200  ringcisoALTV  48234  domnmsuppn0  48292  lindslininds  48388  snlindsntor  48395  isldepslvec2  48409  affinecomb1  48630  prelrrx2b  48642  rrx2plord2  48650  eenglngeehlnm  48667  rrx2vlinest  48669  line2xlem  48681  line2x  48682  line2y  48683  itsclc0xyqsolb  48698  itsclquadb  48704  mpbiran3d  48724  opnneieqv  48833  iscnrm3lem2  48857  fullthinc2  49285  thincciso  49287