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  1819  alexbii  1834  equequ1  2026  equequ2  2027  spsbbi  2076  elequ1  2118  elequ2  2126  sbequ12  2254  sbft  2272  cbv2w  2337  exsb  2359  dral1v  2369  cbv2  2403  cbv2h  2406  ax12b  2424  dral1  2439  dral1ALT  2440  eupickb  2630  eupickbi  2631  2eu2  2648  ralbi  3087  rexbi  3088  ralbida  3243  ceqsalt  3470  rspcebdv  3566  rspceb2dv  3576  ceqex  3602  elabgtOLD  3623  mob2  3669  reu6  3680  sbciegftOLD  3774  sbcg  3809  2reu2  3844  csbiebt  3874  dfss2  3915  ssdifsym  4221  reupick  4276  reupick2  4278  uneqdifeq  4440  prnebg  4805  preqsnd  4808  prel12g  4813  iuneqconst  4951  disjeq2  5060  disjeq1  5063  disjss3  5088  reusv2lem2  5335  reusv2lem3  5336  alxfr  5343  ralxfrd  5344  ralxfrd2  5348  copsexgw  5428  copsexg  5429  snopeqop  5444  euotd  5451  poeq2  5526  sotric  5552  sotrieq  5553  freq2  5582  seeq1  5584  seeq2  5585  iss  5983  tz7.7  6332  ordtri1  6339  ordelinel  6409  funeq  6501  funssres  6525  f0dom0  6707  fnbrfvb  6872  ssimaex  6907  fvimacnv  6986  elpreima  6991  feldmfvelcdm  7019  eldmrexrnb  7025  fsn  7068  fnsnbg  7098  fnsnbOLD  7100  fmptsng  7102  fmptsnd  7103  fprb  7128  tpres  7135  fconst2g  7137  fconst5  7140  elunirn  7185  f1ocnvfvb  7213  f1prex  7218  foeqcnvco  7234  f1eqcocnv  7235  fliftfun  7246  soisores  7261  isofr  7276  isose  7277  isopo  7280  isoso  7282  f1oiso2  7286  eusvobj2  7338  oprabidw  7377  oprabid  7378  f1opw2  7601  oneqmin  7733  ordelsuc  7750  ordsucelsuc  7752  ordunisuc2  7774  limsuc  7779  fndmexb  7836  resf1ext2b  7865  f1ovv  7890  mptcnfimad  7918  op1steq  7965  opreuopreu  7966  funeldmdif  7980  fvn0elsuppb  8111  extmptsuppeq  8118  rntpos  8169  smoiso2  8289  seqomlem2  8370  oaord  8462  oawordex  8472  oaordex  8473  omord2  8482  om00  8490  oeord  8503  nnaord  8534  nnmord  8547  nnawordex  8552  nnaordex  8553  nnaordex2  8554  eldifsucnn  8579  erexb  8647  swoord1  8654  swoord2  8655  ecelqsdmb  8710  iiner  8713  eceqoveq  8746  mapsnd  8810  ralxpmap  8820  omxpenlem  8991  domtriord  9036  mapxpen  9056  mapunen  9059  ssenen  9064  enfi  9096  nneneq  9115  nndomog  9122  onomeneq  9123  en1eqsnbi  9160  fodomfib  9213  fodomfibOLD  9215  f1opwfi  9240  fsuppunbi  9273  elfiun  9314  suplub2  9345  ordiso2  9401  ordiso  9402  oieu  9425  brwdom2  9459  brwdom3  9468  cantnflem1  9579  ttrclselem2  9616  cardidm  9852  carddom2  9870  pm54.43  9894  acnen  9944  acnen2  9946  alephord  9966  alephinit  9986  dfac5  10020  infdif2  10100  fictb  10135  coflim  10152  fincssdom  10214  fin23lem25  10215  isf32lem9  10252  isf34lem4  10268  fin1a2lem11  10301  axdc3lem2  10342  ficard  10456  fpwwe2lem11  10532  fpwwe2  10534  indpi  10798  nqereq  10826  1idpr  10920  ltapr  10936  leltne  11202  ltlen  11214  ltadd2  11217  addlsub  11533  addid0  11536  ltord1  11643  mul0or  11757  ldiv  11955  ltmul1  11971  mulge0b  11992  lt2msq  12007  nnsub  12169  nn0sub  12431  zrevaddcl  12517  zltp1le  12522  zdiv  12543  nneo  12557  zeo2  12560  zmax  12843  zbtwnre  12844  qrevaddcl  12869  xrlttri  13038  xrleltne  13044  xralrple  13104  xltneg  13116  xleadd1  13154  xlemul1  13189  supxrunb1  13218  supxrunb2  13219  ioo0  13270  iccid  13290  ico0  13291  ioc0  13292  icc0  13293  difreicc  13384  iccsplit  13385  zltaddlt1le  13405  0fz1  13444  uzsplit  13496  fzm1  13507  fzrevral  13512  ssfzo12bi  13661  elfznelfzob  13674  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  14649  reuccatpfxs1  14654  repsdf2  14685  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  18562  gsumval2a  18593  frmdss2  18771  isgrpid2  18889  isgrpinv  18906  f1ghm0to0  19157  symg1bas  19303  oddvdsnn0  19456  oddvds  19459  odeq  19462  odeq1  19472  gexdvds  19496  pgpfi  19517  pgpssslw  19526  fislw  19537  sylow3lem2  19540  lsmelvalm  19563  lsmlub  19576  lsmss1b  19578  lsmss2b  19580  efgs1b  19648  cyggenod  19796  cyggexb  19811  dprdfeq0  19936  ablsimpgfind  20024  ringinvnz1ne0  20218  ringinvnzdiv  20219  unitmulclb  20299  dvreq1  20329  isnzr2  20433  0ringnnzr  20440  0ring01eqbi  20447  rngciso  20553  ringciso  20587  rrgeq0  20615  domneq0  20623  drngmul0orOLD  20676  isabvd  20727  issrngd  20770  lssats2  20933  lspsneq0  20945  lsmelval2  21019  lvecvs0or  21045  lspsneq  21059  lspsneu  21060  lidl1el  21163  lidldvgen  21271  pzriprnglem10  21427  pzriprnglem11  21428  znunit  21500  psgndif  21539  ipeq0  21575  ocvsscon  21612  pjdm2  21648  obselocv  21665  islinds4  21772  psdmul  22081  ply1coe1eq  22215  cply1coe0bi  22217  mat1dimelbas  22386  cramer  22606  toponcomb  22844  tgss3  22901  clsval2  22965  isopn3  22981  elcls3  22998  opncldf1  22999  neiint  23019  neips  23028  opnneissb  23029  opnssneib  23030  opnnei  23035  tpnei  23036  opnneiid  23041  restcld  23087  restopnb  23090  tgcn  23167  tgcnp  23168  subbascn  23169  iscnp4  23178  cnpnei  23179  cncls2  23188  cncls  23189  cnntr  23190  lmss  23213  hausnei2  23268  lpcls  23279  ordtt1  23294  cmpsub  23315  tgcmp  23316  1stcelcls  23376  locfincmp  23441  kgencn2  23472  ptpjpre1  23486  upxp  23538  txcn  23541  txlm  23563  tgqtop  23627  kqfvima  23645  isr0  23652  regr1lem2  23655  hmeoopn  23681  hmeocld  23682  ptuncnv  23722  fbunfip  23784  fgss2  23789  ufilb  23821  ufprim  23824  trufil  23825  cfinufil  23843  ufildr  23846  elfm2  23863  elfm3  23865  rnelfm  23868  fmfnfmlem4  23872  fmco  23876  flimtopon  23885  flimopn  23890  fbflim2  23892  flimrest  23898  flffbas  23910  cnpflf  23916  fclstopon  23927  fclsnei  23934  fclsbas  23936  fclsfnflim  23942  fclscmp  23945  ufilcmp  23947  isfcf  23949  fcfnei  23950  cnpfcf  23956  alexsubb  23961  alexsubALT  23966  cldsubg  24026  tgphaus  24032  tgpt0  24034  tsmsgsum  24054  tsmsres  24059  xbln0  24329  blssexps  24341  blssex  24342  isxms2  24363  prdsbl  24406  neibl  24416  metss  24423  met2ndc  24438  metrest  24439  metcnp3  24455  tngngp3  24571  nmoeq0  24651  xrsxmet  24725  reconn  24744  iccpnfcnv  24869  fgcfil  25198  iscau4  25206  cfilres  25223  iunmbl2  25485  ismbf3d  25582  mbfaddlem  25588  i1faddlem  25621  i1fmullem  25622  ellimc3  25807  dvfsumlem2  25960  tdeglem4  25992  deg1nn0clb  26022  deg1lt0  26023  dvdsq1p  26095  plypf1  26144  0dgrb  26178  plymul0or  26215  taylthlem2  26309  ulmshft  26326  ulmcaulem  26330  ulmcau  26331  cosord  26467  eff1olem  26484  lognegb  26526  eflogeq  26538  logdivlt  26557  efopn  26594  cxpeq0  26614  cxpeq  26694  angpieqvd  26768  dcubic  26783  asinsinb  26834  acoscosb  26835  atantanb  26861  rlimcnp  26902  isppw  27051  isppw2  27052  vmappw  27053  isnsqf  27072  ppieq0  27113  fsumdvdsdiag  27121  dvdsppwf1o  27123  fsumfldivdiag  27127  chpeq0  27146  chteq0  27147  dchrptlem1  27202  lgsdir2lem4  27266  lgsne0  27273  lgsqr  27289  lgsdchrval  27292  gausslemma2dlem1a  27303  lgsquadlem1  27318  m1lgs  27326  2sqreultblem  27386  2sqreunnltblem  27389  nodenselem8  27630  sltlend  27710  oldlim  27832  sltlpss  27853  sleadd1  27932  sltneg  27987  muls0ord  28124  absslt  28187  onslt  28204  n0subs  28289  n0sltp1le  28291  zs12ge0  28393  iscgrglt  28492  brbtwn  28877  brcgr  28878  brbtwn2  28883  axcontlem7  28948  uhgr0vb  29050  edglnl  29121  ausgrusgrb  29143  ushgredgedg  29207  ushgredgedgloop  29209  usgr0vb  29215  usgr1v  29234  nbupgr  29322  nbumgrvtx  29324  nbuhgr2vtx1edgb  29330  edgusgrnbfin  29351  nb3grprlem1  29358  uvtxnbvtxm1  29384  cusgrfilem2  29435  uhgr0edg0rgrb  29553  cusgrm1rusgr  29561  spthonepeq  29730  usgr2pth  29742  wlkiswwlks  29854  wlkiswwlkupgr  29856  wlklnwwlkn  29862  wlklnwwlknupgr  29864  wwlksnextbi  29872  wwlksnredwwlkn0  29874  wwlksnextwrd  29875  wwlksnextprop  29890  usgrwwlks2on  29936  umgrwwlks2on  29937  elwspths2on  29940  elwspths2onw  29941  usgr2wspthons3  29945  elwwlks2  29947  elwspths2spth  29948  clwlkclwwlklem3  29981  loopclwwlkn1b  30022  clwwlknon1sn  30080  clwwlknonwwlknonb  30086  umgr3v3e3cycl  30164  eupth2lem3lem4  30211  frgr0v  30242  frgr3vlem2  30254  2clwwlk2clwwlk  30330  wlkl0  30347  grpoinvf  30512  nvmul0or  30630  nvz  30649  diporthcom  30696  ubthlem3  30852  hvmul0or  31005  his6  31079  hial0  31082  hial02  31083  orthcom  31088  normgt0  31107  ocin  31276  occon3  31277  shsel3  31295  shlub  31394  chssoc  31476  h1de2bi  31534  spansncol  31548  elspansn4  31553  spansnss2  31555  sumspansn  31629  lnopcnbd  32016  lnfncnbd  32037  riesz1  32045  elpjrn  32170  cvcon3  32264  dmdmd  32280  dmdbr3  32285  dmdbr4  32286  dmdbr5  32288  mdslmd1i  32309  atcveq0  32328  chcv1  32335  atssma  32358  atcv0eq  32359  atcv1  32360  bian1dOLD  32436  disjeq1f  32553  br8d  32591  fpwrelmap  32716  xaddeq0  32736  eliccelico  32760  elicoelioo  32761  indf1ofs  32847  isarchiofld  33168  unitdivcld  33914  xrge0iifcnv  33946  lmxrge0  33965  eulerpartlemgh  34391  dstfrvunirn  34488  fnrelpredd  35102  rankfilimb  35113  fineqvnttrclse  35144  loop1cycl  35181  cusgracyclt3v  35200  cvmliftmolem2  35326  cvmlift2lem12  35358  satfvsucsuc  35409  satfdm  35413  fmlasuc  35430  satffunlem1lem2  35447  satffunlem2lem2  35450  mthmb  35625  climuzcnv  35715  br8  35800  br6  35801  br4  35802  funbreq  35814  axextbdist  35842  dfrdg4  35995  cgrcom  36034  cgrcoml  36040  cgrdegen  36048  btwncom  36058  brsegle  36152  brsegle2  36153  colinbtwnle  36162  btwnoutside  36169  broutsideof3  36170  outsidele  36176  lineunray  36191  lineelsb2  36192  elhf2  36219  elicc3  36361  nn0prpwlem  36366  opnbnd  36369  cldbnd  36370  opnregcld  36374  cldregopn  36375  fnessref  36401  refssfne  36402  neibastop2  36405  fnemeet2  36411  fnejoin2  36413  fgmin  36414  ontgval  36475  ordtop  36480  ordcmp  36491  nndivsub  36501  bj-19.21t  36813  bj-19.23t  36814  bj-19.42t  36817  bj-sbft  36819  bj-cbv2hv  36841  bj-equsal1t  36866  bj-19.21t0  36874  bj-ceqsalt0  36928  bj-ceqsalt1  36929  bj-xpnzexb  37005  bj-idreseq  37206  bj-imdiridlem  37229  bj-finsumval0  37329  bj-fvimacnv0  37330  bj-isrvec2  37344  bj-bary1  37356  dfgcd3  37368  isbasisrelowllem1  37399  isbasisrelowllem2  37400  finxpsuclem  37441  wl-lem-exsb  37610  wl-mo3t  37620  matunitlindf  37657  poimirlem6  37665  poimirlem7  37666  poimirlem16  37675  poimirlem19  37678  poimirlem22  37681  poimirlem23  37682  poimirlem24  37683  cnambfre  37707  itg2addnc  37713  brabg2  37756  istotbnd3  37810  sstotbnd2  37813  sstotbnd  37814  sstotbnd3  37815  ssbnd  37827  ismtybnd  37846  reheibor  37878  grpoeqdivid  37920  grpokerinj  37932  rngosn3  37963  rngoueqz  37979  1idl  38065  0rngo  38066  divrngidl  38067  igenval2  38105  ispridlc  38109  isdmn3  38113  relcnveq3  38358  iss2  38375  elrelscnveq3  38638  funALTVeq  38797  disjeq  38831  prtlem10  38963  prter2  38979  dral1-o  39002  lshpinN  39087  lsatcveq0  39130  lsatcv0eq  39145  lsatcv1  39146  islshpcv  39151  lkr0f  39192  lkrshp4  39206  lshpkrlem1  39208  lshpset2N  39217  lfl1dim  39219  lfl1dim2N  39220  lub0N  39287  glb0N  39291  oplecon3b  39298  cmtcomN  39347  cmtbr3N  39352  cmtbr4N  39353  cvrnbtwn2  39373  cvrnbtwn3  39374  cvrcon3b  39375  cvrnbtwn4  39377  cvrcmp  39381  atcvreq0  39412  atnle  39415  atlatle  39418  cvlexchb1  39428  cvlcvr1  39437  hlrelat2  39501  exatleN  39502  cvrval3  39511  cvrval4N  39512  cvrexch  39518  atcvr0eq  39524  lnnat  39525  atcvrj0  39526  atcvrj2b  39530  atltcvr  39533  atbtwn  39544  ps-1  39575  3at  39588  islln2a  39615  llncmp  39620  islpln2a  39646  lplncmp  39660  islvol2aN  39690  4at  39711  lvolcmp  39715  pmaple  39859  lncmp  39881  paddss  39943  llnexchb2lem  39966  2polcon4bN  40016  ispsubcl2N  40045  lhpat3  40144  lautcvr  40190  ltrnid  40233  trlval2  40261  trlatn0  40270  ltrnideq  40273  trlnidatb  40275  cdlemeg49lebilem  40637  trlord  40667  cdlemg1a  40668  cdlemg1cex  40686  tendoid0  40923  dva1dim  41083  cdlemm10N  41216  diarnN  41227  cdlemn  41310  dihlspsnssN  41430  dihatexv  41436  dochkrshp  41484  dochkrshp4  41487  djhlsmcl  41512  lcfl6  41598  lcfl8  41600  lcfrvalsnN  41639  lcfrlem9  41648  mapdval2N  41728  mapdordlem2  41735  mapd1o  41746  mapd0  41763  mapdheq2biN  41828  nnproddivdvdsd  42092  primrootspoweq0  42198  aks6d1c1p1  42199  aks6d1c5lem1  42228  sticksstones11  42248  sticksstones22  42260  grpods  42286  unitscyglem2  42288  eqresfnbd  42324  expeq1d  42416  expeqidd  42417  dvdsexpnn  42425  zdivgd  42429  sn-remul0ord  42500  mulgt0b1d  42564  frlmfzowrdb  42596  frlmsnic  42632  evlselvlem  42678  prjspreln0  42701  elrfi  42786  diophrw  42851  eldioph2b  42855  diophin  42864  rexrabdioph  42886  rmxycomplete  43009  coprmdvdsb  43077  jm2.19  43085  jm2.26  43094  jm2.27  43100  limsuc2  43133  dgraa0p  43241  rngunsnply  43261  fiuneneq  43284  unielss  43310  oaabsb  43386  nnoeomeqom  43404  cantnfresb  43416  tfsconcatrn  43434  tfsconcat0b  43438  tfsconcatrev  43440  oadif1lem  43471  oadif1  43472  fzunt  43547  fzuntd  43548  fzunt1d  43549  fzuntgd  43550  pwelg  43652  nzss  44409  dvconstbi  44426  expgrowth  44427  bcc0  44432  axc11next  44498  pm14.24  44524  sbiota1  44526  sbcim2g  44630  sineq0ALT  45028  mapss2  45301  fsneq  45302  fsneqrn  45307  mapssbi  45309  rnmptbd2lem  45344  infnsuprnmpt  45346  rnmptbdlem  45351  xralrple2  45452  infxrunb2  45465  xralrple4  45470  xralrple3  45471  xrralrecnnle  45480  xrralrecnnge  45487  reclt0  45488  supxrunb3  45496  supxrleubrnmpt  45503  xrre4  45508  unb2ltle  45512  rexabslelem  45515  suprleubrnmpt  45519  infxrunb3rnmpt  45525  uzub  45528  supminfrnmpt  45542  iccintsng  45622  sqrlearg  45652  uzinico  45658  preimaiocmnf  45659  limcresiooub  45739  limclr  45752  climeldmeq  45762  limsuppnflem  45807  limsupmnflem  45817  limsupmnfuzlem  45823  limsupre3lem  45829  limsupre3uzlem  45832  liminfreuzlem  45899  dvnmul  46040  dvmptfprodlem  46041  ismbl3  46083  ismbl4  46090  fourierdlem50  46253  fourierdlem89  46292  fourierdlem91  46294  dfsalgen2  46438  sge0repnf  46483  sge0lefi  46495  sge0resplit  46503  sge0fodjrnlem  46513  voliunsge0lem  46569  hspdifhsp  46713  isvonmbl  46735  ovnovollem3  46755  vonvolmbl  46758  pimrecltpos  46805  preimaicomnf  46808  pimrecltneg  46821  issmflem  46824  issmfle  46842  issmfgt  46853  smfaddlem1  46860  issmfge  46867  smfresal  46885  smflimmpt  46907  smfinflem  46914  smflimsuplem7  46923  smflimsupmpt  46926  sigarcol  46961  confun  47038  or2expropbi  47133  fsetsniunop  47148  fcoresf1b  47169  f1cof1b  47176  funfocofob  47177  rexsb  47198  euoreqb  47208  ralbinrald  47221  rlimdmafv  47276  fafv2elrnb  47334  tz6.12c-afv2  47341  dfatbrafv2b  47344  fnbrafv2b  47347  rlimdmafv2  47357  f1oresf1o2  47390  el1fzopredsuc  47424  2ffzoeq  47426  modlt0b  47462  imasetpreimafvbijlemfo  47504  iccpartiun  47533  ichnfb  47564  ich2exprop  47570  sprsymrelfolem2  47592  paireqne  47610  prprelprb  47616  reupr  47621  requad01  47720  requad1  47721  requad2  47722  dfodd6  47736  dfeven4  47737  evensumeven  47806  sbgoldbalt  47880  clnbgrel  47927  dfclnbgr6  47955  dfnbgr6  47956  isubgredg  47965  isuspgrim0  47993  isuspgrim  47995  gricushgr  48016  uhgrimisgrgriclem  48029  clnbgrgrim  48033  grimedg  48034  usgrgrtrirex  48049  uspgrlimlem2  48088  uspgrlim  48091  gpgedgiov  48164  gpgedg2ov  48165  gpgedg2iv  48166  gpgnbgrvtx0  48173  gpgnbgrvtx1  48174  isassintop  48309  uzlidlring  48334  rngcisoALTV  48376  ringcisoALTV  48410  domnmsuppn0  48468  lindslininds  48564  snlindsntor  48571  isldepslvec2  48585  affinecomb1  48802  prelrrx2b  48814  rrx2plord2  48822  eenglngeehlnm  48839  rrx2vlinest  48841  line2xlem  48853  line2x  48854  line2y  48855  itsclc0xyqsolb  48870  itsclquadb  48876  mpbiran3d  48896  opnneieqv  49010  iscnrm3lem2  49034  fullthinc2  49551  thincciso  49553