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  2078  elequ1  2120  elequ2  2128  sbequ12  2256  sbft  2274  cbv2w  2339  exsb  2361  dral1v  2371  cbv2  2405  cbv2h  2408  ax12b  2426  dral1  2441  dral1ALT  2442  eupickb  2633  eupickbi  2634  2eu2  2651  ralbi  3089  rexbi  3090  ralbida  3245  ceqsalt  3472  rspcebdv  3568  rspceb2dv  3578  ceqex  3604  elabgtOLD  3625  mob2  3671  reu6  3682  sbciegftOLD  3776  sbcg  3811  2reu2  3846  csbiebt  3876  dfss2  3917  ssdifsym  4224  reupick  4279  reupick2  4281  uneqdifeq  4443  prnebg  4810  preqsnd  4813  prel12g  4818  iuneqconst  4956  disjeq2  5067  disjeq1  5070  disjss3  5095  reusv2lem2  5342  reusv2lem3  5343  alxfr  5350  ralxfrd  5351  ralxfrd2  5355  copsexgw  5436  copsexg  5437  snopeqop  5452  euotd  5459  poeq2  5534  sotric  5560  sotrieq  5561  freq2  5590  seeq1  5592  seeq2  5593  iss  5992  tz7.7  6341  ordtri1  6348  ordelinel  6418  funeq  6510  funssres  6534  f0dom0  6716  fnbrfvb  6882  ssimaex  6917  fvimacnv  6996  elpreima  7001  feldmfvelcdm  7029  eldmrexrnb  7035  fsn  7078  fnsnbg  7108  fnsnbOLD  7110  fmptsng  7112  fmptsnd  7113  fprb  7138  tpres  7145  fconst2g  7147  fconst5  7150  elunirn  7195  f1ocnvfvb  7223  f1prex  7228  foeqcnvco  7244  f1eqcocnv  7245  fliftfun  7256  soisores  7271  isofr  7286  isose  7287  isopo  7290  isoso  7292  f1oiso2  7296  eusvobj2  7348  oprabidw  7387  oprabid  7388  f1opw2  7611  oneqmin  7743  ordelsuc  7760  ordsucelsuc  7762  ordunisuc2  7784  limsuc  7789  fndmexb  7846  resf1ext2b  7875  f1ovv  7900  mptcnfimad  7928  op1steq  7975  opreuopreu  7976  funeldmdif  7990  fvn0elsuppb  8121  extmptsuppeq  8128  rntpos  8179  smoiso2  8299  seqomlem2  8380  oaord  8472  oawordex  8482  oaordex  8483  omord2  8492  om00  8500  oeord  8514  nnaord  8545  nnmord  8558  nnawordex  8563  nnaordex  8564  nnaordex2  8565  eldifsucnn  8590  erexb  8658  swoord1  8665  swoord2  8666  ecelqsdmb  8721  iiner  8724  eceqoveq  8757  mapsnd  8822  ralxpmap  8832  omxpenlem  9004  domtriord  9049  mapxpen  9069  mapunen  9072  ssenen  9077  enfi  9109  nneneq  9128  nndomog  9135  onomeneq  9136  en1eqsnbi  9174  fodomfib  9227  fodomfibOLD  9229  f1opwfi  9254  fsuppunbi  9290  elfiun  9331  suplub2  9362  ordiso2  9418  ordiso  9419  oieu  9442  brwdom2  9476  brwdom3  9485  cantnflem1  9596  ttrclselem2  9633  cardidm  9869  carddom2  9887  pm54.43  9911  acnen  9961  acnen2  9963  alephord  9983  alephinit  10003  dfac5  10037  infdif2  10117  fictb  10152  coflim  10169  fincssdom  10231  fin23lem25  10232  isf32lem9  10269  isf34lem4  10285  fin1a2lem11  10318  axdc3lem2  10359  ficard  10473  fpwwe2lem11  10550  fpwwe2  10552  indpi  10816  nqereq  10844  1idpr  10938  ltapr  10954  leltne  11220  ltlen  11232  ltadd2  11235  addlsub  11551  addid0  11554  ltord1  11661  mul0or  11775  ldiv  11973  ltmul1  11989  mulge0b  12010  lt2msq  12025  nnsub  12187  nn0sub  12449  zrevaddcl  12534  zltp1le  12539  zdiv  12560  nneo  12574  zeo2  12577  zmax  12856  zbtwnre  12857  qrevaddcl  12882  xrlttri  13051  xrleltne  13057  xralrple  13118  xltneg  13130  xleadd1  13168  xlemul1  13203  supxrunb1  13232  supxrunb2  13233  ioo0  13284  iccid  13304  ico0  13305  ioc0  13306  icc0  13307  difreicc  13398  iccsplit  13399  zltaddlt1le  13419  0fz1  13458  uzsplit  13510  fzm1  13521  fzrevral  13526  ssfzo12bi  13675  elfznelfzob  13688  flge  13723  modid2  13816  modmuladd  13834  ssnn0fi  13906  seqf1olem1  13962  hashen  14268  hashdom  14300  hash2exprb  14392  pr2pwpr  14400  hashtpg  14406  hash3tpexb  14415  len0nnbi  14472  ccats1pfxeqbi  14663  reuccatpfxs1  14668  repsdf2  14699  scshwfzeqfzo  14747  relexpindlem  14984  shftlem  14989  shftuz  14990  abslt  15236  absle  15237  rexico  15275  cau3lem  15276  reusq0  15386  rlim2lt  15418  rlim3  15419  o1lo1  15458  rlimdm  15472  climshft  15497  o1dif  15551  isercolllem2  15587  isercoll  15589  zsum  15639  fsum  15641  fsum00  15719  incexclem  15757  zprod  15858  fprod  15862  dvdsval2  16180  moddvds  16188  negdvdsb  16197  dvdsnegb  16198  dvdscmulr  16209  dvdsmulcr  16210  dvdssub2  16226  dvdsaddre2b  16232  fzo0dvdseq  16248  mod2eq1n2dvds  16272  ltoddhalfle  16286  sumodd  16313  bitsf1ocnv  16369  sadcaddlem  16382  bitsuz  16399  dvdsgcdb  16470  gcdzeq  16477  dvdssqlem  16491  lcmeq0  16525  lcmdvdsb  16538  lcmfeq0b  16555  lcmf  16558  lcmfdvdsb  16568  coprmgcdb  16574  cncongr  16594  isprm2lem  16606  dvdsprime  16612  dvdsprm  16628  isprm7  16633  coprm  16636  euclemma  16638  rpexp  16647  prmdvdsncoprmbd  16652  prmdiveq  16711  hashgcdlem  16713  odzdvds  16721  pythagtrip  16760  pc2dvds  16805  pcprmpw2  16808  pcprmpw  16809  vdwapun  16900  ramtcl2  16937  firest  17350  mrieqv2d  17560  isacs2  17574  isssc  17742  setciso  18013  posasymb  18240  pleval2  18256  pltval3  18258  lublecllem  18279  joinle  18305  meetle  18319  latdisd  18418  lubun  18436  clatleglb  18439  letsr  18514  intopsn  18577  gsumval2a  18608  frmdss2  18786  isgrpid2  18904  isgrpinv  18921  f1ghm0to0  19172  symg1bas  19318  oddvdsnn0  19471  oddvds  19474  odeq  19477  odeq1  19487  gexdvds  19511  pgpfi  19532  pgpssslw  19541  fislw  19552  sylow3lem2  19555  lsmelvalm  19578  lsmlub  19591  lsmss1b  19593  lsmss2b  19595  efgs1b  19663  cyggenod  19811  cyggexb  19826  dprdfeq0  19951  ablsimpgfind  20039  ringinvnz1ne0  20233  ringinvnzdiv  20234  unitmulclb  20315  dvreq1  20345  isnzr2  20449  0ringnnzr  20456  0ring01eqbi  20463  rngciso  20569  ringciso  20603  rrgeq0  20631  domneq0  20639  drngmul0orOLD  20692  isabvd  20743  issrngd  20786  lssats2  20949  lspsneq0  20961  lsmelval2  21035  lvecvs0or  21061  lspsneq  21075  lspsneu  21076  lidl1el  21179  lidldvgen  21287  pzriprnglem10  21443  pzriprnglem11  21444  znunit  21516  psgndif  21555  ipeq0  21591  ocvsscon  21628  pjdm2  21664  obselocv  21681  islinds4  21788  psdmul  22107  ply1coe1eq  22242  cply1coe0bi  22244  mat1dimelbas  22413  cramer  22633  toponcomb  22871  tgss3  22928  clsval2  22992  isopn3  23008  elcls3  23025  opncldf1  23026  neiint  23046  neips  23055  opnneissb  23056  opnssneib  23057  opnnei  23062  tpnei  23063  opnneiid  23068  restcld  23114  restopnb  23117  tgcn  23194  tgcnp  23195  subbascn  23196  iscnp4  23205  cnpnei  23206  cncls2  23215  cncls  23216  cnntr  23217  lmss  23240  hausnei2  23295  lpcls  23306  ordtt1  23321  cmpsub  23342  tgcmp  23343  1stcelcls  23403  locfincmp  23468  kgencn2  23499  ptpjpre1  23513  upxp  23565  txcn  23568  txlm  23590  tgqtop  23654  kqfvima  23672  isr0  23679  regr1lem2  23682  hmeoopn  23708  hmeocld  23709  ptuncnv  23749  fbunfip  23811  fgss2  23816  ufilb  23848  ufprim  23851  trufil  23852  cfinufil  23870  ufildr  23873  elfm2  23890  elfm3  23892  rnelfm  23895  fmfnfmlem4  23899  fmco  23903  flimtopon  23912  flimopn  23917  fbflim2  23919  flimrest  23925  flffbas  23937  cnpflf  23943  fclstopon  23954  fclsnei  23961  fclsbas  23963  fclsfnflim  23969  fclscmp  23972  ufilcmp  23974  isfcf  23976  fcfnei  23977  cnpfcf  23983  alexsubb  23988  alexsubALT  23993  cldsubg  24053  tgphaus  24059  tgpt0  24061  tsmsgsum  24081  tsmsres  24086  xbln0  24356  blssexps  24368  blssex  24369  isxms2  24390  prdsbl  24433  neibl  24443  metss  24450  met2ndc  24465  metrest  24466  metcnp3  24482  tngngp3  24598  nmoeq0  24678  xrsxmet  24752  reconn  24771  iccpnfcnv  24896  fgcfil  25225  iscau4  25233  cfilres  25250  iunmbl2  25512  ismbf3d  25609  mbfaddlem  25615  i1faddlem  25648  i1fmullem  25649  ellimc3  25834  dvfsumlem2  25987  tdeglem4  26019  deg1nn0clb  26049  deg1lt0  26050  dvdsq1p  26122  plypf1  26171  0dgrb  26205  plymul0or  26242  taylthlem2  26336  ulmshft  26353  ulmcaulem  26357  ulmcau  26358  cosord  26494  eff1olem  26511  lognegb  26553  eflogeq  26565  logdivlt  26584  efopn  26621  cxpeq0  26641  cxpeq  26721  angpieqvd  26795  dcubic  26810  asinsinb  26861  acoscosb  26862  atantanb  26888  rlimcnp  26929  isppw  27078  isppw2  27079  vmappw  27080  isnsqf  27099  ppieq0  27140  fsumdvdsdiag  27148  dvdsppwf1o  27150  fsumfldivdiag  27154  chpeq0  27173  chteq0  27174  dchrptlem1  27229  lgsdir2lem4  27293  lgsne0  27300  lgsqr  27316  lgsdchrval  27319  gausslemma2dlem1a  27330  lgsquadlem1  27345  m1lgs  27353  2sqreultblem  27413  2sqreunnltblem  27416  nodenselem8  27657  sltlend  27737  oldlim  27859  sltlpss  27880  sleadd1  27959  sltneg  28014  negsleft  28027  negsright  28028  muls0ord  28154  absslt  28217  onslt  28235  n0subs  28322  n0sltp1le  28324  zs12ge0  28432  iscgrglt  28535  brbtwn  28921  brcgr  28922  brbtwn2  28927  axcontlem7  28992  uhgr0vb  29094  edglnl  29165  ausgrusgrb  29187  ushgredgedg  29251  ushgredgedgloop  29253  usgr0vb  29259  usgr1v  29278  nbupgr  29366  nbumgrvtx  29368  nbuhgr2vtx1edgb  29374  edgusgrnbfin  29395  nb3grprlem1  29402  uvtxnbvtxm1  29428  cusgrfilem2  29479  uhgr0edg0rgrb  29597  cusgrm1rusgr  29605  spthonepeq  29774  usgr2pth  29786  wlkiswwlks  29898  wlkiswwlkupgr  29900  wlklnwwlkn  29906  wlklnwwlknupgr  29908  wwlksnextbi  29916  wwlksnredwwlkn0  29918  wwlksnextwrd  29919  wwlksnextprop  29934  usgrwwlks2on  29980  umgrwwlks2on  29981  elwspths2on  29984  elwspths2onw  29985  usgr2wspthons3  29989  elwwlks2  29991  elwspths2spth  29992  clwlkclwwlklem3  30025  loopclwwlkn1b  30066  clwwlknon1sn  30124  clwwlknonwwlknonb  30130  umgr3v3e3cycl  30208  eupth2lem3lem4  30255  frgr0v  30286  frgr3vlem2  30298  2clwwlk2clwwlk  30374  wlkl0  30391  grpoinvf  30556  nvmul0or  30674  nvz  30693  diporthcom  30740  ubthlem3  30896  hvmul0or  31049  his6  31123  hial0  31126  hial02  31127  orthcom  31132  normgt0  31151  ocin  31320  occon3  31321  shsel3  31339  shlub  31438  chssoc  31520  h1de2bi  31578  spansncol  31592  elspansn4  31597  spansnss2  31599  sumspansn  31673  lnopcnbd  32060  lnfncnbd  32081  riesz1  32089  elpjrn  32214  cvcon3  32308  dmdmd  32324  dmdbr3  32329  dmdbr4  32330  dmdbr5  32332  mdslmd1i  32353  atcveq0  32372  chcv1  32379  atssma  32402  atcv0eq  32403  atcv1  32404  bian1dOLD  32480  disjeq1f  32597  br8d  32635  fpwrelmap  32761  xaddeq0  32782  eliccelico  32806  elicoelioo  32807  indf1ofs  32897  isarchiofld  33230  unitdivcld  34007  xrge0iifcnv  34039  lmxrge0  34058  eulerpartlemgh  34484  dstfrvunirn  34581  fnrelpredd  35196  rankfilimb  35207  fineqvnttrclse  35229  loop1cycl  35280  cusgracyclt3v  35299  cvmliftmolem2  35425  cvmlift2lem12  35457  satfvsucsuc  35508  satfdm  35512  fmlasuc  35529  satffunlem1lem2  35546  satffunlem2lem2  35549  mthmb  35724  climuzcnv  35814  br8  35899  br6  35900  br4  35901  funbreq  35913  axextbdist  35941  dfrdg4  36094  cgrcom  36133  cgrcoml  36139  cgrdegen  36147  btwncom  36157  brsegle  36251  brsegle2  36252  colinbtwnle  36261  btwnoutside  36268  broutsideof3  36269  outsidele  36275  lineunray  36290  lineelsb2  36291  elhf2  36318  elicc3  36460  nn0prpwlem  36465  opnbnd  36468  cldbnd  36469  opnregcld  36473  cldregopn  36474  fnessref  36500  refssfne  36501  neibastop2  36504  fnemeet2  36510  fnejoin2  36512  fgmin  36513  ontgval  36574  ordtop  36579  ordcmp  36590  nndivsub  36600  bj-19.21t  36913  bj-19.23t  36914  bj-19.42t  36917  bj-sbft  36919  bj-cbv2hv  36941  bj-equsal1t  36966  bj-19.21t0  36974  bj-ceqsalt0  37028  bj-ceqsalt1  37029  bj-xpnzexb  37105  bj-idreseq  37306  bj-imdiridlem  37329  bj-finsumval0  37429  bj-fvimacnv0  37430  bj-isrvec2  37444  bj-bary1  37456  dfgcd3  37468  isbasisrelowllem1  37499  isbasisrelowllem2  37500  finxpsuclem  37541  wl-lem-exsb  37710  wl-mo3t  37720  matunitlindf  37758  poimirlem6  37766  poimirlem7  37767  poimirlem16  37776  poimirlem19  37779  poimirlem22  37782  poimirlem23  37783  poimirlem24  37784  cnambfre  37808  itg2addnc  37814  brabg2  37857  istotbnd3  37911  sstotbnd2  37914  sstotbnd  37915  sstotbnd3  37916  ssbnd  37928  ismtybnd  37947  reheibor  37979  grpoeqdivid  38021  grpokerinj  38033  rngosn3  38064  rngoueqz  38080  1idl  38166  0rngo  38167  divrngidl  38168  igenval2  38206  ispridlc  38210  isdmn3  38214  relcnveq3  38459  iss2  38476  elrelscnveq3  38739  funALTVeq  38898  disjeq  38932  prtlem10  39064  prter2  39080  dral1-o  39103  lshpinN  39188  lsatcveq0  39231  lsatcv0eq  39246  lsatcv1  39247  islshpcv  39252  lkr0f  39293  lkrshp4  39307  lshpkrlem1  39309  lshpset2N  39318  lfl1dim  39320  lfl1dim2N  39321  lub0N  39388  glb0N  39392  oplecon3b  39399  cmtcomN  39448  cmtbr3N  39453  cmtbr4N  39454  cvrnbtwn2  39474  cvrnbtwn3  39475  cvrcon3b  39476  cvrnbtwn4  39478  cvrcmp  39482  atcvreq0  39513  atnle  39516  atlatle  39519  cvlexchb1  39529  cvlcvr1  39538  hlrelat2  39602  exatleN  39603  cvrval3  39612  cvrval4N  39613  cvrexch  39619  atcvr0eq  39625  lnnat  39626  atcvrj0  39627  atcvrj2b  39631  atltcvr  39634  atbtwn  39645  ps-1  39676  3at  39689  islln2a  39716  llncmp  39721  islpln2a  39747  lplncmp  39761  islvol2aN  39791  4at  39812  lvolcmp  39816  pmaple  39960  lncmp  39982  paddss  40044  llnexchb2lem  40067  2polcon4bN  40117  ispsubcl2N  40146  lhpat3  40245  lautcvr  40291  ltrnid  40334  trlval2  40362  trlatn0  40371  ltrnideq  40374  trlnidatb  40376  cdlemeg49lebilem  40738  trlord  40768  cdlemg1a  40769  cdlemg1cex  40787  tendoid0  41024  dva1dim  41184  cdlemm10N  41317  diarnN  41328  cdlemn  41411  dihlspsnssN  41531  dihatexv  41537  dochkrshp  41585  dochkrshp4  41588  djhlsmcl  41613  lcfl6  41699  lcfl8  41701  lcfrvalsnN  41740  lcfrlem9  41749  mapdval2N  41829  mapdordlem2  41836  mapd1o  41847  mapd0  41864  mapdheq2biN  41929  nnproddivdvdsd  42193  primrootspoweq0  42299  aks6d1c1p1  42300  aks6d1c5lem1  42329  sticksstones11  42349  sticksstones22  42361  grpods  42387  unitscyglem2  42389  eqresfnbd  42430  expeq1d  42521  expeqidd  42522  dvdsexpnn  42530  zdivgd  42534  sn-remul0ord  42605  mulgt0b1d  42669  frlmfzowrdb  42701  frlmsnic  42737  evlselvlem  42771  prjspreln0  42794  elrfi  42878  diophrw  42943  eldioph2b  42947  diophin  42956  rexrabdioph  42978  rmxycomplete  43101  coprmdvdsb  43169  jm2.19  43177  jm2.26  43186  jm2.27  43192  limsuc2  43225  dgraa0p  43333  rngunsnply  43353  fiuneneq  43376  unielss  43402  oaabsb  43478  nnoeomeqom  43496  cantnfresb  43508  tfsconcatrn  43526  tfsconcat0b  43530  tfsconcatrev  43532  oadif1lem  43563  oadif1  43564  fzunt  43638  fzuntd  43639  fzunt1d  43640  fzuntgd  43641  pwelg  43743  nzss  44500  dvconstbi  44517  expgrowth  44518  bcc0  44523  axc11next  44589  pm14.24  44615  sbiota1  44617  sbcim2g  44721  sineq0ALT  45119  mapss2  45391  fsneq  45392  fsneqrn  45397  mapssbi  45399  rnmptbd2lem  45434  infnsuprnmpt  45436  rnmptbdlem  45441  xralrple2  45541  infxrunb2  45554  xralrple4  45559  xralrple3  45560  xrralrecnnle  45569  xrralrecnnge  45576  reclt0  45577  supxrunb3  45585  supxrleubrnmpt  45592  xrre4  45597  unb2ltle  45601  rexabslelem  45604  suprleubrnmpt  45608  infxrunb3rnmpt  45614  uzub  45617  supminfrnmpt  45631  iccintsng  45711  sqrlearg  45741  uzinico  45747  preimaiocmnf  45748  limcresiooub  45828  limclr  45841  climeldmeq  45851  limsuppnflem  45896  limsupmnflem  45906  limsupmnfuzlem  45912  limsupre3lem  45918  limsupre3uzlem  45921  liminfreuzlem  45988  dvnmul  46129  dvmptfprodlem  46130  ismbl3  46172  ismbl4  46179  fourierdlem50  46342  fourierdlem89  46381  fourierdlem91  46383  dfsalgen2  46527  sge0repnf  46572  sge0lefi  46584  sge0resplit  46592  sge0fodjrnlem  46602  voliunsge0lem  46658  hspdifhsp  46802  isvonmbl  46824  ovnovollem3  46844  vonvolmbl  46847  pimrecltpos  46894  preimaicomnf  46897  pimrecltneg  46910  issmflem  46913  issmfle  46931  issmfgt  46942  smfaddlem1  46949  issmfge  46956  smfresal  46974  smflimmpt  46996  smfinflem  47003  smflimsuplem7  47012  smflimsupmpt  47015  sigarcol  47050  confun  47127  or2expropbi  47222  fsetsniunop  47237  fcoresf1b  47258  f1cof1b  47265  funfocofob  47266  rexsb  47287  euoreqb  47297  ralbinrald  47310  rlimdmafv  47365  fafv2elrnb  47423  tz6.12c-afv2  47430  dfatbrafv2b  47433  fnbrafv2b  47436  rlimdmafv2  47446  f1oresf1o2  47479  el1fzopredsuc  47513  2ffzoeq  47515  modlt0b  47551  imasetpreimafvbijlemfo  47593  iccpartiun  47622  ichnfb  47653  ich2exprop  47659  sprsymrelfolem2  47681  paireqne  47699  prprelprb  47705  reupr  47710  requad01  47809  requad1  47810  requad2  47811  dfodd6  47825  dfeven4  47826  evensumeven  47895  sbgoldbalt  47969  clnbgrel  48016  dfclnbgr6  48044  dfnbgr6  48045  isubgredg  48054  isuspgrim0  48082  isuspgrim  48084  gricushgr  48105  uhgrimisgrgriclem  48118  clnbgrgrim  48122  grimedg  48123  usgrgrtrirex  48138  uspgrlimlem2  48177  uspgrlim  48180  gpgedgiov  48253  gpgedg2ov  48254  gpgedg2iv  48255  gpgnbgrvtx0  48262  gpgnbgrvtx1  48263  isassintop  48398  uzlidlring  48423  rngcisoALTV  48465  ringcisoALTV  48499  domnmsuppn0  48557  lindslininds  48652  snlindsntor  48659  isldepslvec2  48673  affinecomb1  48890  prelrrx2b  48902  rrx2plord2  48910  eenglngeehlnm  48927  rrx2vlinest  48929  line2xlem  48941  line2x  48942  line2y  48943  itsclc0xyqsolb  48958  itsclquadb  48964  mpbiran3d  48984  opnneieqv  49098  iscnrm3lem2  49122  fullthinc2  49638  thincciso  49640