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  801  dedlem0b  1045  dedlema  1046  dedlemb  1047  albi  1818  alexbii  1833  equequ1  2024  equequ2  2025  spsbbi  2073  elequ1  2115  elequ2  2123  sbequ12  2251  sbft  2270  cbv2w  2339  exsb  2362  dral1v  2372  dral1vOLD  2373  cbv2  2408  cbv2h  2411  ax12b  2429  dral1  2444  dral1ALT  2445  eupickb  2635  eupickbi  2636  2eu2  2653  ralbi  3103  rexbi  3104  ralbida  3270  ceqsalt  3515  rspcebdv  3616  rspceb2dv  3626  ceqex  3652  elabgt  3672  mob2  3721  reu6  3732  sbciegftOLD  3826  sbcg  3863  2reu2  3898  csbiebt  3928  dfss2  3969  ssdifsym  4274  reupick  4329  reupick2  4331  uneqdifeq  4493  prnebg  4856  preqsnd  4859  prel12g  4864  iuneqconst  5003  disjeq2  5114  disjeq1  5117  disjss3  5142  reusv2lem2  5399  reusv2lem3  5400  alxfr  5407  ralxfrd  5408  ralxfrd2  5412  copsexgw  5495  copsexg  5496  snopeqop  5511  euotd  5518  poeq2  5596  sotric  5622  sotrieq  5623  freq2  5653  seeq1  5655  seeq2  5656  iss  6053  tz7.7  6410  ordtri1  6417  ordelinel  6485  iotavalOLD  6535  funeq  6586  funssres  6610  f0dom0  6792  tz6.12cOLD  6933  fnbrfvb  6959  ssimaex  6994  fvimacnv  7073  elpreima  7078  feldmfvelcdm  7106  eldmrexrnb  7112  fsn  7155  fnsnb  7186  fmptsng  7188  fmptsnd  7189  fprb  7214  tpres  7221  fconst2g  7223  fconst5  7226  elunirn  7271  f1ocnvfvb  7299  f1prex  7304  foeqcnvco  7320  f1eqcocnv  7321  fliftfun  7332  soisores  7347  isofr  7362  isose  7363  isopo  7366  isoso  7368  f1oiso2  7372  eusvobj2  7423  oprabidw  7462  oprabid  7463  f1opw2  7688  oneqmin  7820  ordsucOLD  7834  ordelsuc  7840  ordsucelsuc  7842  ordunisuc2  7865  limsuc  7870  fndmexb  7928  resf1ext2b  7957  f1ovv  7982  mptcnfimad  8011  op1steq  8058  opreuopreu  8059  funeldmdif  8073  fvn0elsuppb  8206  extmptsuppeq  8213  rntpos  8264  smoiso2  8409  seqomlem2  8491  oaord  8585  oawordex  8595  oaordex  8596  omord2  8605  om00  8613  oeord  8626  nnaord  8657  nnmord  8670  nnawordex  8675  nnaordex  8676  nnaordex2  8677  eldifsucnn  8702  erexb  8770  swoord1  8777  swoord2  8778  iiner  8829  eceqoveq  8862  mapsnd  8926  ralxpmap  8936  omxpenlem  9113  domtriord  9163  mapxpen  9183  mapunen  9186  ssenen  9191  enfi  9227  nneneq  9246  nndomog  9253  nneneqOLD  9258  nndomogOLD  9263  onomeneq  9265  onomeneqOLD  9266  en1eqsnbi  9310  fodomfib  9369  fodomfibOLD  9371  f1opwfi  9396  fsuppunbi  9429  elfiun  9470  suplub2  9501  ordiso2  9555  ordiso  9556  oieu  9579  brwdom2  9613  brwdom3  9622  cantnflem1  9729  ttrclselem2  9766  cardidm  9999  carddom2  10017  pm54.43  10041  pr2neOLD  10045  acnen  10093  acnen2  10095  alephord  10115  alephinit  10135  dfac5  10169  infdif2  10249  fictb  10284  coflim  10301  fincssdom  10363  fin23lem25  10364  isf32lem9  10401  isf34lem4  10417  fin1a2lem11  10450  axdc3lem2  10491  ficard  10605  fpwwe2lem11  10681  fpwwe2  10683  indpi  10947  nqereq  10975  1idpr  11069  ltapr  11085  leltne  11350  ltlen  11362  ltadd2  11365  addlsub  11679  addid0  11682  ltord1  11789  mul0or  11903  ldiv  12101  ltmul1  12117  mulge0b  12138  lt2msq  12153  nnsub  12310  nn0sub  12576  zrevaddcl  12662  zltp1le  12667  zdiv  12688  nneo  12702  zeo2  12705  zmax  12987  zbtwnre  12988  qrevaddcl  13013  xrlttri  13181  xrleltne  13187  xralrple  13247  xltneg  13259  xleadd1  13297  xlemul1  13332  supxrunb1  13361  supxrunb2  13362  ioo0  13412  iccid  13432  ico0  13433  ioc0  13434  icc0  13435  difreicc  13524  iccsplit  13525  zltaddlt1le  13545  0fz1  13584  uzsplit  13636  fzm1  13647  fzrevral  13652  ssfzo12bi  13800  elfznelfzob  13812  flge  13845  modid2  13938  modmuladd  13954  ssnn0fi  14026  seqf1olem1  14082  hashen  14386  hashdom  14418  hash2exprb  14510  pr2pwpr  14518  hashtpg  14524  hash3tpexb  14533  len0nnbi  14589  ccats1pfxeqbi  14780  reuccatpfxs1  14785  repsdf2  14816  scshwfzeqfzo  14865  relexpindlem  15102  shftlem  15107  shftuz  15108  abslt  15353  absle  15354  rexico  15392  cau3lem  15393  reusq0  15501  rlim2lt  15533  rlim3  15534  o1lo1  15573  rlimdm  15587  climshft  15612  o1dif  15666  isercolllem2  15702  isercoll  15704  zsum  15754  fsum  15756  fsum00  15834  incexclem  15872  zprod  15973  fprod  15977  dvdsval2  16293  moddvds  16301  negdvdsb  16310  dvdsnegb  16311  dvdscmulr  16322  dvdsmulcr  16323  dvdssub2  16338  dvdsaddre2b  16344  fzo0dvdseq  16360  mod2eq1n2dvds  16384  ltoddhalfle  16398  sumodd  16425  bitsf1ocnv  16481  sadcaddlem  16494  bitsuz  16511  dvdsgcdb  16582  gcdzeq  16589  dvdssqlem  16603  lcmeq0  16637  lcmdvdsb  16650  lcmfeq0b  16667  lcmf  16670  lcmfdvdsb  16680  coprmgcdb  16686  cncongr  16706  isprm2lem  16718  dvdsprime  16724  dvdsprm  16740  isprm7  16745  coprm  16748  euclemma  16750  rpexp  16759  prmdvdsncoprmbd  16764  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  pythagtrip  16872  pc2dvds  16917  pcprmpw2  16920  pcprmpw  16921  vdwapun  17012  ramtcl2  17049  firest  17477  mrieqv2d  17682  isacs2  17696  isssc  17864  setciso  18136  posasymb  18365  pleval2  18382  pltval3  18384  lublecllem  18405  joinle  18431  meetle  18445  latdisd  18542  lubun  18560  clatleglb  18563  letsr  18638  intopsn  18667  gsumval2a  18698  frmdss2  18876  isgrpid2  18994  isgrpinv  19011  f1ghm0to0  19263  symg1bas  19408  oddvdsnn0  19562  oddvds  19565  odeq  19568  odeq1  19578  gexdvds  19602  pgpfi  19623  pgpssslw  19632  fislw  19643  sylow3lem2  19646  lsmelvalm  19669  lsmlub  19682  lsmss1b  19684  lsmss2b  19686  efgs1b  19754  cyggenod  19902  cyggexb  19917  dprdfeq0  20042  ablsimpgfind  20130  ringinvnz1ne0  20297  ringinvnzdiv  20298  unitmulclb  20381  dvreq1  20411  isnzr2  20518  0ringnnzr  20525  0ring01eqbi  20532  rngciso  20638  ringciso  20672  rrgeq0  20700  domneq0  20708  drngmul0orOLD  20761  isabvd  20813  issrngd  20856  lssats2  20998  lspsneq0  21010  lsmelval2  21084  lvecvs0or  21110  lspsneq  21124  lspsneu  21125  lidl1el  21236  lidldvgen  21344  pzriprnglem10  21501  pzriprnglem11  21502  znunit  21582  psgndif  21620  ipeq0  21656  ocvsscon  21693  pjdm2  21731  obselocv  21748  islinds4  21855  psdmul  22170  ply1coe1eq  22304  cply1coe0bi  22306  mat1dimelbas  22477  cramer  22697  toponcomb  22935  tgss3  22993  clsval2  23058  isopn3  23074  elcls3  23091  opncldf1  23092  neiint  23112  neips  23121  opnneissb  23122  opnssneib  23123  opnnei  23128  tpnei  23129  opnneiid  23134  restcld  23180  restopnb  23183  tgcn  23260  tgcnp  23261  subbascn  23262  iscnp4  23271  cnpnei  23272  cncls2  23281  cncls  23282  cnntr  23283  lmss  23306  hausnei2  23361  lpcls  23372  ordtt1  23387  cmpsub  23408  tgcmp  23409  1stcelcls  23469  locfincmp  23534  kgencn2  23565  ptpjpre1  23579  upxp  23631  txcn  23634  txlm  23656  tgqtop  23720  kqfvima  23738  isr0  23745  regr1lem2  23748  hmeoopn  23774  hmeocld  23775  ptuncnv  23815  fbunfip  23877  fgss2  23882  ufilb  23914  ufprim  23917  trufil  23918  cfinufil  23936  ufildr  23939  elfm2  23956  elfm3  23958  rnelfm  23961  fmfnfmlem4  23965  fmco  23969  flimtopon  23978  flimopn  23983  fbflim2  23985  flimrest  23991  flffbas  24003  cnpflf  24009  fclstopon  24020  fclsnei  24027  fclsbas  24029  fclsfnflim  24035  fclscmp  24038  ufilcmp  24040  isfcf  24042  fcfnei  24043  cnpfcf  24049  alexsubb  24054  alexsubALT  24059  cldsubg  24119  tgphaus  24125  tgpt0  24127  tsmsgsum  24147  tsmsres  24152  xbln0  24424  blssexps  24436  blssex  24437  isxms2  24458  prdsbl  24504  neibl  24514  metss  24521  met2ndc  24536  metrest  24537  metcnp3  24553  tngngp3  24677  nmoeq0  24757  xrsxmet  24831  reconn  24850  iccpnfcnv  24975  fgcfil  25305  iscau4  25313  cfilres  25330  iunmbl2  25592  ismbf3d  25689  mbfaddlem  25695  i1faddlem  25728  i1fmullem  25729  ellimc3  25914  dvfsumlem2  26067  tdeglem4  26099  deg1nn0clb  26129  deg1lt0  26130  dvdsq1p  26202  plypf1  26251  0dgrb  26285  plymul0or  26322  taylthlem2  26416  ulmshft  26433  ulmcaulem  26437  ulmcau  26438  cosord  26573  eff1olem  26590  lognegb  26632  eflogeq  26644  logdivlt  26663  efopn  26700  cxpeq0  26720  cxpeq  26800  angpieqvd  26874  dcubic  26889  asinsinb  26940  acoscosb  26941  atantanb  26967  rlimcnp  27008  isppw  27157  isppw2  27158  vmappw  27159  isnsqf  27178  ppieq0  27219  fsumdvdsdiag  27227  dvdsppwf1o  27229  fsumfldivdiag  27233  chpeq0  27252  chteq0  27253  dchrptlem1  27308  lgsdir2lem4  27372  lgsne0  27379  lgsqr  27395  lgsdchrval  27398  gausslemma2dlem1a  27409  lgsquadlem1  27424  m1lgs  27432  2sqreultblem  27492  2sqreunnltblem  27495  nodenselem8  27736  sltlend  27816  oldlim  27925  sltlpss  27945  sleadd1  28022  sltneg  28077  muls0ord  28211  absslt  28273  n0subs  28360  iscgrglt  28522  brbtwn  28914  brcgr  28915  brbtwn2  28920  axcontlem7  28985  uhgr0vb  29089  edglnl  29160  ausgrusgrb  29182  ushgredgedg  29246  ushgredgedgloop  29248  usgr0vb  29254  usgr1v  29273  nbupgr  29361  nbumgrvtx  29363  nbuhgr2vtx1edgb  29369  edgusgrnbfin  29390  nb3grprlem1  29397  uvtxnbvtxm1  29423  cusgrfilem2  29474  uhgr0edg0rgrb  29592  cusgrm1rusgr  29600  spthonepeq  29772  usgr2pth  29784  wlkiswwlks  29896  wlkiswwlkupgr  29898  wlklnwwlkn  29904  wlklnwwlknupgr  29906  wwlksnextbi  29914  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  wwlksnextprop  29932  umgrwwlks2on  29977  elwspths2on  29980  usgr2wspthons3  29984  elwwlks2  29986  elwspths2spth  29987  clwlkclwwlklem3  30020  loopclwwlkn1b  30061  clwwlknon1sn  30119  clwwlknonwwlknonb  30125  umgr3v3e3cycl  30203  eupth2lem3lem4  30250  frgr0v  30281  frgr3vlem2  30293  2clwwlk2clwwlk  30369  wlkl0  30386  grpoinvf  30551  nvmul0or  30669  nvz  30688  diporthcom  30735  ubthlem3  30891  hvmul0or  31044  his6  31118  hial0  31121  hial02  31122  orthcom  31127  normgt0  31146  ocin  31315  occon3  31316  shsel3  31334  shlub  31433  chssoc  31515  h1de2bi  31573  spansncol  31587  elspansn4  31592  spansnss2  31594  sumspansn  31668  lnopcnbd  32055  lnfncnbd  32076  riesz1  32084  elpjrn  32209  cvcon3  32303  dmdmd  32319  dmdbr3  32324  dmdbr4  32325  dmdbr5  32327  mdslmd1i  32348  atcveq0  32367  chcv1  32374  atssma  32397  atcv0eq  32398  atcv1  32399  bian1dOLD  32476  disjeq1f  32586  br8d  32622  fpwrelmap  32744  xaddeq0  32757  eliccelico  32779  elicoelioo  32780  indf1ofs  32851  isarchiofld  33347  unitdivcld  33900  xrge0iifcnv  33932  lmxrge0  33951  eulerpartlemgh  34380  dstfrvunirn  34477  fnrelpredd  35103  loop1cycl  35142  cusgracyclt3v  35161  cvmliftmolem2  35287  cvmlift2lem12  35319  satfvsucsuc  35370  satfdm  35374  fmlasuc  35391  satffunlem1lem2  35408  satffunlem2lem2  35411  mthmb  35586  climuzcnv  35676  br8  35756  br6  35757  br4  35758  funbreq  35770  axextbdist  35801  dfrdg4  35952  cgrcom  35991  cgrcoml  35997  cgrdegen  36005  btwncom  36015  brsegle  36109  brsegle2  36110  colinbtwnle  36119  btwnoutside  36126  broutsideof3  36127  outsidele  36133  lineunray  36148  lineelsb2  36149  elhf2  36176  elicc3  36318  nn0prpwlem  36323  opnbnd  36326  cldbnd  36327  opnregcld  36331  cldregopn  36332  fnessref  36358  refssfne  36359  neibastop2  36362  fnemeet2  36368  fnejoin2  36370  fgmin  36371  ontgval  36432  ordtop  36437  ordcmp  36448  nndivsub  36458  bj-19.21t  36770  bj-19.23t  36771  bj-19.42t  36774  bj-sbft  36776  bj-cbv2hv  36798  bj-equsal1t  36823  bj-19.21t0  36831  bj-ceqsalt0  36885  bj-ceqsalt1  36886  bj-xpnzexb  36962  bj-idreseq  37163  bj-imdiridlem  37186  bj-finsumval0  37286  bj-fvimacnv0  37287  bj-isrvec2  37301  bj-bary1  37313  dfgcd3  37325  isbasisrelowllem1  37356  isbasisrelowllem2  37357  finxpsuclem  37398  wl-lem-exsb  37567  wl-mo3t  37577  wl-ax11-lem1  37586  matunitlindf  37625  poimirlem6  37633  poimirlem7  37634  poimirlem16  37643  poimirlem19  37646  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  cnambfre  37675  itg2addnc  37681  brabg2  37724  istotbnd3  37778  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  ssbnd  37795  ismtybnd  37814  reheibor  37846  grpoeqdivid  37888  grpokerinj  37900  rngosn3  37931  rngoueqz  37947  1idl  38033  0rngo  38034  divrngidl  38035  igenval2  38073  ispridlc  38077  isdmn3  38081  relcnveq3  38322  iss2  38345  elrelscnveq3  38492  funALTVeq  38701  disjeq  38735  prtlem10  38866  prter2  38882  dral1-o  38905  lshpinN  38990  lsatcveq0  39033  lsatcv0eq  39048  lsatcv1  39049  islshpcv  39054  lkr0f  39095  lkrshp4  39109  lshpkrlem1  39111  lshpset2N  39120  lfl1dim  39122  lfl1dim2N  39123  lub0N  39190  glb0N  39194  oplecon3b  39201  cmtcomN  39250  cmtbr3N  39255  cmtbr4N  39256  cvrnbtwn2  39276  cvrnbtwn3  39277  cvrcon3b  39278  cvrnbtwn4  39280  cvrcmp  39284  atcvreq0  39315  atnle  39318  atlatle  39321  cvlexchb1  39331  cvlcvr1  39340  hlrelat2  39405  exatleN  39406  cvrval3  39415  cvrval4N  39416  cvrexch  39422  atcvr0eq  39428  lnnat  39429  atcvrj0  39430  atcvrj2b  39434  atltcvr  39437  atbtwn  39448  ps-1  39479  3at  39492  islln2a  39519  llncmp  39524  islpln2a  39550  lplncmp  39564  islvol2aN  39594  4at  39615  lvolcmp  39619  pmaple  39763  lncmp  39785  paddss  39847  llnexchb2lem  39870  2polcon4bN  39920  ispsubcl2N  39949  lhpat3  40048  lautcvr  40094  ltrnid  40137  trlval2  40165  trlatn0  40174  ltrnideq  40177  trlnidatb  40179  cdlemeg49lebilem  40541  trlord  40571  cdlemg1a  40572  cdlemg1cex  40590  tendoid0  40827  dva1dim  40987  cdlemm10N  41120  diarnN  41131  cdlemn  41214  dihlspsnssN  41334  dihatexv  41340  dochkrshp  41388  dochkrshp4  41391  djhlsmcl  41416  lcfl6  41502  lcfl8  41504  lcfrvalsnN  41543  lcfrlem9  41552  mapdval2N  41632  mapdordlem2  41639  mapd1o  41650  mapd0  41667  mapdheq2biN  41732  nnproddivdvdsd  42001  primrootspoweq0  42107  aks6d1c1p1  42108  aks6d1c5lem1  42137  sticksstones11  42157  sticksstones22  42169  grpods  42195  unitscyglem2  42197  fnsnbt  42271  eqresfnbd  42273  expeq1d  42359  expeqidd  42360  dvdsexpnn  42368  zdivgd  42372  mulgt0b2d  42490  frlmfzowrdb  42514  frlmsnic  42550  evlselvlem  42596  prjspreln0  42619  elrfi  42705  diophrw  42770  eldioph2b  42774  diophin  42783  rexrabdioph  42805  rmxycomplete  42929  coprmdvdsb  42997  jm2.19  43005  jm2.26  43014  jm2.27  43020  limsuc2  43053  dgraa0p  43161  rngunsnply  43181  fiuneneq  43204  unielss  43230  oaabsb  43307  nnoeomeqom  43325  cantnfresb  43337  tfsconcatrn  43355  tfsconcat0b  43359  tfsconcatrev  43361  oadif1lem  43392  oadif1  43393  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  pwelg  43573  nzss  44336  dvconstbi  44353  expgrowth  44354  bcc0  44359  axc11next  44425  pm14.24  44451  sbiota1  44453  sbcim2g  44558  sineq0ALT  44957  mapss2  45210  fsneq  45211  fsneqrn  45216  mapssbi  45218  rnmptbd2lem  45255  infnsuprnmpt  45257  rnmptbdlem  45262  xralrple2  45365  infxrunb2  45379  xralrple4  45384  xralrple3  45385  xrralrecnnle  45394  xrralrecnnge  45401  reclt0  45402  supxrunb3  45410  supxrleubrnmpt  45417  xrre4  45422  unb2ltle  45426  rexabslelem  45429  suprleubrnmpt  45433  infxrunb3rnmpt  45439  uzub  45442  supminfrnmpt  45456  iccintsng  45536  sqrlearg  45566  uzinico  45573  preimaiocmnf  45574  limcresiooub  45657  limclr  45670  climeldmeq  45680  limsuppnflem  45725  limsupmnflem  45735  limsupmnfuzlem  45741  limsupre3lem  45747  limsupre3uzlem  45750  liminfreuzlem  45817  dvnmul  45958  dvmptfprodlem  45959  ismbl3  46001  ismbl4  46008  fourierdlem50  46171  fourierdlem89  46210  fourierdlem91  46212  dfsalgen2  46356  sge0repnf  46401  sge0lefi  46413  sge0resplit  46421  sge0fodjrnlem  46431  voliunsge0lem  46487  hspdifhsp  46631  isvonmbl  46653  ovnovollem3  46673  vonvolmbl  46676  pimrecltpos  46723  preimaicomnf  46726  pimrecltneg  46739  issmflem  46742  issmfle  46760  issmfgt  46771  smfaddlem1  46778  issmfge  46785  smfresal  46803  smflimmpt  46825  smfinflem  46832  smflimsuplem7  46841  smflimsupmpt  46844  sigarcol  46879  confun  46951  or2expropbi  47046  fsetsniunop  47061  fcoresf1b  47082  f1cof1b  47089  funfocofob  47090  rexsb  47111  euoreqb  47121  ralbinrald  47134  rlimdmafv  47189  fafv2elrnb  47247  tz6.12c-afv2  47254  dfatbrafv2b  47257  fnbrafv2b  47260  rlimdmafv2  47270  f1oresf1o2  47303  el1fzopredsuc  47337  2ffzoeq  47339  imasetpreimafvbijlemfo  47392  iccpartiun  47421  ichnfb  47452  ich2exprop  47458  sprsymrelfolem2  47480  paireqne  47498  prprelprb  47504  reupr  47509  requad01  47608  requad1  47609  requad2  47610  dfodd6  47624  dfeven4  47625  evensumeven  47694  sbgoldbalt  47768  clnbgrel  47815  dfclnbgr6  47842  dfnbgr6  47843  isubgredg  47852  isuspgrim0  47872  isuspgrim  47875  gricushgr  47886  uhgrimisgrgriclem  47898  clnbgrgrim  47902  grimedg  47903  usgrgrtrirex  47917  uspgrlimlem2  47956  uspgrlim  47959  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  isassintop  48126  uzlidlring  48151  rngcisoALTV  48193  ringcisoALTV  48227  domnmsuppn0  48285  lindslininds  48381  snlindsntor  48388  isldepslvec2  48402  affinecomb1  48623  prelrrx2b  48635  rrx2plord2  48643  eenglngeehlnm  48660  rrx2vlinest  48662  line2xlem  48674  line2x  48675  line2y  48676  itsclc0xyqsolb  48691  itsclquadb  48697  mpbiran3d  48717  opnneieqv  48808  iscnrm3lem2  48832  fullthinc2  49100  thincciso  49102