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  642  impbida  801  dedlem0b  1045  dedlema  1046  dedlemb  1047  albi  1820  alexbii  1835  equequ1  2027  equequ2  2028  spsbbi  2079  elequ1  2121  elequ2  2129  sbequ12  2259  sbft  2277  cbv2w  2342  exsb  2364  dral1v  2374  cbv2  2408  cbv2h  2411  ax12b  2429  dral1  2444  dral1ALT  2445  eupickb  2636  eupickbi  2637  2eu2  2654  ralbi  3092  rexbi  3093  ralbida  3248  ceqsalt  3475  rspcebdv  3571  rspceb2dv  3581  ceqex  3607  elabgtOLD  3628  mob2  3674  reu6  3685  sbciegftOLD  3779  sbcg  3814  2reu2  3849  csbiebt  3879  dfss2  3920  ssdifsym  4227  reupick  4282  reupick2  4284  uneqdifeq  4446  prnebg  4813  preqsnd  4816  prel12g  4821  iuneqconst  4959  disjeq2  5070  disjeq1  5073  disjss3  5098  reusv2lem2  5345  reusv2lem3  5346  alxfr  5353  ralxfrd  5354  ralxfrd2  5358  copsexgw  5439  copsexg  5440  snopeqop  5455  euotd  5462  poeq2  5537  sotric  5563  sotrieq  5564  freq2  5593  seeq1  5595  seeq2  5596  iss  5995  tz7.7  6344  ordtri1  6351  ordelinel  6421  funeq  6513  funssres  6537  f0dom0  6719  fnbrfvb  6885  ssimaex  6920  fvimacnv  7000  elpreima  7005  feldmfvelcdm  7033  eldmrexrnb  7039  fsn  7082  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fprb  7142  tpres  7149  fconst2g  7151  fconst5  7154  elunirn  7199  f1ocnvfvb  7227  f1prex  7232  foeqcnvco  7248  f1eqcocnv  7249  fliftfun  7260  soisores  7275  isofr  7290  isose  7291  isopo  7294  isoso  7296  f1oiso2  7300  eusvobj2  7352  oprabidw  7391  oprabid  7392  f1opw2  7615  oneqmin  7747  ordelsuc  7764  ordsucelsuc  7766  ordunisuc2  7788  limsuc  7793  fndmexb  7850  resf1ext2b  7879  f1ovv  7904  mptcnfimad  7932  op1steq  7979  opreuopreu  7980  funeldmdif  7994  fvn0elsuppb  8125  extmptsuppeq  8132  rntpos  8183  smoiso2  8303  seqomlem2  8384  oaord  8476  oawordex  8486  oaordex  8487  omord2  8496  om00  8504  oeord  8518  nnaord  8549  nnmord  8562  nnawordex  8567  nnaordex  8568  nnaordex2  8569  eldifsucnn  8594  erexb  8663  swoord1  8670  swoord2  8671  ecelqsdmb  8727  iiner  8730  eceqoveq  8763  mapsnd  8828  ralxpmap  8838  omxpenlem  9010  domtriord  9055  mapxpen  9075  mapunen  9078  ssenen  9083  enfi  9115  nneneq  9134  nndomog  9141  onomeneq  9142  en1eqsnbi  9180  fodomfib  9233  fodomfibOLD  9235  f1opwfi  9260  fsuppunbi  9296  elfiun  9337  suplub2  9368  ordiso2  9424  ordiso  9425  oieu  9448  brwdom2  9482  brwdom3  9491  cantnflem1  9602  ttrclselem2  9639  cardidm  9875  carddom2  9893  pm54.43  9917  acnen  9967  acnen2  9969  alephord  9989  alephinit  10009  dfac5  10043  infdif2  10123  fictb  10158  coflim  10175  fincssdom  10237  fin23lem25  10238  isf32lem9  10275  isf34lem4  10291  fin1a2lem11  10324  axdc3lem2  10365  ficard  10479  fpwwe2lem11  10556  fpwwe2  10558  indpi  10822  nqereq  10850  1idpr  10944  ltapr  10960  leltne  11226  ltlen  11238  ltadd2  11241  addlsub  11557  addid0  11560  ltord1  11667  mul0or  11781  ldiv  11979  ltmul1  11995  mulge0b  12016  lt2msq  12031  nnsub  12193  nn0sub  12455  zrevaddcl  12540  zltp1le  12545  zdiv  12566  nneo  12580  zeo2  12583  zmax  12862  zbtwnre  12863  qrevaddcl  12888  xrlttri  13057  xrleltne  13063  xralrple  13124  xltneg  13136  xleadd1  13174  xlemul1  13209  supxrunb1  13238  supxrunb2  13239  ioo0  13290  iccid  13310  ico0  13311  ioc0  13312  icc0  13313  difreicc  13404  iccsplit  13405  zltaddlt1le  13425  0fz1  13464  uzsplit  13516  fzm1  13527  fzrevral  13532  ssfzo12bi  13681  elfznelfzob  13694  flge  13729  modid2  13822  modmuladd  13840  ssnn0fi  13912  seqf1olem1  13968  hashen  14274  hashdom  14306  hash2exprb  14398  pr2pwpr  14406  hashtpg  14412  hash3tpexb  14421  len0nnbi  14478  ccats1pfxeqbi  14669  reuccatpfxs1  14674  repsdf2  14705  scshwfzeqfzo  14753  relexpindlem  14990  shftlem  14995  shftuz  14996  abslt  15242  absle  15243  rexico  15281  cau3lem  15282  reusq0  15392  rlim2lt  15424  rlim3  15425  o1lo1  15464  rlimdm  15478  climshft  15503  o1dif  15557  isercolllem2  15593  isercoll  15595  zsum  15645  fsum  15647  fsum00  15725  incexclem  15763  zprod  15864  fprod  15868  dvdsval2  16186  moddvds  16194  negdvdsb  16203  dvdsnegb  16204  dvdscmulr  16215  dvdsmulcr  16216  dvdssub2  16232  dvdsaddre2b  16238  fzo0dvdseq  16254  mod2eq1n2dvds  16278  ltoddhalfle  16292  sumodd  16319  bitsf1ocnv  16375  sadcaddlem  16388  bitsuz  16405  dvdsgcdb  16476  gcdzeq  16483  dvdssqlem  16497  lcmeq0  16531  lcmdvdsb  16544  lcmfeq0b  16561  lcmf  16564  lcmfdvdsb  16574  coprmgcdb  16580  cncongr  16600  isprm2lem  16612  dvdsprime  16618  dvdsprm  16634  isprm7  16639  coprm  16642  euclemma  16644  rpexp  16653  prmdvdsncoprmbd  16658  prmdiveq  16717  hashgcdlem  16719  odzdvds  16727  pythagtrip  16766  pc2dvds  16811  pcprmpw2  16814  pcprmpw  16815  vdwapun  16906  ramtcl2  16943  firest  17356  mrieqv2d  17566  isacs2  17580  isssc  17748  setciso  18019  posasymb  18246  pleval2  18262  pltval3  18264  lublecllem  18285  joinle  18311  meetle  18325  latdisd  18424  lubun  18442  clatleglb  18445  letsr  18520  intopsn  18583  gsumval2a  18614  frmdss2  18792  isgrpid2  18910  isgrpinv  18927  f1ghm0to0  19178  symg1bas  19324  oddvdsnn0  19477  oddvds  19480  odeq  19483  odeq1  19493  gexdvds  19517  pgpfi  19538  pgpssslw  19547  fislw  19558  sylow3lem2  19561  lsmelvalm  19584  lsmlub  19597  lsmss1b  19599  lsmss2b  19601  efgs1b  19669  cyggenod  19817  cyggexb  19832  dprdfeq0  19957  ablsimpgfind  20045  ringinvnz1ne0  20239  ringinvnzdiv  20240  unitmulclb  20321  dvreq1  20351  isnzr2  20455  0ringnnzr  20462  0ring01eqbi  20469  rngciso  20575  ringciso  20609  rrgeq0  20637  domneq0  20645  drngmul0orOLD  20698  isabvd  20749  issrngd  20792  lssats2  20955  lspsneq0  20967  lsmelval2  21041  lvecvs0or  21067  lspsneq  21081  lspsneu  21082  lidl1el  21185  lidldvgen  21293  pzriprnglem10  21449  pzriprnglem11  21450  znunit  21522  psgndif  21561  ipeq0  21597  ocvsscon  21634  pjdm2  21670  obselocv  21687  islinds4  21794  psdmul  22113  ply1coe1eq  22248  cply1coe0bi  22250  mat1dimelbas  22419  cramer  22639  toponcomb  22877  tgss3  22934  clsval2  22998  isopn3  23014  elcls3  23031  opncldf1  23032  neiint  23052  neips  23061  opnneissb  23062  opnssneib  23063  opnnei  23068  tpnei  23069  opnneiid  23074  restcld  23120  restopnb  23123  tgcn  23200  tgcnp  23201  subbascn  23202  iscnp4  23211  cnpnei  23212  cncls2  23221  cncls  23222  cnntr  23223  lmss  23246  hausnei2  23301  lpcls  23312  ordtt1  23327  cmpsub  23348  tgcmp  23349  1stcelcls  23409  locfincmp  23474  kgencn2  23505  ptpjpre1  23519  upxp  23571  txcn  23574  txlm  23596  tgqtop  23660  kqfvima  23678  isr0  23685  regr1lem2  23688  hmeoopn  23714  hmeocld  23715  ptuncnv  23755  fbunfip  23817  fgss2  23822  ufilb  23854  ufprim  23857  trufil  23858  cfinufil  23876  ufildr  23879  elfm2  23896  elfm3  23898  rnelfm  23901  fmfnfmlem4  23905  fmco  23909  flimtopon  23918  flimopn  23923  fbflim2  23925  flimrest  23931  flffbas  23943  cnpflf  23949  fclstopon  23960  fclsnei  23967  fclsbas  23969  fclsfnflim  23975  fclscmp  23978  ufilcmp  23980  isfcf  23982  fcfnei  23983  cnpfcf  23989  alexsubb  23994  alexsubALT  23999  cldsubg  24059  tgphaus  24065  tgpt0  24067  tsmsgsum  24087  tsmsres  24092  xbln0  24362  blssexps  24374  blssex  24375  isxms2  24396  prdsbl  24439  neibl  24449  metss  24456  met2ndc  24471  metrest  24472  metcnp3  24488  tngngp3  24604  nmoeq0  24684  xrsxmet  24758  reconn  24777  iccpnfcnv  24902  fgcfil  25231  iscau4  25239  cfilres  25256  iunmbl2  25518  ismbf3d  25615  mbfaddlem  25621  i1faddlem  25654  i1fmullem  25655  ellimc3  25840  dvfsumlem2  25993  tdeglem4  26025  deg1nn0clb  26055  deg1lt0  26056  dvdsq1p  26128  plypf1  26177  0dgrb  26211  plymul0or  26248  taylthlem2  26342  ulmshft  26359  ulmcaulem  26363  ulmcau  26364  cosord  26500  eff1olem  26517  lognegb  26559  eflogeq  26571  logdivlt  26590  efopn  26627  cxpeq0  26647  cxpeq  26727  angpieqvd  26801  dcubic  26816  asinsinb  26867  acoscosb  26868  atantanb  26894  rlimcnp  26935  isppw  27084  isppw2  27085  vmappw  27086  isnsqf  27105  ppieq0  27146  fsumdvdsdiag  27154  dvdsppwf1o  27156  fsumfldivdiag  27160  chpeq0  27179  chteq0  27180  dchrptlem1  27235  lgsdir2lem4  27299  lgsne0  27306  lgsqr  27322  lgsdchrval  27325  gausslemma2dlem1a  27336  lgsquadlem1  27351  m1lgs  27359  2sqreultblem  27419  2sqreunnltblem  27422  nodenselem8  27663  ltlesnd  27747  oldlim  27887  ltslpss  27908  leadds1  27989  ltnegs  28045  negleft  28058  negright  28059  muls0ord  28185  abslts  28249  onlts  28267  n0subs  28363  n0ltsp1le  28365  z12sge0  28483  iscgrglt  28590  brbtwn  28976  brcgr  28977  brbtwn2  28982  axcontlem7  29047  uhgr0vb  29149  edglnl  29220  ausgrusgrb  29242  ushgredgedg  29306  ushgredgedgloop  29308  usgr0vb  29314  usgr1v  29333  nbupgr  29421  nbumgrvtx  29423  nbuhgr2vtx1edgb  29429  edgusgrnbfin  29450  nb3grprlem1  29457  uvtxnbvtxm1  29483  cusgrfilem2  29534  uhgr0edg0rgrb  29652  cusgrm1rusgr  29660  spthonepeq  29829  usgr2pth  29841  wlkiswwlks  29953  wlkiswwlkupgr  29955  wlklnwwlkn  29961  wlklnwwlknupgr  29963  wwlksnextbi  29971  wwlksnredwwlkn0  29973  wwlksnextwrd  29974  wwlksnextprop  29989  usgrwwlks2on  30035  umgrwwlks2on  30036  elwspths2on  30039  elwspths2onw  30040  usgr2wspthons3  30044  elwwlks2  30046  elwspths2spth  30047  clwlkclwwlklem3  30080  loopclwwlkn1b  30121  clwwlknon1sn  30179  clwwlknonwwlknonb  30185  umgr3v3e3cycl  30263  eupth2lem3lem4  30310  frgr0v  30341  frgr3vlem2  30353  2clwwlk2clwwlk  30429  wlkl0  30446  grpoinvf  30611  nvmul0or  30729  nvz  30748  diporthcom  30795  ubthlem3  30951  hvmul0or  31104  his6  31178  hial0  31181  hial02  31182  orthcom  31187  normgt0  31206  ocin  31375  occon3  31376  shsel3  31394  shlub  31493  chssoc  31575  h1de2bi  31633  spansncol  31647  elspansn4  31652  spansnss2  31654  sumspansn  31728  lnopcnbd  32115  lnfncnbd  32136  riesz1  32144  elpjrn  32269  cvcon3  32363  dmdmd  32379  dmdbr3  32384  dmdbr4  32385  dmdbr5  32387  mdslmd1i  32408  atcveq0  32427  chcv1  32434  atssma  32457  atcv0eq  32458  atcv1  32459  bian1dOLD  32534  disjeq1f  32651  br8d  32689  fpwrelmap  32814  xaddeq0  32835  eliccelico  32859  elicoelioo  32860  indf1ofs  32950  isarchiofld  33283  unitdivcld  34060  xrge0iifcnv  34092  lmxrge0  34111  eulerpartlemgh  34537  dstfrvunirn  34634  fnrelpredd  35249  rankfilimb  35260  fineqvnttrclse  35282  loop1cycl  35333  cusgracyclt3v  35352  cvmliftmolem2  35478  cvmlift2lem12  35510  satfvsucsuc  35561  satfdm  35565  fmlasuc  35582  satffunlem1lem2  35599  satffunlem2lem2  35602  mthmb  35777  climuzcnv  35867  br8  35952  br6  35953  br4  35954  funbreq  35966  axextbdist  35994  dfrdg4  36147  cgrcom  36186  cgrcoml  36192  cgrdegen  36200  btwncom  36210  brsegle  36304  brsegle2  36305  colinbtwnle  36314  btwnoutside  36321  broutsideof3  36322  outsidele  36328  lineunray  36343  lineelsb2  36344  elhf2  36371  elicc3  36513  nn0prpwlem  36518  opnbnd  36521  cldbnd  36522  opnregcld  36526  cldregopn  36527  fnessref  36553  refssfne  36554  neibastop2  36557  fnemeet2  36563  fnejoin2  36565  fgmin  36566  ontgval  36627  ordtop  36632  ordcmp  36643  nndivsub  36653  bj-19.21t  36972  bj-19.23t  36973  bj-19.42t  36976  bj-sbft  36978  bj-cbv2hv  37000  bj-equsal1t  37025  bj-19.21t0  37033  bj-ceqsalt0  37087  bj-ceqsalt1  37088  bj-xpnzexb  37164  bj-idreseq  37369  bj-imdiridlem  37392  bj-finsumval0  37492  bj-fvimacnv0  37493  bj-isrvec2  37507  bj-bary1  37519  dfgcd3  37531  isbasisrelowllem1  37562  isbasisrelowllem2  37563  finxpsuclem  37604  wl-lem-exsb  37773  wl-mo3t  37783  matunitlindf  37821  poimirlem6  37829  poimirlem7  37830  poimirlem16  37839  poimirlem19  37842  poimirlem22  37845  poimirlem23  37846  poimirlem24  37847  cnambfre  37871  itg2addnc  37877  brabg2  37920  istotbnd3  37974  sstotbnd2  37977  sstotbnd  37978  sstotbnd3  37979  ssbnd  37991  ismtybnd  38010  reheibor  38042  grpoeqdivid  38084  grpokerinj  38096  rngosn3  38127  rngoueqz  38143  1idl  38229  0rngo  38230  divrngidl  38231  igenval2  38269  ispridlc  38273  isdmn3  38277  relcnveq3  38530  iss2  38547  elrelscnveq3  38830  funALTVeq  38988  disjeq  39037  prtlem10  39193  prter2  39209  dral1-o  39232  lshpinN  39317  lsatcveq0  39360  lsatcv0eq  39375  lsatcv1  39376  islshpcv  39381  lkr0f  39422  lkrshp4  39436  lshpkrlem1  39438  lshpset2N  39447  lfl1dim  39449  lfl1dim2N  39450  lub0N  39517  glb0N  39521  oplecon3b  39528  cmtcomN  39577  cmtbr3N  39582  cmtbr4N  39583  cvrnbtwn2  39603  cvrnbtwn3  39604  cvrcon3b  39605  cvrnbtwn4  39607  cvrcmp  39611  atcvreq0  39642  atnle  39645  atlatle  39648  cvlexchb1  39658  cvlcvr1  39667  hlrelat2  39731  exatleN  39732  cvrval3  39741  cvrval4N  39742  cvrexch  39748  atcvr0eq  39754  lnnat  39755  atcvrj0  39756  atcvrj2b  39760  atltcvr  39763  atbtwn  39774  ps-1  39805  3at  39818  islln2a  39845  llncmp  39850  islpln2a  39876  lplncmp  39890  islvol2aN  39920  4at  39941  lvolcmp  39945  pmaple  40089  lncmp  40111  paddss  40173  llnexchb2lem  40196  2polcon4bN  40246  ispsubcl2N  40275  lhpat3  40374  lautcvr  40420  ltrnid  40463  trlval2  40491  trlatn0  40500  ltrnideq  40503  trlnidatb  40505  cdlemeg49lebilem  40867  trlord  40897  cdlemg1a  40898  cdlemg1cex  40916  tendoid0  41153  dva1dim  41313  cdlemm10N  41446  diarnN  41457  cdlemn  41540  dihlspsnssN  41660  dihatexv  41666  dochkrshp  41714  dochkrshp4  41717  djhlsmcl  41742  lcfl6  41828  lcfl8  41830  lcfrvalsnN  41869  lcfrlem9  41878  mapdval2N  41958  mapdordlem2  41965  mapd1o  41976  mapd0  41993  mapdheq2biN  42058  nnproddivdvdsd  42322  primrootspoweq0  42428  aks6d1c1p1  42429  aks6d1c5lem1  42458  sticksstones11  42478  sticksstones22  42490  grpods  42516  unitscyglem2  42518  eqresfnbd  42556  expeq1d  42646  expeqidd  42647  dvdsexpnn  42655  zdivgd  42659  sn-remul0ord  42730  mulgt0b1d  42794  frlmfzowrdb  42826  frlmsnic  42862  evlselvlem  42896  prjspreln0  42919  elrfi  43003  diophrw  43068  eldioph2b  43072  diophin  43081  rexrabdioph  43103  rmxycomplete  43226  coprmdvdsb  43294  jm2.19  43302  jm2.26  43311  jm2.27  43317  limsuc2  43350  dgraa0p  43458  rngunsnply  43478  fiuneneq  43501  unielss  43527  oaabsb  43603  nnoeomeqom  43621  cantnfresb  43633  tfsconcatrn  43651  tfsconcat0b  43655  tfsconcatrev  43657  oadif1lem  43688  oadif1  43689  fzunt  43763  fzuntd  43764  fzunt1d  43765  fzuntgd  43766  pwelg  43868  nzss  44625  dvconstbi  44642  expgrowth  44643  bcc0  44648  axc11next  44714  pm14.24  44740  sbiota1  44742  sbcim2g  44846  sineq0ALT  45244  mapss2  45516  fsneq  45517  fsneqrn  45522  mapssbi  45524  rnmptbd2lem  45559  infnsuprnmpt  45561  rnmptbdlem  45566  xralrple2  45666  infxrunb2  45679  xralrple4  45684  xralrple3  45685  xrralrecnnle  45694  xrralrecnnge  45701  reclt0  45702  supxrunb3  45710  supxrleubrnmpt  45717  xrre4  45722  unb2ltle  45726  rexabslelem  45729  suprleubrnmpt  45733  infxrunb3rnmpt  45739  uzub  45742  supminfrnmpt  45756  iccintsng  45836  sqrlearg  45866  uzinico  45872  preimaiocmnf  45873  limcresiooub  45953  limclr  45966  climeldmeq  45976  limsuppnflem  46021  limsupmnflem  46031  limsupmnfuzlem  46037  limsupre3lem  46043  limsupre3uzlem  46046  liminfreuzlem  46113  dvnmul  46254  dvmptfprodlem  46255  ismbl3  46297  ismbl4  46304  fourierdlem50  46467  fourierdlem89  46506  fourierdlem91  46508  dfsalgen2  46652  sge0repnf  46697  sge0lefi  46709  sge0resplit  46717  sge0fodjrnlem  46727  voliunsge0lem  46783  hspdifhsp  46927  isvonmbl  46949  ovnovollem3  46969  vonvolmbl  46972  pimrecltpos  47019  preimaicomnf  47022  pimrecltneg  47035  issmflem  47038  issmfle  47056  issmfgt  47067  smfaddlem1  47074  issmfge  47081  smfresal  47099  smflimmpt  47121  smfinflem  47128  smflimsuplem7  47137  smflimsupmpt  47140  sigarcol  47175  confun  47252  or2expropbi  47347  fsetsniunop  47362  fcoresf1b  47383  f1cof1b  47390  funfocofob  47391  rexsb  47412  euoreqb  47422  ralbinrald  47435  rlimdmafv  47490  fafv2elrnb  47548  tz6.12c-afv2  47555  dfatbrafv2b  47558  fnbrafv2b  47561  rlimdmafv2  47571  f1oresf1o2  47604  el1fzopredsuc  47638  2ffzoeq  47640  modlt0b  47676  imasetpreimafvbijlemfo  47718  iccpartiun  47747  ichnfb  47778  ich2exprop  47784  sprsymrelfolem2  47806  paireqne  47824  prprelprb  47830  reupr  47835  requad01  47934  requad1  47935  requad2  47936  dfodd6  47950  dfeven4  47951  evensumeven  48020  sbgoldbalt  48094  clnbgrel  48141  dfclnbgr6  48169  dfnbgr6  48170  isubgredg  48179  isuspgrim0  48207  isuspgrim  48209  gricushgr  48230  uhgrimisgrgriclem  48243  clnbgrgrim  48247  grimedg  48248  usgrgrtrirex  48263  uspgrlimlem2  48302  uspgrlim  48305  gpgedgiov  48378  gpgedg2ov  48379  gpgedg2iv  48380  gpgnbgrvtx0  48387  gpgnbgrvtx1  48388  isassintop  48523  uzlidlring  48548  rngcisoALTV  48590  ringcisoALTV  48624  domnmsuppn0  48682  lindslininds  48777  snlindsntor  48784  isldepslvec2  48798  affinecomb1  49015  prelrrx2b  49027  rrx2plord2  49035  eenglngeehlnm  49052  rrx2vlinest  49054  line2xlem  49066  line2x  49067  line2y  49068  itsclc0xyqsolb  49083  itsclquadb  49089  mpbiran3d  49109  opnneieqv  49223  iscnrm3lem2  49247  fullthinc2  49763  thincciso  49765