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  641  impbida  801  dedlem0b  1044  dedlema  1045  dedlemb  1046  albi  1814  alexbii  1829  equequ1  2021  equequ2  2022  spsbbi  2070  elequ1  2112  elequ2  2120  sbequ12  2248  sbft  2267  cbv2w  2337  exsb  2359  dral1v  2369  dral1vOLD  2370  cbv2  2405  cbv2h  2408  ax12b  2426  dral1  2441  dral1ALT  2442  eupickb  2632  eupickbi  2633  2eu2  2650  ralbi  3100  rexbi  3101  ralbida  3267  ceqsalt  3512  rspcebdv  3615  rspceb2dv  3625  ceqex  3651  elabgt  3671  mob2  3723  reu6  3734  sbciegftOLD  3829  sbcg  3869  2reu2  3906  csbiebt  3937  dfss2  3980  sseq1  4020  ssdifsym  4279  reupick  4334  reupick2  4336  uneqdifeq  4498  prnebg  4860  preqsnd  4863  prel12g  4868  iuneqconst  5007  disjeq2  5118  disjeq1  5121  disjss3  5146  reusv2lem2  5404  reusv2lem3  5405  alxfr  5412  ralxfrd  5413  ralxfrd2  5417  copsexgw  5500  copsexg  5501  snopeqop  5515  euotd  5522  poeq2  5600  sotric  5625  sotrieq  5626  freq2  5656  seeq1  5658  seeq2  5659  iss  6054  tz7.7  6411  ordtri1  6418  ordelinel  6486  iotavalOLD  6536  funeq  6587  funssres  6611  f0dom0  6792  tz6.12cOLD  6933  fnbrfvb  6959  ssimaex  6993  fvimacnv  7072  elpreima  7077  feldmfvelcdm  7105  eldmrexrnb  7111  fsn  7154  fnsnb  7185  fmptsng  7187  fmptsnd  7188  fprb  7213  tpres  7220  fconst2g  7222  fconst5  7225  elunirn  7270  f1ocnvfvb  7298  f1prex  7303  foeqcnvco  7319  f1eqcocnv  7320  fliftfun  7331  soisores  7346  isofr  7361  isose  7362  isopo  7365  isoso  7367  f1oiso2  7371  eusvobj2  7422  oprabidw  7461  oprabid  7462  f1opw2  7687  oneqmin  7819  ordsucOLD  7833  ordelsuc  7839  ordsucelsuc  7841  ordunisuc2  7864  limsuc  7869  fndmexb  7928  f1ovv  7980  mptcnfimad  8009  op1steq  8056  opreuopreu  8057  funeldmdif  8071  fvn0elsuppb  8204  extmptsuppeq  8211  rntpos  8262  smoiso2  8407  seqomlem2  8489  oaord  8583  oawordex  8593  oaordex  8594  omord2  8603  om00  8611  oeord  8624  nnaord  8655  nnmord  8668  nnawordex  8673  nnaordex  8674  nnaordex2  8675  eldifsucnn  8700  erexb  8768  swoord1  8775  swoord2  8776  iiner  8827  eceqoveq  8860  mapsnd  8924  ralxpmap  8934  omxpenlem  9111  domtriord  9161  mapxpen  9181  mapunen  9184  ssenen  9189  enfi  9224  nneneq  9243  nndomog  9250  nneneqOLD  9255  nndomogOLD  9260  onomeneq  9262  onomeneqOLD  9263  en1eqsnbi  9307  fodomfib  9366  fodomfibOLD  9368  f1opwfi  9393  fsuppunbi  9426  elfiun  9467  suplub2  9498  ordiso2  9552  ordiso  9553  oieu  9576  brwdom2  9610  brwdom3  9619  cantnflem1  9726  ttrclselem2  9763  cardidm  9996  carddom2  10014  pm54.43  10038  pr2neOLD  10042  acnen  10090  acnen2  10092  alephord  10112  alephinit  10132  dfac5  10166  infdif2  10246  fictb  10281  coflim  10298  fincssdom  10360  fin23lem25  10361  isf32lem9  10398  isf34lem4  10414  fin1a2lem11  10447  axdc3lem2  10488  ficard  10602  fpwwe2lem11  10678  fpwwe2  10680  indpi  10944  nqereq  10972  1idpr  11066  ltapr  11082  leltne  11347  ltlen  11359  ltadd2  11362  addlsub  11676  addid0  11679  ltord1  11786  mul0or  11900  ldiv  12098  ltmul1  12114  mulge0b  12135  lt2msq  12150  nnsub  12307  nn0sub  12573  zrevaddcl  12659  zltp1le  12664  zdiv  12685  nneo  12699  zeo2  12702  zmax  12984  zbtwnre  12985  qrevaddcl  13010  xrlttri  13177  xrleltne  13183  xralrple  13243  xltneg  13255  xleadd1  13293  xlemul1  13328  supxrunb1  13357  supxrunb2  13358  ioo0  13408  iccid  13428  ico0  13429  ioc0  13430  icc0  13431  difreicc  13520  iccsplit  13521  zltaddlt1le  13541  0fz1  13580  uzsplit  13632  fzm1  13643  fzrevral  13648  ssfzo12bi  13796  elfznelfzob  13808  flge  13841  modid2  13934  modmuladd  13950  ssnn0fi  14022  seqf1olem1  14078  hashen  14382  hashdom  14414  hash2exprb  14506  pr2pwpr  14514  hashtpg  14520  hash3tpexb  14529  len0nnbi  14585  ccats1pfxeqbi  14776  reuccatpfxs1  14781  repsdf2  14812  scshwfzeqfzo  14861  relexpindlem  15098  shftlem  15103  shftuz  15104  abslt  15349  absle  15350  rexico  15388  cau3lem  15389  reusq0  15497  rlim2lt  15529  rlim3  15530  o1lo1  15569  rlimdm  15583  climshft  15608  o1dif  15662  isercolllem2  15698  isercoll  15700  zsum  15750  fsum  15752  fsum00  15830  incexclem  15868  zprod  15969  fprod  15973  dvdsval2  16289  moddvds  16297  negdvdsb  16306  dvdsnegb  16307  dvdscmulr  16318  dvdsmulcr  16319  dvdssub2  16334  dvdsaddre2b  16340  fzo0dvdseq  16356  mod2eq1n2dvds  16380  ltoddhalfle  16394  sumodd  16421  bitsf1ocnv  16477  sadcaddlem  16490  bitsuz  16507  dvdsgcdb  16578  gcdzeq  16585  dvdssqlem  16599  lcmeq0  16633  lcmdvdsb  16646  lcmfeq0b  16663  lcmf  16666  lcmfdvdsb  16676  coprmgcdb  16682  cncongr  16702  isprm2lem  16714  dvdsprime  16720  dvdsprm  16736  isprm7  16741  coprm  16744  euclemma  16746  rpexp  16755  prmdvdsncoprmbd  16760  prmdiveq  16819  hashgcdlem  16821  odzdvds  16828  pythagtrip  16867  pc2dvds  16912  pcprmpw2  16915  pcprmpw  16916  vdwapun  17007  ramtcl2  17044  firest  17478  mrieqv2d  17683  isacs2  17697  isssc  17867  setciso  18144  posasymb  18376  pleval2  18394  pltval3  18396  lublecllem  18417  joinle  18443  meetle  18457  latdisd  18554  lubun  18572  clatleglb  18575  letsr  18650  intopsn  18679  gsumval2a  18710  frmdss2  18888  isgrpid2  19006  isgrpinv  19023  f1ghm0to0  19275  symg1bas  19422  oddvdsnn0  19576  oddvds  19579  odeq  19582  odeq1  19592  gexdvds  19616  pgpfi  19637  pgpssslw  19646  fislw  19657  sylow3lem2  19660  lsmelvalm  19683  lsmlub  19696  lsmss1b  19698  lsmss2b  19700  efgs1b  19768  cyggenod  19916  cyggexb  19931  dprdfeq0  20056  ablsimpgfind  20144  ringinvnz1ne0  20313  ringinvnzdiv  20314  unitmulclb  20397  dvreq1  20427  isnzr2  20534  0ringnnzr  20541  0ring01eqbi  20548  rngciso  20654  ringciso  20688  rrgeq0  20716  domneq0  20724  drngmul0orOLD  20777  isabvd  20829  issrngd  20872  lssats2  21015  lspsneq0  21027  lsmelval2  21101  lvecvs0or  21127  lspsneq  21141  lspsneu  21142  lidl1el  21253  lidldvgen  21361  pzriprnglem10  21518  pzriprnglem11  21519  znunit  21599  psgndif  21637  ipeq0  21673  ocvsscon  21710  pjdm2  21748  obselocv  21765  islinds4  21872  psdmul  22187  ply1coe1eq  22319  cply1coe0bi  22321  mat1dimelbas  22492  cramer  22712  toponcomb  22950  tgss3  23008  clsval2  23073  isopn3  23089  elcls3  23106  opncldf1  23107  neiint  23127  neips  23136  opnneissb  23137  opnssneib  23138  opnnei  23143  tpnei  23144  opnneiid  23149  restcld  23195  restopnb  23198  tgcn  23275  tgcnp  23276  subbascn  23277  iscnp4  23286  cnpnei  23287  cncls2  23296  cncls  23297  cnntr  23298  lmss  23321  hausnei2  23376  lpcls  23387  ordtt1  23402  cmpsub  23423  tgcmp  23424  1stcelcls  23484  locfincmp  23549  kgencn2  23580  ptpjpre1  23594  upxp  23646  txcn  23649  txlm  23671  tgqtop  23735  kqfvima  23753  isr0  23760  regr1lem2  23763  hmeoopn  23789  hmeocld  23790  ptuncnv  23830  fbunfip  23892  fgss2  23897  ufilb  23929  ufprim  23932  trufil  23933  cfinufil  23951  ufildr  23954  elfm2  23971  elfm3  23973  rnelfm  23976  fmfnfmlem4  23980  fmco  23984  flimtopon  23993  flimopn  23998  fbflim2  24000  flimrest  24006  flffbas  24018  cnpflf  24024  fclstopon  24035  fclsnei  24042  fclsbas  24044  fclsfnflim  24050  fclscmp  24053  ufilcmp  24055  isfcf  24057  fcfnei  24058  cnpfcf  24064  alexsubb  24069  alexsubALT  24074  cldsubg  24134  tgphaus  24140  tgpt0  24142  tsmsgsum  24162  tsmsres  24167  xbln0  24439  blssexps  24451  blssex  24452  isxms2  24473  prdsbl  24519  neibl  24529  metss  24536  met2ndc  24551  metrest  24552  metcnp3  24568  tngngp3  24692  nmoeq0  24772  xrsxmet  24844  reconn  24863  iccpnfcnv  24988  fgcfil  25318  iscau4  25326  cfilres  25343  iunmbl2  25605  ismbf3d  25702  mbfaddlem  25708  i1faddlem  25741  i1fmullem  25742  ellimc3  25928  dvfsumlem2  26081  tdeglem4  26113  deg1nn0clb  26143  deg1lt0  26144  dvdsq1p  26216  plypf1  26265  0dgrb  26299  plymul0or  26336  taylthlem2  26430  ulmshft  26447  ulmcaulem  26451  ulmcau  26452  cosord  26587  eff1olem  26604  lognegb  26646  eflogeq  26658  logdivlt  26677  efopn  26714  cxpeq0  26734  cxpeq  26814  angpieqvd  26888  dcubic  26903  asinsinb  26954  acoscosb  26955  atantanb  26981  rlimcnp  27022  isppw  27171  isppw2  27172  vmappw  27173  isnsqf  27192  ppieq0  27233  fsumdvdsdiag  27241  dvdsppwf1o  27243  fsumfldivdiag  27247  chpeq0  27266  chteq0  27267  dchrptlem1  27322  lgsdir2lem4  27386  lgsne0  27393  lgsqr  27409  lgsdchrval  27412  gausslemma2dlem1a  27423  lgsquadlem1  27438  m1lgs  27446  2sqreultblem  27506  2sqreunnltblem  27509  nodenselem8  27750  sltlend  27830  oldlim  27939  sltlpss  27959  sleadd1  28036  sltneg  28091  muls0ord  28225  absslt  28287  n0subs  28374  iscgrglt  28536  brbtwn  28928  brcgr  28929  brbtwn2  28934  axcontlem7  28999  uhgr0vb  29103  edglnl  29174  ausgrusgrb  29196  ushgredgedg  29260  ushgredgedgloop  29262  usgr0vb  29268  usgr1v  29287  nbupgr  29375  nbumgrvtx  29377  nbuhgr2vtx1edgb  29383  edgusgrnbfin  29404  nb3grprlem1  29411  uvtxnbvtxm1  29437  cusgrfilem2  29488  uhgr0edg0rgrb  29606  cusgrm1rusgr  29614  spthonepeq  29784  usgr2pth  29796  wlkiswwlks  29905  wlkiswwlkupgr  29907  wlklnwwlkn  29913  wlklnwwlknupgr  29915  wwlksnextbi  29923  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  wwlksnextprop  29941  umgrwwlks2on  29986  elwspths2on  29989  usgr2wspthons3  29993  elwwlks2  29995  elwspths2spth  29996  clwlkclwwlklem3  30029  loopclwwlkn1b  30070  clwwlknon1sn  30128  clwwlknonwwlknonb  30134  umgr3v3e3cycl  30212  eupth2lem3lem4  30259  frgr0v  30290  frgr3vlem2  30302  2clwwlk2clwwlk  30378  wlkl0  30395  grpoinvf  30560  nvmul0or  30678  nvz  30697  diporthcom  30744  ubthlem3  30900  hvmul0or  31053  his6  31127  hial0  31130  hial02  31131  orthcom  31136  normgt0  31155  ocin  31324  occon3  31325  shsel3  31343  shlub  31442  chssoc  31524  h1de2bi  31582  spansncol  31596  elspansn4  31601  spansnss2  31603  sumspansn  31677  lnopcnbd  32064  lnfncnbd  32085  riesz1  32093  elpjrn  32218  cvcon3  32312  dmdmd  32328  dmdbr3  32333  dmdbr4  32334  dmdbr5  32336  mdslmd1i  32357  atcveq0  32376  chcv1  32383  atssma  32406  atcv0eq  32407  atcv1  32408  bian1dOLD  32484  disjeq1f  32592  br8d  32629  fpwrelmap  32750  xaddeq0  32763  eliccelico  32785  elicoelioo  32786  isarchiofld  33326  unitdivcld  33861  xrge0iifcnv  33893  lmxrge0  33912  indf1ofs  34006  eulerpartlemgh  34359  dstfrvunirn  34455  fnrelpredd  35081  loop1cycl  35121  cusgracyclt3v  35140  cvmliftmolem2  35266  cvmlift2lem12  35298  satfvsucsuc  35349  satfdm  35353  fmlasuc  35370  satffunlem1lem2  35387  satffunlem2lem2  35390  mthmb  35565  climuzcnv  35655  br8  35735  br6  35736  br4  35737  funbreq  35750  axextbdist  35781  dfrdg4  35932  cgrcom  35971  cgrcoml  35977  cgrdegen  35985  btwncom  35995  brsegle  36089  brsegle2  36090  colinbtwnle  36099  btwnoutside  36106  broutsideof3  36107  outsidele  36113  lineunray  36128  lineelsb2  36129  elhf2  36156  elicc3  36299  nn0prpwlem  36304  opnbnd  36307  cldbnd  36308  opnregcld  36312  cldregopn  36313  fnessref  36339  refssfne  36340  neibastop2  36343  fnemeet2  36349  fnejoin2  36351  fgmin  36352  ontgval  36413  ordtop  36418  ordcmp  36429  nndivsub  36439  bj-19.21t  36751  bj-19.23t  36752  bj-19.42t  36755  bj-sbft  36757  bj-cbv2hv  36779  bj-equsal1t  36804  bj-19.21t0  36812  bj-ceqsalt0  36866  bj-ceqsalt1  36867  bj-xpnzexb  36943  bj-idreseq  37144  bj-imdiridlem  37167  bj-finsumval0  37267  bj-fvimacnv0  37268  bj-isrvec2  37282  bj-bary1  37294  dfgcd3  37306  isbasisrelowllem1  37337  isbasisrelowllem2  37338  finxpsuclem  37379  wl-lem-exsb  37546  wl-mo3t  37556  wl-ax11-lem1  37565  matunitlindf  37604  poimirlem6  37612  poimirlem7  37613  poimirlem16  37622  poimirlem19  37625  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  cnambfre  37654  itg2addnc  37660  brabg2  37703  istotbnd3  37757  sstotbnd2  37760  sstotbnd  37761  sstotbnd3  37762  ssbnd  37774  ismtybnd  37793  reheibor  37825  grpoeqdivid  37867  grpokerinj  37879  rngosn3  37910  rngoueqz  37926  1idl  38012  0rngo  38013  divrngidl  38014  igenval2  38052  ispridlc  38056  isdmn3  38060  relcnveq3  38302  iss2  38325  elrelscnveq3  38472  funALTVeq  38681  disjeq  38715  prtlem10  38846  prter2  38862  dral1-o  38885  lshpinN  38970  lsatcveq0  39013  lsatcv0eq  39028  lsatcv1  39029  islshpcv  39034  lkr0f  39075  lkrshp4  39089  lshpkrlem1  39091  lshpset2N  39100  lfl1dim  39102  lfl1dim2N  39103  lub0N  39170  glb0N  39174  oplecon3b  39181  cmtcomN  39230  cmtbr3N  39235  cmtbr4N  39236  cvrnbtwn2  39256  cvrnbtwn3  39257  cvrcon3b  39258  cvrnbtwn4  39260  cvrcmp  39264  atcvreq0  39295  atnle  39298  atlatle  39301  cvlexchb1  39311  cvlcvr1  39320  hlrelat2  39385  exatleN  39386  cvrval3  39395  cvrval4N  39396  cvrexch  39402  atcvr0eq  39408  lnnat  39409  atcvrj0  39410  atcvrj2b  39414  atltcvr  39417  atbtwn  39428  ps-1  39459  3at  39472  islln2a  39499  llncmp  39504  islpln2a  39530  lplncmp  39544  islvol2aN  39574  4at  39595  lvolcmp  39599  pmaple  39743  lncmp  39765  paddss  39827  llnexchb2lem  39850  2polcon4bN  39900  ispsubcl2N  39929  lhpat3  40028  lautcvr  40074  ltrnid  40117  trlval2  40145  trlatn0  40154  ltrnideq  40157  trlnidatb  40159  cdlemeg49lebilem  40521  trlord  40551  cdlemg1a  40552  cdlemg1cex  40570  tendoid0  40807  dva1dim  40967  cdlemm10N  41100  diarnN  41111  cdlemn  41194  dihlspsnssN  41314  dihatexv  41320  dochkrshp  41368  dochkrshp4  41371  djhlsmcl  41396  lcfl6  41482  lcfl8  41484  lcfrvalsnN  41523  lcfrlem9  41532  mapdval2N  41612  mapdordlem2  41619  mapd1o  41630  mapd0  41647  mapdheq2biN  41712  nnproddivdvdsd  41981  primrootspoweq0  42087  aks6d1c1p1  42088  aks6d1c5lem1  42117  sticksstones11  42137  sticksstones22  42149  grpods  42175  unitscyglem2  42177  fnsnbt  42249  eqresfnbd  42251  expeq1d  42337  expeqidd  42338  dvdsexpnn  42346  zdivgd  42350  mulgt0b2d  42466  frlmfzowrdb  42490  frlmsnic  42526  evlselvlem  42572  prjspreln0  42595  elrfi  42681  diophrw  42746  eldioph2b  42750  diophin  42759  rexrabdioph  42781  rmxycomplete  42905  coprmdvdsb  42973  jm2.19  42981  jm2.26  42990  jm2.27  42996  limsuc2  43029  dgraa0p  43137  rngunsnply  43157  fiuneneq  43180  unielss  43206  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  44312  dvconstbi  44329  expgrowth  44330  bcc0  44335  axc11next  44401  pm14.24  44427  sbiota1  44429  sbcim2g  44535  sineq0ALT  44934  pwssfi  44984  mapss2  45147  fsneq  45148  fsneqrn  45153  mapssbi  45155  rnmptbd2lem  45192  infnsuprnmpt  45194  rnmptbdlem  45199  xralrple2  45303  infxrunb2  45317  xralrple4  45322  xralrple3  45323  xrralrecnnle  45332  xrralrecnnge  45339  reclt0  45340  supxrunb3  45348  supxrleubrnmpt  45355  xrre4  45360  unb2ltle  45364  rexabslelem  45367  suprleubrnmpt  45371  infxrunb3rnmpt  45377  uzub  45380  supminfrnmpt  45394  iccintsng  45475  sqrlearg  45505  uzinico  45512  preimaiocmnf  45513  limcresiooub  45597  limclr  45610  climeldmeq  45620  limsuppnflem  45665  limsupmnflem  45675  limsupmnfuzlem  45681  limsupre3lem  45687  limsupre3uzlem  45690  liminfreuzlem  45757  dvnmul  45898  dvmptfprodlem  45899  ismbl3  45941  ismbl4  45948  fourierdlem50  46111  fourierdlem89  46150  fourierdlem91  46152  dfsalgen2  46296  sge0repnf  46341  sge0lefi  46353  sge0resplit  46361  sge0fodjrnlem  46371  voliunsge0lem  46427  hspdifhsp  46571  isvonmbl  46593  ovnovollem3  46613  vonvolmbl  46616  pimrecltpos  46663  preimaicomnf  46666  pimrecltneg  46679  issmflem  46682  issmfle  46700  issmfgt  46711  smfaddlem1  46718  issmfge  46725  smfresal  46743  smflimmpt  46765  smfinflem  46772  smflimsuplem7  46781  smflimsupmpt  46784  sigarcol  46819  confun  46888  or2expropbi  46983  fsetsniunop  46998  fcoresf1b  47019  f1cof1b  47026  funfocofob  47027  rexsb  47048  euoreqb  47058  ralbinrald  47071  rlimdmafv  47126  fafv2elrnb  47184  tz6.12c-afv2  47191  dfatbrafv2b  47194  fnbrafv2b  47197  rlimdmafv2  47207  f1oresf1o2  47240  el1fzopredsuc  47274  2ffzoeq  47276  imasetpreimafvbijlemfo  47329  iccpartiun  47358  ichnfb  47389  ich2exprop  47395  sprsymrelfolem2  47417  paireqne  47435  prprelprb  47441  reupr  47446  requad01  47545  requad1  47546  requad2  47547  dfodd6  47561  dfeven4  47562  evensumeven  47631  sbgoldbalt  47705  clnbgrel  47752  dfclnbgr6  47779  dfnbgr6  47780  isubgredg  47789  isuspgrim0  47809  isuspgrim  47812  gricushgr  47823  uhgrimisgrgriclem  47835  clnbgrgrim  47839  grimedg  47840  usgrgrtrirex  47852  uspgrlimlem2  47891  uspgrlim  47894  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  isassintop  48053  uzlidlring  48078  rngcisoALTV  48120  ringcisoALTV  48154  domnmsuppn0  48213  lindslininds  48309  snlindsntor  48316  isldepslvec2  48330  affinecomb1  48551  prelrrx2b  48563  rrx2plord2  48571  eenglngeehlnm  48588  rrx2vlinest  48590  line2xlem  48602  line2x  48603  line2y  48604  itsclc0xyqsolb  48619  itsclquadb  48625  mpbiran3d  48645  opnneieqv  48706  iscnrm3lem2  48730  fullthinc2  48846  thincciso  48848