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  3084  rexbi  3085  ralbida  3240  ceqsalt  3470  rspcebdv  3571  rspceb2dv  3581  ceqex  3607  elabgtOLD  3628  mob2  3675  reu6  3686  sbciegftOLD  3780  sbcg  3815  2reu2  3850  csbiebt  3880  dfss2  3921  ssdifsym  4225  reupick  4280  reupick2  4282  uneqdifeq  4444  prnebg  4807  preqsnd  4810  prel12g  4815  iuneqconst  4953  disjeq2  5063  disjeq1  5066  disjss3  5091  reusv2lem2  5338  reusv2lem3  5339  alxfr  5346  ralxfrd  5347  ralxfrd2  5351  copsexgw  5433  copsexg  5434  snopeqop  5449  euotd  5456  poeq2  5531  sotric  5557  sotrieq  5558  freq2  5587  seeq1  5589  seeq2  5590  iss  5986  tz7.7  6333  ordtri1  6340  ordelinel  6410  funeq  6502  funssres  6526  f0dom0  6708  fnbrfvb  6873  ssimaex  6908  fvimacnv  6987  elpreima  6992  feldmfvelcdm  7020  eldmrexrnb  7026  fsn  7069  fnsnbg  7100  fnsnbOLD  7102  fmptsng  7104  fmptsnd  7105  fprb  7130  tpres  7137  fconst2g  7139  fconst5  7142  elunirn  7187  f1ocnvfvb  7216  f1prex  7221  foeqcnvco  7237  f1eqcocnv  7238  fliftfun  7249  soisores  7264  isofr  7279  isose  7280  isopo  7283  isoso  7285  f1oiso2  7289  eusvobj2  7341  oprabidw  7380  oprabid  7381  f1opw2  7604  oneqmin  7736  ordelsuc  7753  ordsucelsuc  7755  ordunisuc2  7777  limsuc  7782  fndmexb  7839  resf1ext2b  7868  f1ovv  7893  mptcnfimad  7921  op1steq  7968  opreuopreu  7969  funeldmdif  7983  fvn0elsuppb  8114  extmptsuppeq  8121  rntpos  8172  smoiso2  8292  seqomlem2  8373  oaord  8465  oawordex  8475  oaordex  8476  omord2  8485  om00  8493  oeord  8506  nnaord  8537  nnmord  8550  nnawordex  8555  nnaordex  8556  nnaordex2  8557  eldifsucnn  8582  erexb  8650  swoord1  8657  swoord2  8658  ecelqsdmb  8713  iiner  8716  eceqoveq  8749  mapsnd  8813  ralxpmap  8823  omxpenlem  8995  domtriord  9040  mapxpen  9060  mapunen  9063  ssenen  9068  enfi  9101  nneneq  9120  nndomog  9127  onomeneq  9128  en1eqsnbi  9165  fodomfib  9219  fodomfibOLD  9221  f1opwfi  9246  fsuppunbi  9279  elfiun  9320  suplub2  9351  ordiso2  9407  ordiso  9408  oieu  9431  brwdom2  9465  brwdom3  9474  cantnflem1  9585  ttrclselem2  9622  cardidm  9855  carddom2  9873  pm54.43  9897  acnen  9947  acnen2  9949  alephord  9969  alephinit  9989  dfac5  10023  infdif2  10103  fictb  10138  coflim  10155  fincssdom  10217  fin23lem25  10218  isf32lem9  10255  isf34lem4  10271  fin1a2lem11  10304  axdc3lem2  10345  ficard  10459  fpwwe2lem11  10535  fpwwe2  10537  indpi  10801  nqereq  10829  1idpr  10923  ltapr  10939  leltne  11205  ltlen  11217  ltadd2  11220  addlsub  11536  addid0  11539  ltord1  11646  mul0or  11760  ldiv  11958  ltmul1  11974  mulge0b  11995  lt2msq  12010  nnsub  12172  nn0sub  12434  zrevaddcl  12520  zltp1le  12525  zdiv  12546  nneo  12560  zeo2  12563  zmax  12846  zbtwnre  12847  qrevaddcl  12872  xrlttri  13041  xrleltne  13047  xralrple  13107  xltneg  13119  xleadd1  13157  xlemul1  13192  supxrunb1  13221  supxrunb2  13222  ioo0  13273  iccid  13293  ico0  13294  ioc0  13295  icc0  13296  difreicc  13387  iccsplit  13388  zltaddlt1le  13408  0fz1  13447  uzsplit  13499  fzm1  13510  fzrevral  13515  ssfzo12bi  13664  elfznelfzob  13676  flge  13709  modid2  13802  modmuladd  13820  ssnn0fi  13892  seqf1olem1  13948  hashen  14254  hashdom  14286  hash2exprb  14378  pr2pwpr  14386  hashtpg  14392  hash3tpexb  14401  len0nnbi  14458  ccats1pfxeqbi  14648  reuccatpfxs1  14653  repsdf2  14684  scshwfzeqfzo  14733  relexpindlem  14970  shftlem  14975  shftuz  14976  abslt  15222  absle  15223  rexico  15261  cau3lem  15262  reusq0  15372  rlim2lt  15404  rlim3  15405  o1lo1  15444  rlimdm  15458  climshft  15483  o1dif  15537  isercolllem2  15573  isercoll  15575  zsum  15625  fsum  15627  fsum00  15705  incexclem  15743  zprod  15844  fprod  15848  dvdsval2  16166  moddvds  16174  negdvdsb  16183  dvdsnegb  16184  dvdscmulr  16195  dvdsmulcr  16196  dvdssub2  16212  dvdsaddre2b  16218  fzo0dvdseq  16234  mod2eq1n2dvds  16258  ltoddhalfle  16272  sumodd  16299  bitsf1ocnv  16355  sadcaddlem  16368  bitsuz  16385  dvdsgcdb  16456  gcdzeq  16463  dvdssqlem  16477  lcmeq0  16511  lcmdvdsb  16524  lcmfeq0b  16541  lcmf  16544  lcmfdvdsb  16554  coprmgcdb  16560  cncongr  16580  isprm2lem  16592  dvdsprime  16598  dvdsprm  16614  isprm7  16619  coprm  16622  euclemma  16624  rpexp  16633  prmdvdsncoprmbd  16638  prmdiveq  16697  hashgcdlem  16699  odzdvds  16707  pythagtrip  16746  pc2dvds  16791  pcprmpw2  16794  pcprmpw  16795  vdwapun  16886  ramtcl2  16923  firest  17336  mrieqv2d  17545  isacs2  17559  isssc  17727  setciso  17998  posasymb  18225  pleval2  18241  pltval3  18243  lublecllem  18264  joinle  18290  meetle  18304  latdisd  18403  lubun  18421  clatleglb  18424  letsr  18499  intopsn  18528  gsumval2a  18559  frmdss2  18737  isgrpid2  18855  isgrpinv  18872  f1ghm0to0  19124  symg1bas  19270  oddvdsnn0  19423  oddvds  19426  odeq  19429  odeq1  19439  gexdvds  19463  pgpfi  19484  pgpssslw  19493  fislw  19504  sylow3lem2  19507  lsmelvalm  19530  lsmlub  19543  lsmss1b  19545  lsmss2b  19547  efgs1b  19615  cyggenod  19763  cyggexb  19778  dprdfeq0  19903  ablsimpgfind  19991  ringinvnz1ne0  20185  ringinvnzdiv  20186  unitmulclb  20266  dvreq1  20296  isnzr2  20403  0ringnnzr  20410  0ring01eqbi  20417  rngciso  20523  ringciso  20557  rrgeq0  20585  domneq0  20593  drngmul0orOLD  20646  isabvd  20697  issrngd  20740  lssats2  20903  lspsneq0  20915  lsmelval2  20989  lvecvs0or  21015  lspsneq  21029  lspsneu  21030  lidl1el  21133  lidldvgen  21241  pzriprnglem10  21397  pzriprnglem11  21398  znunit  21470  psgndif  21509  ipeq0  21545  ocvsscon  21582  pjdm2  21618  obselocv  21635  islinds4  21742  psdmul  22051  ply1coe1eq  22185  cply1coe0bi  22187  mat1dimelbas  22356  cramer  22576  toponcomb  22814  tgss3  22871  clsval2  22935  isopn3  22951  elcls3  22968  opncldf1  22969  neiint  22989  neips  22998  opnneissb  22999  opnssneib  23000  opnnei  23005  tpnei  23006  opnneiid  23011  restcld  23057  restopnb  23060  tgcn  23137  tgcnp  23138  subbascn  23139  iscnp4  23148  cnpnei  23149  cncls2  23158  cncls  23159  cnntr  23160  lmss  23183  hausnei2  23238  lpcls  23249  ordtt1  23264  cmpsub  23285  tgcmp  23286  1stcelcls  23346  locfincmp  23411  kgencn2  23442  ptpjpre1  23456  upxp  23508  txcn  23511  txlm  23533  tgqtop  23597  kqfvima  23615  isr0  23622  regr1lem2  23625  hmeoopn  23651  hmeocld  23652  ptuncnv  23692  fbunfip  23754  fgss2  23759  ufilb  23791  ufprim  23794  trufil  23795  cfinufil  23813  ufildr  23816  elfm2  23833  elfm3  23835  rnelfm  23838  fmfnfmlem4  23842  fmco  23846  flimtopon  23855  flimopn  23860  fbflim2  23862  flimrest  23868  flffbas  23880  cnpflf  23886  fclstopon  23897  fclsnei  23904  fclsbas  23906  fclsfnflim  23912  fclscmp  23915  ufilcmp  23917  isfcf  23919  fcfnei  23920  cnpfcf  23926  alexsubb  23931  alexsubALT  23936  cldsubg  23996  tgphaus  24002  tgpt0  24004  tsmsgsum  24024  tsmsres  24029  xbln0  24300  blssexps  24312  blssex  24313  isxms2  24334  prdsbl  24377  neibl  24387  metss  24394  met2ndc  24409  metrest  24410  metcnp3  24426  tngngp3  24542  nmoeq0  24622  xrsxmet  24696  reconn  24715  iccpnfcnv  24840  fgcfil  25169  iscau4  25177  cfilres  25194  iunmbl2  25456  ismbf3d  25553  mbfaddlem  25559  i1faddlem  25592  i1fmullem  25593  ellimc3  25778  dvfsumlem2  25931  tdeglem4  25963  deg1nn0clb  25993  deg1lt0  25994  dvdsq1p  26066  plypf1  26115  0dgrb  26149  plymul0or  26186  taylthlem2  26280  ulmshft  26297  ulmcaulem  26301  ulmcau  26302  cosord  26438  eff1olem  26455  lognegb  26497  eflogeq  26509  logdivlt  26528  efopn  26565  cxpeq0  26585  cxpeq  26665  angpieqvd  26739  dcubic  26754  asinsinb  26805  acoscosb  26806  atantanb  26832  rlimcnp  26873  isppw  27022  isppw2  27023  vmappw  27024  isnsqf  27043  ppieq0  27084  fsumdvdsdiag  27092  dvdsppwf1o  27094  fsumfldivdiag  27098  chpeq0  27117  chteq0  27118  dchrptlem1  27173  lgsdir2lem4  27237  lgsne0  27244  lgsqr  27260  lgsdchrval  27263  gausslemma2dlem1a  27274  lgsquadlem1  27289  m1lgs  27297  2sqreultblem  27357  2sqreunnltblem  27360  nodenselem8  27601  sltlend  27681  oldlim  27801  sltlpss  27822  sleadd1  27901  sltneg  27956  muls0ord  28093  absslt  28156  onslt  28173  n0subs  28258  n0sltp1le  28260  zs12ge0  28360  iscgrglt  28459  brbtwn  28844  brcgr  28845  brbtwn2  28850  axcontlem7  28915  uhgr0vb  29017  edglnl  29088  ausgrusgrb  29110  ushgredgedg  29174  ushgredgedgloop  29176  usgr0vb  29182  usgr1v  29201  nbupgr  29289  nbumgrvtx  29291  nbuhgr2vtx1edgb  29297  edgusgrnbfin  29318  nb3grprlem1  29325  uvtxnbvtxm1  29351  cusgrfilem2  29402  uhgr0edg0rgrb  29520  cusgrm1rusgr  29528  spthonepeq  29697  usgr2pth  29709  wlkiswwlks  29821  wlkiswwlkupgr  29823  wlklnwwlkn  29829  wlklnwwlknupgr  29831  wwlksnextbi  29839  wwlksnredwwlkn0  29841  wwlksnextwrd  29842  wwlksnextprop  29857  umgrwwlks2on  29902  elwspths2on  29905  usgr2wspthons3  29909  elwwlks2  29911  elwspths2spth  29912  clwlkclwwlklem3  29945  loopclwwlkn1b  29986  clwwlknon1sn  30044  clwwlknonwwlknonb  30050  umgr3v3e3cycl  30128  eupth2lem3lem4  30175  frgr0v  30206  frgr3vlem2  30218  2clwwlk2clwwlk  30294  wlkl0  30311  grpoinvf  30476  nvmul0or  30594  nvz  30613  diporthcom  30660  ubthlem3  30816  hvmul0or  30969  his6  31043  hial0  31046  hial02  31047  orthcom  31052  normgt0  31071  ocin  31240  occon3  31241  shsel3  31259  shlub  31358  chssoc  31440  h1de2bi  31498  spansncol  31512  elspansn4  31517  spansnss2  31519  sumspansn  31593  lnopcnbd  31980  lnfncnbd  32001  riesz1  32009  elpjrn  32134  cvcon3  32228  dmdmd  32244  dmdbr3  32249  dmdbr4  32250  dmdbr5  32252  mdslmd1i  32273  atcveq0  32292  chcv1  32299  atssma  32322  atcv0eq  32323  atcv1  32324  bian1dOLD  32401  disjeq1f  32517  br8d  32555  fpwrelmap  32677  xaddeq0  32697  eliccelico  32721  elicoelioo  32722  indf1ofs  32810  isarchiofld  33142  unitdivcld  33874  xrge0iifcnv  33906  lmxrge0  33925  eulerpartlemgh  34352  dstfrvunirn  34449  fnrelpredd  35062  fineqvnttrclse  35083  loop1cycl  35120  cusgracyclt3v  35139  cvmliftmolem2  35265  cvmlift2lem12  35297  satfvsucsuc  35348  satfdm  35352  fmlasuc  35369  satffunlem1lem2  35386  satffunlem2lem2  35389  mthmb  35564  climuzcnv  35654  br8  35739  br6  35740  br4  35741  funbreq  35753  axextbdist  35784  dfrdg4  35935  cgrcom  35974  cgrcoml  35980  cgrdegen  35988  btwncom  35998  brsegle  36092  brsegle2  36093  colinbtwnle  36102  btwnoutside  36109  broutsideof3  36110  outsidele  36116  lineunray  36131  lineelsb2  36132  elhf2  36159  elicc3  36301  nn0prpwlem  36306  opnbnd  36309  cldbnd  36310  opnregcld  36314  cldregopn  36315  fnessref  36341  refssfne  36342  neibastop2  36345  fnemeet2  36351  fnejoin2  36353  fgmin  36354  ontgval  36415  ordtop  36420  ordcmp  36431  nndivsub  36441  bj-19.21t  36753  bj-19.23t  36754  bj-19.42t  36757  bj-sbft  36759  bj-cbv2hv  36781  bj-equsal1t  36806  bj-19.21t0  36814  bj-ceqsalt0  36868  bj-ceqsalt1  36869  bj-xpnzexb  36945  bj-idreseq  37146  bj-imdiridlem  37169  bj-finsumval0  37269  bj-fvimacnv0  37270  bj-isrvec2  37284  bj-bary1  37296  dfgcd3  37308  isbasisrelowllem1  37339  isbasisrelowllem2  37340  finxpsuclem  37381  wl-lem-exsb  37550  wl-mo3t  37560  wl-ax11-lem1  37569  matunitlindf  37608  poimirlem6  37616  poimirlem7  37617  poimirlem16  37626  poimirlem19  37629  poimirlem22  37632  poimirlem23  37633  poimirlem24  37634  cnambfre  37658  itg2addnc  37664  brabg2  37707  istotbnd3  37761  sstotbnd2  37764  sstotbnd  37765  sstotbnd3  37766  ssbnd  37778  ismtybnd  37797  reheibor  37829  grpoeqdivid  37871  grpokerinj  37883  rngosn3  37914  rngoueqz  37930  1idl  38016  0rngo  38017  divrngidl  38018  igenval2  38056  ispridlc  38060  isdmn3  38064  relcnveq3  38305  iss2  38322  elrelscnveq3  38478  funALTVeq  38688  disjeq  38722  prtlem10  38854  prter2  38870  dral1-o  38893  lshpinN  38978  lsatcveq0  39021  lsatcv0eq  39036  lsatcv1  39037  islshpcv  39042  lkr0f  39083  lkrshp4  39097  lshpkrlem1  39099  lshpset2N  39108  lfl1dim  39110  lfl1dim2N  39111  lub0N  39178  glb0N  39182  oplecon3b  39189  cmtcomN  39238  cmtbr3N  39243  cmtbr4N  39244  cvrnbtwn2  39264  cvrnbtwn3  39265  cvrcon3b  39266  cvrnbtwn4  39268  cvrcmp  39272  atcvreq0  39303  atnle  39306  atlatle  39309  cvlexchb1  39319  cvlcvr1  39328  hlrelat2  39392  exatleN  39393  cvrval3  39402  cvrval4N  39403  cvrexch  39409  atcvr0eq  39415  lnnat  39416  atcvrj0  39417  atcvrj2b  39421  atltcvr  39424  atbtwn  39435  ps-1  39466  3at  39479  islln2a  39506  llncmp  39511  islpln2a  39537  lplncmp  39551  islvol2aN  39581  4at  39602  lvolcmp  39606  pmaple  39750  lncmp  39772  paddss  39834  llnexchb2lem  39857  2polcon4bN  39907  ispsubcl2N  39936  lhpat3  40035  lautcvr  40081  ltrnid  40124  trlval2  40152  trlatn0  40161  ltrnideq  40164  trlnidatb  40166  cdlemeg49lebilem  40528  trlord  40558  cdlemg1a  40559  cdlemg1cex  40577  tendoid0  40814  dva1dim  40974  cdlemm10N  41107  diarnN  41118  cdlemn  41201  dihlspsnssN  41321  dihatexv  41327  dochkrshp  41375  dochkrshp4  41378  djhlsmcl  41403  lcfl6  41489  lcfl8  41491  lcfrvalsnN  41530  lcfrlem9  41539  mapdval2N  41619  mapdordlem2  41626  mapd1o  41637  mapd0  41654  mapdheq2biN  41719  nnproddivdvdsd  41983  primrootspoweq0  42089  aks6d1c1p1  42090  aks6d1c5lem1  42119  sticksstones11  42139  sticksstones22  42151  grpods  42177  unitscyglem2  42179  eqresfnbd  42215  expeq1d  42307  expeqidd  42308  dvdsexpnn  42316  zdivgd  42320  sn-remul0ord  42391  mulgt0b1d  42455  frlmfzowrdb  42487  frlmsnic  42523  evlselvlem  42569  prjspreln0  42592  elrfi  42677  diophrw  42742  eldioph2b  42746  diophin  42755  rexrabdioph  42777  rmxycomplete  42900  coprmdvdsb  42968  jm2.19  42976  jm2.26  42985  jm2.27  42991  limsuc2  43024  dgraa0p  43132  rngunsnply  43152  fiuneneq  43175  unielss  43201  oaabsb  43277  nnoeomeqom  43295  cantnfresb  43307  tfsconcatrn  43325  tfsconcat0b  43329  tfsconcatrev  43331  oadif1lem  43362  oadif1  43363  fzunt  43438  fzuntd  43439  fzunt1d  43440  fzuntgd  43441  pwelg  43543  nzss  44300  dvconstbi  44317  expgrowth  44318  bcc0  44323  axc11next  44389  pm14.24  44415  sbiota1  44417  sbcim2g  44522  sineq0ALT  44920  mapss2  45193  fsneq  45194  fsneqrn  45199  mapssbi  45201  rnmptbd2lem  45236  infnsuprnmpt  45238  rnmptbdlem  45243  xralrple2  45344  infxrunb2  45357  xralrple4  45362  xralrple3  45363  xrralrecnnle  45372  xrralrecnnge  45379  reclt0  45380  supxrunb3  45388  supxrleubrnmpt  45395  xrre4  45400  unb2ltle  45404  rexabslelem  45407  suprleubrnmpt  45411  infxrunb3rnmpt  45417  uzub  45420  supminfrnmpt  45434  iccintsng  45514  sqrlearg  45544  uzinico  45550  preimaiocmnf  45551  limcresiooub  45633  limclr  45646  climeldmeq  45656  limsuppnflem  45701  limsupmnflem  45711  limsupmnfuzlem  45717  limsupre3lem  45723  limsupre3uzlem  45726  liminfreuzlem  45793  dvnmul  45934  dvmptfprodlem  45935  ismbl3  45977  ismbl4  45984  fourierdlem50  46147  fourierdlem89  46186  fourierdlem91  46188  dfsalgen2  46332  sge0repnf  46377  sge0lefi  46389  sge0resplit  46397  sge0fodjrnlem  46407  voliunsge0lem  46463  hspdifhsp  46607  isvonmbl  46629  ovnovollem3  46649  vonvolmbl  46652  pimrecltpos  46699  preimaicomnf  46702  pimrecltneg  46715  issmflem  46718  issmfle  46736  issmfgt  46747  smfaddlem1  46754  issmfge  46761  smfresal  46779  smflimmpt  46801  smfinflem  46808  smflimsuplem7  46817  smflimsupmpt  46820  sigarcol  46855  confun  46933  or2expropbi  47028  fsetsniunop  47043  fcoresf1b  47064  f1cof1b  47071  funfocofob  47072  rexsb  47093  euoreqb  47103  ralbinrald  47116  rlimdmafv  47171  fafv2elrnb  47229  tz6.12c-afv2  47236  dfatbrafv2b  47239  fnbrafv2b  47242  rlimdmafv2  47252  f1oresf1o2  47285  el1fzopredsuc  47319  2ffzoeq  47321  modlt0b  47357  imasetpreimafvbijlemfo  47399  iccpartiun  47428  ichnfb  47459  ich2exprop  47465  sprsymrelfolem2  47487  paireqne  47505  prprelprb  47511  reupr  47516  requad01  47615  requad1  47616  requad2  47617  dfodd6  47631  dfeven4  47632  evensumeven  47701  sbgoldbalt  47775  clnbgrel  47822  dfclnbgr6  47850  dfnbgr6  47851  isubgredg  47860  isuspgrim0  47888  isuspgrim  47890  gricushgr  47911  uhgrimisgrgriclem  47924  clnbgrgrim  47928  grimedg  47929  usgrgrtrirex  47944  uspgrlimlem2  47983  uspgrlim  47986  gpgedgiov  48059  gpgedg2ov  48060  gpgedg2iv  48061  gpgnbgrvtx0  48068  gpgnbgrvtx1  48069  isassintop  48204  uzlidlring  48229  rngcisoALTV  48271  ringcisoALTV  48305  domnmsuppn0  48363  lindslininds  48459  snlindsntor  48466  isldepslvec2  48480  affinecomb1  48697  prelrrx2b  48709  rrx2plord2  48717  eenglngeehlnm  48734  rrx2vlinest  48736  line2xlem  48748  line2x  48749  line2y  48750  itsclc0xyqsolb  48765  itsclquadb  48771  mpbiran3d  48791  opnneieqv  48905  iscnrm3lem2  48929  fullthinc2  49446  thincciso  49448