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  3085  rexbi  3086  ralbida  3246  ceqsalt  3478  rspcebdv  3579  rspceb2dv  3589  ceqex  3615  elabgtOLD  3636  mob2  3683  reu6  3694  sbciegftOLD  3788  sbcg  3823  2reu2  3858  csbiebt  3888  dfss2  3929  ssdifsym  4233  reupick  4288  reupick2  4290  uneqdifeq  4452  prnebg  4816  preqsnd  4819  prel12g  4824  iuneqconst  4963  disjeq2  5073  disjeq1  5076  disjss3  5101  reusv2lem2  5349  reusv2lem3  5350  alxfr  5357  ralxfrd  5358  ralxfrd2  5362  copsexgw  5445  copsexg  5446  snopeqop  5461  euotd  5468  poeq2  5543  sotric  5569  sotrieq  5570  freq2  5599  seeq1  5601  seeq2  5602  iss  5995  tz7.7  6346  ordtri1  6353  ordelinel  6423  iotavalOLD  6473  funeq  6520  funssres  6544  f0dom0  6726  tz6.12cOLD  6867  fnbrfvb  6893  ssimaex  6928  fvimacnv  7007  elpreima  7012  feldmfvelcdm  7040  eldmrexrnb  7046  fsn  7089  fnsnbg  7120  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  fprb  7150  tpres  7157  fconst2g  7159  fconst5  7162  elunirn  7207  f1ocnvfvb  7236  f1prex  7241  foeqcnvco  7257  f1eqcocnv  7258  fliftfun  7269  soisores  7284  isofr  7299  isose  7300  isopo  7303  isoso  7305  f1oiso2  7309  eusvobj2  7361  oprabidw  7400  oprabid  7401  f1opw2  7624  oneqmin  7756  ordsucOLD  7769  ordelsuc  7775  ordsucelsuc  7777  ordunisuc2  7800  limsuc  7805  fndmexb  7862  resf1ext2b  7891  f1ovv  7916  mptcnfimad  7944  op1steq  7991  opreuopreu  7992  funeldmdif  8006  fvn0elsuppb  8137  extmptsuppeq  8144  rntpos  8195  smoiso2  8315  seqomlem2  8396  oaord  8488  oawordex  8498  oaordex  8499  omord2  8508  om00  8516  oeord  8529  nnaord  8560  nnmord  8573  nnawordex  8578  nnaordex  8579  nnaordex2  8580  eldifsucnn  8605  erexb  8673  swoord1  8680  swoord2  8681  ecelqsdmb  8736  iiner  8739  eceqoveq  8772  mapsnd  8836  ralxpmap  8846  omxpenlem  9019  domtriord  9064  mapxpen  9084  mapunen  9087  ssenen  9092  enfi  9128  nneneq  9147  nndomog  9154  onomeneq  9155  en1eqsnbi  9197  fodomfib  9256  fodomfibOLD  9258  f1opwfi  9283  fsuppunbi  9316  elfiun  9357  suplub2  9388  ordiso2  9444  ordiso  9445  oieu  9468  brwdom2  9502  brwdom3  9511  cantnflem1  9618  ttrclselem2  9655  cardidm  9888  carddom2  9906  pm54.43  9930  pr2neOLD  9934  acnen  9982  acnen2  9984  alephord  10004  alephinit  10024  dfac5  10058  infdif2  10138  fictb  10173  coflim  10190  fincssdom  10252  fin23lem25  10253  isf32lem9  10290  isf34lem4  10306  fin1a2lem11  10339  axdc3lem2  10380  ficard  10494  fpwwe2lem11  10570  fpwwe2  10572  indpi  10836  nqereq  10864  1idpr  10958  ltapr  10974  leltne  11239  ltlen  11251  ltadd2  11254  addlsub  11570  addid0  11573  ltord1  11680  mul0or  11794  ldiv  11992  ltmul1  12008  mulge0b  12029  lt2msq  12044  nnsub  12206  nn0sub  12468  zrevaddcl  12554  zltp1le  12559  zdiv  12580  nneo  12594  zeo2  12597  zmax  12880  zbtwnre  12881  qrevaddcl  12906  xrlttri  13075  xrleltne  13081  xralrple  13141  xltneg  13153  xleadd1  13191  xlemul1  13226  supxrunb1  13255  supxrunb2  13256  ioo0  13307  iccid  13327  ico0  13328  ioc0  13329  icc0  13330  difreicc  13421  iccsplit  13422  zltaddlt1le  13442  0fz1  13481  uzsplit  13533  fzm1  13544  fzrevral  13549  ssfzo12bi  13698  elfznelfzob  13710  flge  13743  modid2  13836  modmuladd  13854  ssnn0fi  13926  seqf1olem1  13982  hashen  14288  hashdom  14320  hash2exprb  14412  pr2pwpr  14420  hashtpg  14426  hash3tpexb  14435  len0nnbi  14492  ccats1pfxeqbi  14683  reuccatpfxs1  14688  repsdf2  14719  scshwfzeqfzo  14768  relexpindlem  15005  shftlem  15010  shftuz  15011  abslt  15257  absle  15258  rexico  15296  cau3lem  15297  reusq0  15407  rlim2lt  15439  rlim3  15440  o1lo1  15479  rlimdm  15493  climshft  15518  o1dif  15572  isercolllem2  15608  isercoll  15610  zsum  15660  fsum  15662  fsum00  15740  incexclem  15778  zprod  15879  fprod  15883  dvdsval2  16201  moddvds  16209  negdvdsb  16218  dvdsnegb  16219  dvdscmulr  16230  dvdsmulcr  16231  dvdssub2  16247  dvdsaddre2b  16253  fzo0dvdseq  16269  mod2eq1n2dvds  16293  ltoddhalfle  16307  sumodd  16334  bitsf1ocnv  16390  sadcaddlem  16403  bitsuz  16420  dvdsgcdb  16491  gcdzeq  16498  dvdssqlem  16512  lcmeq0  16546  lcmdvdsb  16559  lcmfeq0b  16576  lcmf  16579  lcmfdvdsb  16589  coprmgcdb  16595  cncongr  16615  isprm2lem  16627  dvdsprime  16633  dvdsprm  16649  isprm7  16654  coprm  16657  euclemma  16659  rpexp  16668  prmdvdsncoprmbd  16673  prmdiveq  16732  hashgcdlem  16734  odzdvds  16742  pythagtrip  16781  pc2dvds  16826  pcprmpw2  16829  pcprmpw  16830  vdwapun  16921  ramtcl2  16958  firest  17371  mrieqv2d  17580  isacs2  17594  isssc  17762  setciso  18033  posasymb  18260  pleval2  18276  pltval3  18278  lublecllem  18299  joinle  18325  meetle  18339  latdisd  18438  lubun  18456  clatleglb  18459  letsr  18534  intopsn  18563  gsumval2a  18594  frmdss2  18772  isgrpid2  18890  isgrpinv  18907  f1ghm0to0  19159  symg1bas  19305  oddvdsnn0  19458  oddvds  19461  odeq  19464  odeq1  19474  gexdvds  19498  pgpfi  19519  pgpssslw  19528  fislw  19539  sylow3lem2  19542  lsmelvalm  19565  lsmlub  19578  lsmss1b  19580  lsmss2b  19582  efgs1b  19650  cyggenod  19798  cyggexb  19813  dprdfeq0  19938  ablsimpgfind  20026  ringinvnz1ne0  20220  ringinvnzdiv  20221  unitmulclb  20301  dvreq1  20331  isnzr2  20438  0ringnnzr  20445  0ring01eqbi  20452  rngciso  20558  ringciso  20592  rrgeq0  20620  domneq0  20628  drngmul0orOLD  20681  isabvd  20732  issrngd  20775  lssats2  20938  lspsneq0  20950  lsmelval2  21024  lvecvs0or  21050  lspsneq  21064  lspsneu  21065  lidl1el  21168  lidldvgen  21276  pzriprnglem10  21432  pzriprnglem11  21433  znunit  21505  psgndif  21544  ipeq0  21580  ocvsscon  21617  pjdm2  21653  obselocv  21670  islinds4  21777  psdmul  22086  ply1coe1eq  22220  cply1coe0bi  22222  mat1dimelbas  22391  cramer  22611  toponcomb  22849  tgss3  22906  clsval2  22970  isopn3  22986  elcls3  23003  opncldf1  23004  neiint  23024  neips  23033  opnneissb  23034  opnssneib  23035  opnnei  23040  tpnei  23041  opnneiid  23046  restcld  23092  restopnb  23095  tgcn  23172  tgcnp  23173  subbascn  23174  iscnp4  23183  cnpnei  23184  cncls2  23193  cncls  23194  cnntr  23195  lmss  23218  hausnei2  23273  lpcls  23284  ordtt1  23299  cmpsub  23320  tgcmp  23321  1stcelcls  23381  locfincmp  23446  kgencn2  23477  ptpjpre1  23491  upxp  23543  txcn  23546  txlm  23568  tgqtop  23632  kqfvima  23650  isr0  23657  regr1lem2  23660  hmeoopn  23686  hmeocld  23687  ptuncnv  23727  fbunfip  23789  fgss2  23794  ufilb  23826  ufprim  23829  trufil  23830  cfinufil  23848  ufildr  23851  elfm2  23868  elfm3  23870  rnelfm  23873  fmfnfmlem4  23877  fmco  23881  flimtopon  23890  flimopn  23895  fbflim2  23897  flimrest  23903  flffbas  23915  cnpflf  23921  fclstopon  23932  fclsnei  23939  fclsbas  23941  fclsfnflim  23947  fclscmp  23950  ufilcmp  23952  isfcf  23954  fcfnei  23955  cnpfcf  23961  alexsubb  23966  alexsubALT  23971  cldsubg  24031  tgphaus  24037  tgpt0  24039  tsmsgsum  24059  tsmsres  24064  xbln0  24335  blssexps  24347  blssex  24348  isxms2  24369  prdsbl  24412  neibl  24422  metss  24429  met2ndc  24444  metrest  24445  metcnp3  24461  tngngp3  24577  nmoeq0  24657  xrsxmet  24731  reconn  24750  iccpnfcnv  24875  fgcfil  25204  iscau4  25212  cfilres  25229  iunmbl2  25491  ismbf3d  25588  mbfaddlem  25594  i1faddlem  25627  i1fmullem  25628  ellimc3  25813  dvfsumlem2  25966  tdeglem4  25998  deg1nn0clb  26028  deg1lt0  26029  dvdsq1p  26101  plypf1  26150  0dgrb  26184  plymul0or  26221  taylthlem2  26315  ulmshft  26332  ulmcaulem  26336  ulmcau  26337  cosord  26473  eff1olem  26490  lognegb  26532  eflogeq  26544  logdivlt  26563  efopn  26600  cxpeq0  26620  cxpeq  26700  angpieqvd  26774  dcubic  26789  asinsinb  26840  acoscosb  26841  atantanb  26867  rlimcnp  26908  isppw  27057  isppw2  27058  vmappw  27059  isnsqf  27078  ppieq0  27119  fsumdvdsdiag  27127  dvdsppwf1o  27129  fsumfldivdiag  27133  chpeq0  27152  chteq0  27153  dchrptlem1  27208  lgsdir2lem4  27272  lgsne0  27279  lgsqr  27295  lgsdchrval  27298  gausslemma2dlem1a  27309  lgsquadlem1  27324  m1lgs  27332  2sqreultblem  27392  2sqreunnltblem  27395  nodenselem8  27636  sltlend  27716  oldlim  27836  sltlpss  27857  sleadd1  27936  sltneg  27991  muls0ord  28128  absslt  28191  onslt  28208  n0subs  28293  n0sltp1le  28295  zs12ge0  28395  iscgrglt  28494  brbtwn  28879  brcgr  28880  brbtwn2  28885  axcontlem7  28950  uhgr0vb  29052  edglnl  29123  ausgrusgrb  29145  ushgredgedg  29209  ushgredgedgloop  29211  usgr0vb  29217  usgr1v  29236  nbupgr  29324  nbumgrvtx  29326  nbuhgr2vtx1edgb  29332  edgusgrnbfin  29353  nb3grprlem1  29360  uvtxnbvtxm1  29386  cusgrfilem2  29437  uhgr0edg0rgrb  29555  cusgrm1rusgr  29563  spthonepeq  29732  usgr2pth  29744  wlkiswwlks  29856  wlkiswwlkupgr  29858  wlklnwwlkn  29864  wlklnwwlknupgr  29866  wwlksnextbi  29874  wwlksnredwwlkn0  29876  wwlksnextwrd  29877  wwlksnextprop  29892  umgrwwlks2on  29937  elwspths2on  29940  usgr2wspthons3  29944  elwwlks2  29946  elwspths2spth  29947  clwlkclwwlklem3  29980  loopclwwlkn1b  30021  clwwlknon1sn  30079  clwwlknonwwlknonb  30085  umgr3v3e3cycl  30163  eupth2lem3lem4  30210  frgr0v  30241  frgr3vlem2  30253  2clwwlk2clwwlk  30329  wlkl0  30346  grpoinvf  30511  nvmul0or  30629  nvz  30648  diporthcom  30695  ubthlem3  30851  hvmul0or  31004  his6  31078  hial0  31081  hial02  31082  orthcom  31087  normgt0  31106  ocin  31275  occon3  31276  shsel3  31294  shlub  31393  chssoc  31475  h1de2bi  31533  spansncol  31547  elspansn4  31552  spansnss2  31554  sumspansn  31628  lnopcnbd  32015  lnfncnbd  32036  riesz1  32044  elpjrn  32169  cvcon3  32263  dmdmd  32279  dmdbr3  32284  dmdbr4  32285  dmdbr5  32287  mdslmd1i  32308  atcveq0  32327  chcv1  32334  atssma  32357  atcv0eq  32358  atcv1  32359  bian1dOLD  32436  disjeq1f  32552  br8d  32588  fpwrelmap  32706  xaddeq0  32726  eliccelico  32750  elicoelioo  32751  indf1ofs  32839  isarchiofld  33168  unitdivcld  33884  xrge0iifcnv  33916  lmxrge0  33935  eulerpartlemgh  34362  dstfrvunirn  34459  fnrelpredd  35072  loop1cycl  35117  cusgracyclt3v  35136  cvmliftmolem2  35262  cvmlift2lem12  35294  satfvsucsuc  35345  satfdm  35349  fmlasuc  35366  satffunlem1lem2  35383  satffunlem2lem2  35386  mthmb  35561  climuzcnv  35651  br8  35736  br6  35737  br4  35738  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  36298  nn0prpwlem  36303  opnbnd  36306  cldbnd  36307  opnregcld  36311  cldregopn  36312  fnessref  36338  refssfne  36339  neibastop2  36342  fnemeet2  36348  fnejoin2  36350  fgmin  36351  ontgval  36412  ordtop  36417  ordcmp  36428  nndivsub  36438  bj-19.21t  36750  bj-19.23t  36751  bj-19.42t  36754  bj-sbft  36756  bj-cbv2hv  36778  bj-equsal1t  36803  bj-19.21t0  36811  bj-ceqsalt0  36865  bj-ceqsalt1  36866  bj-xpnzexb  36942  bj-idreseq  37143  bj-imdiridlem  37166  bj-finsumval0  37266  bj-fvimacnv0  37267  bj-isrvec2  37281  bj-bary1  37293  dfgcd3  37305  isbasisrelowllem1  37336  isbasisrelowllem2  37337  finxpsuclem  37378  wl-lem-exsb  37547  wl-mo3t  37557  wl-ax11-lem1  37566  matunitlindf  37605  poimirlem6  37613  poimirlem7  37614  poimirlem16  37623  poimirlem19  37626  poimirlem22  37629  poimirlem23  37630  poimirlem24  37631  cnambfre  37655  itg2addnc  37661  brabg2  37704  istotbnd3  37758  sstotbnd2  37761  sstotbnd  37762  sstotbnd3  37763  ssbnd  37775  ismtybnd  37794  reheibor  37826  grpoeqdivid  37868  grpokerinj  37880  rngosn3  37911  rngoueqz  37927  1idl  38013  0rngo  38014  divrngidl  38015  igenval2  38053  ispridlc  38057  isdmn3  38061  relcnveq3  38302  iss2  38319  elrelscnveq3  38475  funALTVeq  38685  disjeq  38719  prtlem10  38851  prter2  38867  dral1-o  38890  lshpinN  38975  lsatcveq0  39018  lsatcv0eq  39033  lsatcv1  39034  islshpcv  39039  lkr0f  39080  lkrshp4  39094  lshpkrlem1  39096  lshpset2N  39105  lfl1dim  39107  lfl1dim2N  39108  lub0N  39175  glb0N  39179  oplecon3b  39186  cmtcomN  39235  cmtbr3N  39240  cmtbr4N  39241  cvrnbtwn2  39261  cvrnbtwn3  39262  cvrcon3b  39263  cvrnbtwn4  39265  cvrcmp  39269  atcvreq0  39300  atnle  39303  atlatle  39306  cvlexchb1  39316  cvlcvr1  39325  hlrelat2  39390  exatleN  39391  cvrval3  39400  cvrval4N  39401  cvrexch  39407  atcvr0eq  39413  lnnat  39414  atcvrj0  39415  atcvrj2b  39419  atltcvr  39422  atbtwn  39433  ps-1  39464  3at  39477  islln2a  39504  llncmp  39509  islpln2a  39535  lplncmp  39549  islvol2aN  39579  4at  39600  lvolcmp  39604  pmaple  39748  lncmp  39770  paddss  39832  llnexchb2lem  39855  2polcon4bN  39905  ispsubcl2N  39934  lhpat3  40033  lautcvr  40079  ltrnid  40122  trlval2  40150  trlatn0  40159  ltrnideq  40162  trlnidatb  40164  cdlemeg49lebilem  40526  trlord  40556  cdlemg1a  40557  cdlemg1cex  40575  tendoid0  40812  dva1dim  40972  cdlemm10N  41105  diarnN  41116  cdlemn  41199  dihlspsnssN  41319  dihatexv  41325  dochkrshp  41373  dochkrshp4  41376  djhlsmcl  41401  lcfl6  41487  lcfl8  41489  lcfrvalsnN  41528  lcfrlem9  41537  mapdval2N  41617  mapdordlem2  41624  mapd1o  41635  mapd0  41652  mapdheq2biN  41717  nnproddivdvdsd  41981  primrootspoweq0  42087  aks6d1c1p1  42088  aks6d1c5lem1  42117  sticksstones11  42137  sticksstones22  42149  grpods  42175  unitscyglem2  42177  eqresfnbd  42213  expeq1d  42305  expeqidd  42306  dvdsexpnn  42314  zdivgd  42318  sn-remul0ord  42389  mulgt0b1d  42453  frlmfzowrdb  42485  frlmsnic  42521  evlselvlem  42567  prjspreln0  42590  elrfi  42675  diophrw  42740  eldioph2b  42744  diophin  42753  rexrabdioph  42775  rmxycomplete  42899  coprmdvdsb  42967  jm2.19  42975  jm2.26  42984  jm2.27  42990  limsuc2  43023  dgraa0p  43131  rngunsnply  43151  fiuneneq  43174  unielss  43200  oaabsb  43276  nnoeomeqom  43294  cantnfresb  43306  tfsconcatrn  43324  tfsconcat0b  43328  tfsconcatrev  43330  oadif1lem  43361  oadif1  43362  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  pwelg  43542  nzss  44299  dvconstbi  44316  expgrowth  44317  bcc0  44322  axc11next  44388  pm14.24  44414  sbiota1  44416  sbcim2g  44521  sineq0ALT  44919  mapss2  45192  fsneq  45193  fsneqrn  45198  mapssbi  45200  rnmptbd2lem  45235  infnsuprnmpt  45237  rnmptbdlem  45242  xralrple2  45343  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  47849  dfnbgr6  47850  isubgredg  47859  isuspgrim0  47887  isuspgrim  47889  gricushgr  47910  uhgrimisgrgriclem  47923  clnbgrgrim  47927  grimedg  47928  usgrgrtrirex  47942  uspgrlimlem2  47981  uspgrlim  47984  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  gpgnbgrvtx0  48058  gpgnbgrvtx1  48059  isassintop  48191  uzlidlring  48216  rngcisoALTV  48258  ringcisoALTV  48292  domnmsuppn0  48350  lindslininds  48446  snlindsntor  48453  isldepslvec2  48467  affinecomb1  48684  prelrrx2b  48696  rrx2plord2  48704  eenglngeehlnm  48721  rrx2vlinest  48723  line2xlem  48735  line2x  48736  line2y  48737  itsclc0xyqsolb  48752  itsclquadb  48758  mpbiran3d  48778  opnneieqv  48892  iscnrm3lem2  48916  fullthinc2  49433  thincciso  49435