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  2358  dral1v  2368  cbv2  2402  cbv2h  2405  ax12b  2423  dral1  2438  dral1ALT  2439  eupickb  2629  eupickbi  2630  2eu2  2647  ralbi  3086  rexbi  3087  ralbida  3249  ceqsalt  3484  rspcebdv  3585  rspceb2dv  3595  ceqex  3621  elabgtOLD  3642  mob2  3689  reu6  3700  sbciegftOLD  3794  sbcg  3829  2reu2  3864  csbiebt  3894  dfss2  3935  ssdifsym  4240  reupick  4295  reupick2  4297  uneqdifeq  4459  prnebg  4823  preqsnd  4826  prel12g  4831  iuneqconst  4970  disjeq2  5081  disjeq1  5084  disjss3  5109  reusv2lem2  5357  reusv2lem3  5358  alxfr  5365  ralxfrd  5366  ralxfrd2  5370  copsexgw  5453  copsexg  5454  snopeqop  5469  euotd  5476  poeq2  5553  sotric  5579  sotrieq  5580  freq2  5609  seeq1  5611  seeq2  5612  iss  6009  tz7.7  6361  ordtri1  6368  ordelinel  6438  iotavalOLD  6488  funeq  6539  funssres  6563  f0dom0  6747  tz6.12cOLD  6888  fnbrfvb  6914  ssimaex  6949  fvimacnv  7028  elpreima  7033  feldmfvelcdm  7061  eldmrexrnb  7067  fsn  7110  fnsnbg  7141  fnsnbOLD  7143  fmptsng  7145  fmptsnd  7146  fprb  7171  tpres  7178  fconst2g  7180  fconst5  7183  elunirn  7228  f1ocnvfvb  7257  f1prex  7262  foeqcnvco  7278  f1eqcocnv  7279  fliftfun  7290  soisores  7305  isofr  7320  isose  7321  isopo  7324  isoso  7326  f1oiso2  7330  eusvobj2  7382  oprabidw  7421  oprabid  7422  f1opw2  7647  oneqmin  7779  ordsucOLD  7792  ordelsuc  7798  ordsucelsuc  7800  ordunisuc2  7823  limsuc  7828  fndmexb  7885  resf1ext2b  7914  f1ovv  7939  mptcnfimad  7968  op1steq  8015  opreuopreu  8016  funeldmdif  8030  fvn0elsuppb  8163  extmptsuppeq  8170  rntpos  8221  smoiso2  8341  seqomlem2  8422  oaord  8514  oawordex  8524  oaordex  8525  omord2  8534  om00  8542  oeord  8555  nnaord  8586  nnmord  8599  nnawordex  8604  nnaordex  8605  nnaordex2  8606  eldifsucnn  8631  erexb  8699  swoord1  8706  swoord2  8707  ecelqsdmb  8762  iiner  8765  eceqoveq  8798  mapsnd  8862  ralxpmap  8872  omxpenlem  9047  domtriord  9093  mapxpen  9113  mapunen  9116  ssenen  9121  enfi  9157  nneneq  9176  nndomog  9183  onomeneq  9184  en1eqsnbi  9228  fodomfib  9287  fodomfibOLD  9289  f1opwfi  9314  fsuppunbi  9347  elfiun  9388  suplub2  9419  ordiso2  9475  ordiso  9476  oieu  9499  brwdom2  9533  brwdom3  9542  cantnflem1  9649  ttrclselem2  9686  cardidm  9919  carddom2  9937  pm54.43  9961  pr2neOLD  9965  acnen  10013  acnen2  10015  alephord  10035  alephinit  10055  dfac5  10089  infdif2  10169  fictb  10204  coflim  10221  fincssdom  10283  fin23lem25  10284  isf32lem9  10321  isf34lem4  10337  fin1a2lem11  10370  axdc3lem2  10411  ficard  10525  fpwwe2lem11  10601  fpwwe2  10603  indpi  10867  nqereq  10895  1idpr  10989  ltapr  11005  leltne  11270  ltlen  11282  ltadd2  11285  addlsub  11601  addid0  11604  ltord1  11711  mul0or  11825  ldiv  12023  ltmul1  12039  mulge0b  12060  lt2msq  12075  nnsub  12237  nn0sub  12499  zrevaddcl  12585  zltp1le  12590  zdiv  12611  nneo  12625  zeo2  12628  zmax  12911  zbtwnre  12912  qrevaddcl  12937  xrlttri  13106  xrleltne  13112  xralrple  13172  xltneg  13184  xleadd1  13222  xlemul1  13257  supxrunb1  13286  supxrunb2  13287  ioo0  13338  iccid  13358  ico0  13359  ioc0  13360  icc0  13361  difreicc  13452  iccsplit  13453  zltaddlt1le  13473  0fz1  13512  uzsplit  13564  fzm1  13575  fzrevral  13580  ssfzo12bi  13729  elfznelfzob  13741  flge  13774  modid2  13867  modmuladd  13885  ssnn0fi  13957  seqf1olem1  14013  hashen  14319  hashdom  14351  hash2exprb  14443  pr2pwpr  14451  hashtpg  14457  hash3tpexb  14466  len0nnbi  14523  ccats1pfxeqbi  14714  reuccatpfxs1  14719  repsdf2  14750  scshwfzeqfzo  14799  relexpindlem  15036  shftlem  15041  shftuz  15042  abslt  15288  absle  15289  rexico  15327  cau3lem  15328  reusq0  15438  rlim2lt  15470  rlim3  15471  o1lo1  15510  rlimdm  15524  climshft  15549  o1dif  15603  isercolllem2  15639  isercoll  15641  zsum  15691  fsum  15693  fsum00  15771  incexclem  15809  zprod  15910  fprod  15914  dvdsval2  16232  moddvds  16240  negdvdsb  16249  dvdsnegb  16250  dvdscmulr  16261  dvdsmulcr  16262  dvdssub2  16278  dvdsaddre2b  16284  fzo0dvdseq  16300  mod2eq1n2dvds  16324  ltoddhalfle  16338  sumodd  16365  bitsf1ocnv  16421  sadcaddlem  16434  bitsuz  16451  dvdsgcdb  16522  gcdzeq  16529  dvdssqlem  16543  lcmeq0  16577  lcmdvdsb  16590  lcmfeq0b  16607  lcmf  16610  lcmfdvdsb  16620  coprmgcdb  16626  cncongr  16646  isprm2lem  16658  dvdsprime  16664  dvdsprm  16680  isprm7  16685  coprm  16688  euclemma  16690  rpexp  16699  prmdvdsncoprmbd  16704  prmdiveq  16763  hashgcdlem  16765  odzdvds  16773  pythagtrip  16812  pc2dvds  16857  pcprmpw2  16860  pcprmpw  16861  vdwapun  16952  ramtcl2  16989  firest  17402  mrieqv2d  17607  isacs2  17621  isssc  17789  setciso  18060  posasymb  18287  pleval2  18303  pltval3  18305  lublecllem  18326  joinle  18352  meetle  18366  latdisd  18463  lubun  18481  clatleglb  18484  letsr  18559  intopsn  18588  gsumval2a  18619  frmdss2  18797  isgrpid2  18915  isgrpinv  18932  f1ghm0to0  19184  symg1bas  19328  oddvdsnn0  19481  oddvds  19484  odeq  19487  odeq1  19497  gexdvds  19521  pgpfi  19542  pgpssslw  19551  fislw  19562  sylow3lem2  19565  lsmelvalm  19588  lsmlub  19601  lsmss1b  19603  lsmss2b  19605  efgs1b  19673  cyggenod  19821  cyggexb  19836  dprdfeq0  19961  ablsimpgfind  20049  ringinvnz1ne0  20216  ringinvnzdiv  20217  unitmulclb  20297  dvreq1  20327  isnzr2  20434  0ringnnzr  20441  0ring01eqbi  20448  rngciso  20554  ringciso  20588  rrgeq0  20616  domneq0  20624  drngmul0orOLD  20677  isabvd  20728  issrngd  20771  lssats2  20913  lspsneq0  20925  lsmelval2  20999  lvecvs0or  21025  lspsneq  21039  lspsneu  21040  lidl1el  21143  lidldvgen  21251  pzriprnglem10  21407  pzriprnglem11  21408  znunit  21480  psgndif  21518  ipeq0  21554  ocvsscon  21591  pjdm2  21627  obselocv  21644  islinds4  21751  psdmul  22060  ply1coe1eq  22194  cply1coe0bi  22196  mat1dimelbas  22365  cramer  22585  toponcomb  22823  tgss3  22880  clsval2  22944  isopn3  22960  elcls3  22977  opncldf1  22978  neiint  22998  neips  23007  opnneissb  23008  opnssneib  23009  opnnei  23014  tpnei  23015  opnneiid  23020  restcld  23066  restopnb  23069  tgcn  23146  tgcnp  23147  subbascn  23148  iscnp4  23157  cnpnei  23158  cncls2  23167  cncls  23168  cnntr  23169  lmss  23192  hausnei2  23247  lpcls  23258  ordtt1  23273  cmpsub  23294  tgcmp  23295  1stcelcls  23355  locfincmp  23420  kgencn2  23451  ptpjpre1  23465  upxp  23517  txcn  23520  txlm  23542  tgqtop  23606  kqfvima  23624  isr0  23631  regr1lem2  23634  hmeoopn  23660  hmeocld  23661  ptuncnv  23701  fbunfip  23763  fgss2  23768  ufilb  23800  ufprim  23803  trufil  23804  cfinufil  23822  ufildr  23825  elfm2  23842  elfm3  23844  rnelfm  23847  fmfnfmlem4  23851  fmco  23855  flimtopon  23864  flimopn  23869  fbflim2  23871  flimrest  23877  flffbas  23889  cnpflf  23895  fclstopon  23906  fclsnei  23913  fclsbas  23915  fclsfnflim  23921  fclscmp  23924  ufilcmp  23926  isfcf  23928  fcfnei  23929  cnpfcf  23935  alexsubb  23940  alexsubALT  23945  cldsubg  24005  tgphaus  24011  tgpt0  24013  tsmsgsum  24033  tsmsres  24038  xbln0  24309  blssexps  24321  blssex  24322  isxms2  24343  prdsbl  24386  neibl  24396  metss  24403  met2ndc  24418  metrest  24419  metcnp3  24435  tngngp3  24551  nmoeq0  24631  xrsxmet  24705  reconn  24724  iccpnfcnv  24849  fgcfil  25178  iscau4  25186  cfilres  25203  iunmbl2  25465  ismbf3d  25562  mbfaddlem  25568  i1faddlem  25601  i1fmullem  25602  ellimc3  25787  dvfsumlem2  25940  tdeglem4  25972  deg1nn0clb  26002  deg1lt0  26003  dvdsq1p  26075  plypf1  26124  0dgrb  26158  plymul0or  26195  taylthlem2  26289  ulmshft  26306  ulmcaulem  26310  ulmcau  26311  cosord  26447  eff1olem  26464  lognegb  26506  eflogeq  26518  logdivlt  26537  efopn  26574  cxpeq0  26594  cxpeq  26674  angpieqvd  26748  dcubic  26763  asinsinb  26814  acoscosb  26815  atantanb  26841  rlimcnp  26882  isppw  27031  isppw2  27032  vmappw  27033  isnsqf  27052  ppieq0  27093  fsumdvdsdiag  27101  dvdsppwf1o  27103  fsumfldivdiag  27107  chpeq0  27126  chteq0  27127  dchrptlem1  27182  lgsdir2lem4  27246  lgsne0  27253  lgsqr  27269  lgsdchrval  27272  gausslemma2dlem1a  27283  lgsquadlem1  27298  m1lgs  27306  2sqreultblem  27366  2sqreunnltblem  27369  nodenselem8  27610  sltlend  27690  oldlim  27805  sltlpss  27826  sleadd1  27903  sltneg  27958  muls0ord  28095  absslt  28158  onslt  28175  n0subs  28260  n0sltp1le  28262  zs12ge0  28349  iscgrglt  28448  brbtwn  28833  brcgr  28834  brbtwn2  28839  axcontlem7  28904  uhgr0vb  29006  edglnl  29077  ausgrusgrb  29099  ushgredgedg  29163  ushgredgedgloop  29165  usgr0vb  29171  usgr1v  29190  nbupgr  29278  nbumgrvtx  29280  nbuhgr2vtx1edgb  29286  edgusgrnbfin  29307  nb3grprlem1  29314  uvtxnbvtxm1  29340  cusgrfilem2  29391  uhgr0edg0rgrb  29509  cusgrm1rusgr  29517  spthonepeq  29689  usgr2pth  29701  wlkiswwlks  29813  wlkiswwlkupgr  29815  wlklnwwlkn  29821  wlklnwwlknupgr  29823  wwlksnextbi  29831  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  wwlksnextprop  29849  umgrwwlks2on  29894  elwspths2on  29897  usgr2wspthons3  29901  elwwlks2  29903  elwspths2spth  29904  clwlkclwwlklem3  29937  loopclwwlkn1b  29978  clwwlknon1sn  30036  clwwlknonwwlknonb  30042  umgr3v3e3cycl  30120  eupth2lem3lem4  30167  frgr0v  30198  frgr3vlem2  30210  2clwwlk2clwwlk  30286  wlkl0  30303  grpoinvf  30468  nvmul0or  30586  nvz  30605  diporthcom  30652  ubthlem3  30808  hvmul0or  30961  his6  31035  hial0  31038  hial02  31039  orthcom  31044  normgt0  31063  ocin  31232  occon3  31233  shsel3  31251  shlub  31350  chssoc  31432  h1de2bi  31490  spansncol  31504  elspansn4  31509  spansnss2  31511  sumspansn  31585  lnopcnbd  31972  lnfncnbd  31993  riesz1  32001  elpjrn  32126  cvcon3  32220  dmdmd  32236  dmdbr3  32241  dmdbr4  32242  dmdbr5  32244  mdslmd1i  32265  atcveq0  32284  chcv1  32291  atssma  32314  atcv0eq  32315  atcv1  32316  bian1dOLD  32393  disjeq1f  32509  br8d  32545  fpwrelmap  32663  xaddeq0  32683  eliccelico  32707  elicoelioo  32708  indf1ofs  32796  isarchiofld  33302  unitdivcld  33898  xrge0iifcnv  33930  lmxrge0  33949  eulerpartlemgh  34376  dstfrvunirn  34473  fnrelpredd  35086  loop1cycl  35131  cusgracyclt3v  35150  cvmliftmolem2  35276  cvmlift2lem12  35308  satfvsucsuc  35359  satfdm  35363  fmlasuc  35380  satffunlem1lem2  35397  satffunlem2lem2  35400  mthmb  35575  climuzcnv  35665  br8  35750  br6  35751  br4  35752  funbreq  35764  axextbdist  35795  dfrdg4  35946  cgrcom  35985  cgrcoml  35991  cgrdegen  35999  btwncom  36009  brsegle  36103  brsegle2  36104  colinbtwnle  36113  btwnoutside  36120  broutsideof3  36121  outsidele  36127  lineunray  36142  lineelsb2  36143  elhf2  36170  elicc3  36312  nn0prpwlem  36317  opnbnd  36320  cldbnd  36321  opnregcld  36325  cldregopn  36326  fnessref  36352  refssfne  36353  neibastop2  36356  fnemeet2  36362  fnejoin2  36364  fgmin  36365  ontgval  36426  ordtop  36431  ordcmp  36442  nndivsub  36452  bj-19.21t  36764  bj-19.23t  36765  bj-19.42t  36768  bj-sbft  36770  bj-cbv2hv  36792  bj-equsal1t  36817  bj-19.21t0  36825  bj-ceqsalt0  36879  bj-ceqsalt1  36880  bj-xpnzexb  36956  bj-idreseq  37157  bj-imdiridlem  37180  bj-finsumval0  37280  bj-fvimacnv0  37281  bj-isrvec2  37295  bj-bary1  37307  dfgcd3  37319  isbasisrelowllem1  37350  isbasisrelowllem2  37351  finxpsuclem  37392  wl-lem-exsb  37561  wl-mo3t  37571  wl-ax11-lem1  37580  matunitlindf  37619  poimirlem6  37627  poimirlem7  37628  poimirlem16  37637  poimirlem19  37640  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  cnambfre  37669  itg2addnc  37675  brabg2  37718  istotbnd3  37772  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  ssbnd  37789  ismtybnd  37808  reheibor  37840  grpoeqdivid  37882  grpokerinj  37894  rngosn3  37925  rngoueqz  37941  1idl  38027  0rngo  38028  divrngidl  38029  igenval2  38067  ispridlc  38071  isdmn3  38075  relcnveq3  38316  iss2  38333  elrelscnveq3  38489  funALTVeq  38699  disjeq  38733  prtlem10  38865  prter2  38881  dral1-o  38904  lshpinN  38989  lsatcveq0  39032  lsatcv0eq  39047  lsatcv1  39048  islshpcv  39053  lkr0f  39094  lkrshp4  39108  lshpkrlem1  39110  lshpset2N  39119  lfl1dim  39121  lfl1dim2N  39122  lub0N  39189  glb0N  39193  oplecon3b  39200  cmtcomN  39249  cmtbr3N  39254  cmtbr4N  39255  cvrnbtwn2  39275  cvrnbtwn3  39276  cvrcon3b  39277  cvrnbtwn4  39279  cvrcmp  39283  atcvreq0  39314  atnle  39317  atlatle  39320  cvlexchb1  39330  cvlcvr1  39339  hlrelat2  39404  exatleN  39405  cvrval3  39414  cvrval4N  39415  cvrexch  39421  atcvr0eq  39427  lnnat  39428  atcvrj0  39429  atcvrj2b  39433  atltcvr  39436  atbtwn  39447  ps-1  39478  3at  39491  islln2a  39518  llncmp  39523  islpln2a  39549  lplncmp  39563  islvol2aN  39593  4at  39614  lvolcmp  39618  pmaple  39762  lncmp  39784  paddss  39846  llnexchb2lem  39869  2polcon4bN  39919  ispsubcl2N  39948  lhpat3  40047  lautcvr  40093  ltrnid  40136  trlval2  40164  trlatn0  40173  ltrnideq  40176  trlnidatb  40178  cdlemeg49lebilem  40540  trlord  40570  cdlemg1a  40571  cdlemg1cex  40589  tendoid0  40826  dva1dim  40986  cdlemm10N  41119  diarnN  41130  cdlemn  41213  dihlspsnssN  41333  dihatexv  41339  dochkrshp  41387  dochkrshp4  41390  djhlsmcl  41415  lcfl6  41501  lcfl8  41503  lcfrvalsnN  41542  lcfrlem9  41551  mapdval2N  41631  mapdordlem2  41638  mapd1o  41649  mapd0  41666  mapdheq2biN  41731  nnproddivdvdsd  41995  primrootspoweq0  42101  aks6d1c1p1  42102  aks6d1c5lem1  42131  sticksstones11  42151  sticksstones22  42163  grpods  42189  unitscyglem2  42191  eqresfnbd  42227  expeq1d  42319  expeqidd  42320  dvdsexpnn  42328  zdivgd  42332  sn-remul0ord  42403  mulgt0b1d  42467  frlmfzowrdb  42499  frlmsnic  42535  evlselvlem  42581  prjspreln0  42604  elrfi  42689  diophrw  42754  eldioph2b  42758  diophin  42767  rexrabdioph  42789  rmxycomplete  42913  coprmdvdsb  42981  jm2.19  42989  jm2.26  42998  jm2.27  43004  limsuc2  43037  dgraa0p  43145  rngunsnply  43165  fiuneneq  43188  unielss  43214  oaabsb  43290  nnoeomeqom  43308  cantnfresb  43320  tfsconcatrn  43338  tfsconcat0b  43342  tfsconcatrev  43344  oadif1lem  43375  oadif1  43376  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  pwelg  43556  nzss  44313  dvconstbi  44330  expgrowth  44331  bcc0  44336  axc11next  44402  pm14.24  44428  sbiota1  44430  sbcim2g  44535  sineq0ALT  44933  mapss2  45206  fsneq  45207  fsneqrn  45212  mapssbi  45214  rnmptbd2lem  45249  infnsuprnmpt  45251  rnmptbdlem  45256  xralrple2  45357  infxrunb2  45371  xralrple4  45376  xralrple3  45377  xrralrecnnle  45386  xrralrecnnge  45393  reclt0  45394  supxrunb3  45402  supxrleubrnmpt  45409  xrre4  45414  unb2ltle  45418  rexabslelem  45421  suprleubrnmpt  45425  infxrunb3rnmpt  45431  uzub  45434  supminfrnmpt  45448  iccintsng  45528  sqrlearg  45558  uzinico  45564  preimaiocmnf  45565  limcresiooub  45647  limclr  45660  climeldmeq  45670  limsuppnflem  45715  limsupmnflem  45725  limsupmnfuzlem  45731  limsupre3lem  45737  limsupre3uzlem  45740  liminfreuzlem  45807  dvnmul  45948  dvmptfprodlem  45949  ismbl3  45991  ismbl4  45998  fourierdlem50  46161  fourierdlem89  46200  fourierdlem91  46202  dfsalgen2  46346  sge0repnf  46391  sge0lefi  46403  sge0resplit  46411  sge0fodjrnlem  46421  voliunsge0lem  46477  hspdifhsp  46621  isvonmbl  46643  ovnovollem3  46663  vonvolmbl  46666  pimrecltpos  46713  preimaicomnf  46716  pimrecltneg  46729  issmflem  46732  issmfle  46750  issmfgt  46761  smfaddlem1  46768  issmfge  46775  smfresal  46793  smflimmpt  46815  smfinflem  46822  smflimsuplem7  46831  smflimsupmpt  46834  sigarcol  46869  confun  46944  or2expropbi  47039  fsetsniunop  47054  fcoresf1b  47075  f1cof1b  47082  funfocofob  47083  rexsb  47104  euoreqb  47114  ralbinrald  47127  rlimdmafv  47182  fafv2elrnb  47240  tz6.12c-afv2  47247  dfatbrafv2b  47250  fnbrafv2b  47253  rlimdmafv2  47263  f1oresf1o2  47296  el1fzopredsuc  47330  2ffzoeq  47332  modlt0b  47368  imasetpreimafvbijlemfo  47410  iccpartiun  47439  ichnfb  47470  ich2exprop  47476  sprsymrelfolem2  47498  paireqne  47516  prprelprb  47522  reupr  47527  requad01  47626  requad1  47627  requad2  47628  dfodd6  47642  dfeven4  47643  evensumeven  47712  sbgoldbalt  47786  clnbgrel  47833  dfclnbgr6  47860  dfnbgr6  47861  isubgredg  47870  isuspgrim0  47898  isuspgrim  47900  gricushgr  47921  uhgrimisgrgriclem  47934  clnbgrgrim  47938  grimedg  47939  usgrgrtrirex  47953  uspgrlimlem2  47992  uspgrlim  47995  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  isassintop  48202  uzlidlring  48227  rngcisoALTV  48269  ringcisoALTV  48303  domnmsuppn0  48361  lindslininds  48457  snlindsntor  48464  isldepslvec2  48478  affinecomb1  48695  prelrrx2b  48707  rrx2plord2  48715  eenglngeehlnm  48732  rrx2vlinest  48734  line2xlem  48746  line2x  48747  line2y  48748  itsclc0xyqsolb  48763  itsclquadb  48769  mpbiran3d  48789  opnneieqv  48903  iscnrm3lem2  48927  fullthinc2  49444  thincciso  49446