Theorem impbid 215

Description: Deduce an equivalence from two implications. Deduction associated with impbi 211 and impbii 212. (Contributed by NM, 24-Jan-1993.) Prove it from impbid21d 214. (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 214	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 53	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom1  224  impbid1  228  impcon4bid  230  pm5.74  273  imbi1d  344  pm5.501  369  anbiimOLD  653  impbida  812  dedlem0b  1060  dedlema  1061  dedlemb  1062  albi  1848  alexbii  1863  equequ1  2055  equequ2  2056  spsbbi  2107  elequ1  2150  elequ2  2158  sbequ12  2287  sbft  2305  cbv2w  2369  exsb  2391  dral1v  2401  cbv2  2435  cbv2h  2438  ax12b  2456  dral1  2471  dral1ALT  2472  eupickb  2663  eupickbi  2664  2eu2  2680  ralbi  3120  rexbi  3121  ralbida  3276  ceqsalt  3488  rspcebdv  3575  rspceb2dv  3585  ceqex  3611  elabgtOLD  3632  mob2  3678  reu6  3689  sbcg  3816  2reu2  3852  csbiebt  3882  dfss2  3923  reupick  4282  reupick2  4284  uneqdifeq  4453  prnebg  4821  preqsnd  4824  prel12g  4829  iuneqconst  4968  disjeq2  5080  disjeq1  5083  disjss3  5108  reusv2lem2  5370  reusv2lem3  5371  alxfr  5378  ralxfrd  5379  ralxfrd2  5383  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  snopeqop  5489  euotd  5496  poeq2  5573  sotric  5599  sotrieq  5600  freq2  5629  seeq1  5631  seeq2  5632  iss  6037  tz7.7  6386  ordtri1  6394  ordelinel  6464  funeq  6556  funssres  6580  f0dom0  6762  fnbrfvb  6931  ssimaex  6966  fsneq  7030  fvimacnv  7048  elpreima  7053  feldmfvelcdm  7081  eldmrexrnb  7087  fsn  7131  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  fprb  7192  tpres  7199  fconst2g  7201  fconst5  7204  elunirn  7249  f1ocnvfvb  7277  f1prex  7282  foeqcnvco  7298  f1eqcocnv  7299  fliftfun  7310  soisores  7325  isofr  7340  isose  7341  isopo  7344  isoso  7346  f1oiso2  7350  eusvobj2  7402  oprabidw  7441  oprabid  7442  f1opw2  7665  oneqmin  7795  ordelsuc  7812  ordsucelsuc  7814  ordunisuc2  7836  limsuc  7841  fndmexb  7899  resf1ext2b  7928  f1ovv  7951  mptcnfimad  7979  op1steq  8026  opreuopreu  8027  funeldmdif  8041  fvn0elsuppb  8173  extmptsuppeq  8180  rntpos  8231  smoiso2  8352  seqomlem2  8434  oaord  8528  oawordex  8538  oaordex  8539  omord2  8548  om00  8556  oeord  8570  nnaord  8601  nnmord  8614  nnawordex  8619  nnaordex  8620  nnaordex2  8621  eldifsucnn  8646  erexb  8716  swoord1  8723  swoord2  8724  ecelqsdmb  8780  iiner  8783  eceqoveq  8816  mapsnd  8880  ralxpmap  8890  omxpenlem  9062  domtriord  9107  mapxpen  9127  mapunen  9130  ssenen  9135  enfi  9167  nneneq  9186  nndomog  9193  onomeneq  9194  en1eqsnbi  9232  fodomfib  9284  f1opwfi  9309  fsuppunbi  9345  elfiun  9386  suplub2  9417  ordiso2  9473  ordiso  9474  oieu  9497  brwdom2  9531  brwdom3  9540  cantnflem1  9654  ttrclselem2  9691  cardidm  9950  carddom2  9968  pm54.43  9992  acnen  10042  acnen2  10044  alephord  10064  alephinit  10084  dfac5  10117  infdif2  10197  fictb  10232  coflim  10249  fincssdom  10311  fin23lem25  10312  isf32lem9  10349  isf34lem4  10365  fin1a2lem11  10398  axdc3lem2  10439  ficard  10553  fpwwe2lem11  10630  fpwwe2  10632  indpi  10896  nqereq  10924  1idpr  11018  ltapr  11034  leltne  11303  ltlen  11315  ltadd2  11318  addlsub  11634  addid0  11637  ltord1  11744  mul0or  11858  ldiv  12053  ltmul1  12069  mulge0b  12089  lt2msq  12104  nnsub  12284  nn0sub  12558  zrevaddcl  12643  zltp1le  12648  zdiv  12670  nneo  12684  zeo2  12687  zmax  12973  zbtwnre  12974  qrevaddcl  12999  xrlttri  13168  xrleltne  13174  xralrple  13235  xltneg  13247  xleadd1  13285  xlemul1  13320  supxrunb1  13349  supxrunb2  13350  ioo0  13401  iccid  13421  ico0  13422  ioc0  13423  icc0  13424  difreicc  13515  iccsplit  13516  zltaddlt1le  13536  0fz1  13576  uzsplit  13629  fzm1  13640  fzrevral  13645  ssfzo12bi  13795  elfznelfzob  13808  flge  13843  modid2  13936  modmuladd  13954  ssnn0fi  14026  seqf1olem1  14082  hashen  14388  hashdom  14420  hash2exprb  14513  pr2pwpr  14521  hashtpg  14527  hash3tpexb  14536  len0nnbi  14593  ccats1pfxeqbi  14784  reuccatpfxs1  14789  repsdf2  14820  scshwfzeqfzo  14868  relexpindlem  15105  shftlem  15110  shftuz  15111  abslt  15371  absle  15372  rexico  15410  cau3lem  15411  reusq0  15521  rlim2lt  15553  rlim3  15554  o1lo1  15593  rlimdm  15607  climshft  15632  o1dif  15686  isercolllem2  15722  isercoll  15724  zsum  15774  fsum  15776  fsum00  15855  incexclem  15895  zprod  15996  fprod  16000  dvdsval2  16317  moddvds  16325  negdvdsb  16334  dvdsnegb  16335  dvdscmulr  16346  dvdsmulcr  16347  dvdssub2  16363  dvdsaddre2b  16369  fzo0dvdseq  16385  mod2eq1n2dvds  16409  ltoddhalfle  16423  sumodd  16450  bitsf1ocnv  16506  sadcaddlem  16519  bitsuz  16536  dvdsgcdb  16607  gcdzeq  16614  dvdssqlem  16628  lcmeq0  16662  lcmdvdsb  16675  lcmfeq0b  16692  lcmf  16695  lcmfdvdsb  16705  coprmgcdb  16711  cncongr  16731  isprm2lem  16743  dvdsprime  16749  dvdsprm  16766  isprm7  16771  coprm  16774  euclemma  16776  rpexp  16785  prmdvdsncoprmbd  16790  prmdiveq  16849  hashgcdlem  16851  odzdvds  16859  pythagtrip  16898  pc2dvds  16943  pcprmpw2  16946  pcprmpw  16947  vdwapun  17038  ramtcl2  17075  firest  17489  mrieqv2d  17699  isacs2  17713  isssc  17881  setciso  18152  posasymb  18379  pleval2  18395  pltval3  18397  lublecllem  18418  joinle  18444  meetle  18458  latdisd  18557  lubun  18575  clatleglb  18578  letsr  18653  intopsn  18716  gsumval2a  18747  frmdss2  18926  isgrpid2  19047  isgrpinv  19064  f1ghm0to0  19319  symg1bas  19465  oddvdsnn0  19618  oddvds  19621  odeq  19624  odeq1  19634  gexdvds  19658  pgpfi  19679  pgpssslw  19688  fislw  19699  sylow3lem2  19702  lsmelvalm  19725  lsmlub  19738  lsmss1b  19740  lsmss2b  19742  efgs1b  19810  cyggenod  19958  cyggexb  19973  dprdfeq0  20098  ablsimpgfind  20186  ringinvnz1ne0  20388  ringinvnzdiv  20389  unitmulclb  20468  dvreq1  20498  isnzr2  20624  0ringnnzr  20632  0ring01eqbi2  20639  0ring01eqbi  20640  rngciso  20746  ringciso  20780  rrgeq0  20808  domneq0  20816  isabvd  20924  issrngd  20967  lssats2  21130  lspsneq0  21142  lsmelval2  21215  lvecvs0or  21241  lspsneq  21255  lspsneu  21256  lidl1el  21360  rspprop  21379  lidldvgen  21511  pzriprnglem10  21649  pzriprnglem11  21650  znunit  21722  psgndif  21761  ipeq0  21797  ocvsscon  21834  pjdm2  21870  obselocv  21887  islinds4  21994  psdmul  22338  ply1coe1eq  22469  cply1coe0bi  22471  mat1dimelbas  22637  cramer  22857  toponcomb  23095  tgss3  23152  clsval2  23216  isopn3  23232  elcls3  23249  opncldf1  23250  neiint  23270  neips  23279  opnneissb  23280  opnssneib  23281  opnnei  23286  tpnei  23287  opnneiid  23292  restcld  23338  restopnb  23341  tgcn  23418  tgcnp  23419  subbascn  23420  iscnp4  23429  cnpnei  23430  cncls2  23439  cncls  23440  cnntr  23441  lmss  23464  hausnei2  23519  lpcls  23530  ordtt1  23545  cmpsub  23566  tgcmp  23567  1stcelcls  23627  locfincmp  23692  kgencn2  23723  ptpjpre1  23737  upxp  23789  txcn  23792  txlm  23814  tgqtop  23878  kqfvima  23896  isr0  23903  regr1lem2  23906  hmeoopn  23932  hmeocld  23933  ptuncnv  23973  fbunfip  24035  fgss2  24040  ufilb  24072  ufprim  24075  trufil  24076  cfinufil  24094  ufildr  24097  elfm2  24114  elfm3  24116  rnelfm  24119  fmfnfmlem4  24123  fmco  24127  flimtopon  24136  flimopn  24141  fbflim2  24143  flimrest  24149  flffbas  24161  cnpflf  24167  fclstopon  24178  fclsnei  24185  fclsbas  24187  fclsfnflim  24193  fclscmp  24196  ufilcmp  24198  isfcf  24200  fcfnei  24201  cnpfcf  24207  alexsubb  24212  alexsubALT  24217  cldsubg  24277  tgphaus  24283  tgpt0  24285  tsmsgsum  24305  tsmsres  24310  xbln0  24580  blssexps  24592  blssex  24593  isxms2  24614  prdsbl  24657  neibl  24667  metss  24674  met2ndc  24689  metrest  24690  metcnp3  24706  tngngp3  24822  nmoeq0  24902  xrsxmet  24976  reconn  24995  iccpnfcnv  25112  fgcfil  25439  iscau4  25447  cfilres  25464  iunmbl2  25725  ismbf3d  25822  mbfaddlem  25828  i1faddlem  25861  i1fmullem  25862  ellimc3  26047  dvfsumlem2  26195  tdeglem4  26226  deg1nn0clb  26256  deg1lt0  26257  dvdsq1p  26329  plypf1  26378  0dgrb  26412  plymul0or  26448  taylthlem2  26546  ulmshft  26562  ulmcaulem  26566  ulmcau  26567  cosord  26705  eff1olem  26722  lognegb  26764  eflogeq  26776  logdivlt  26795  efopn  26832  cxpeq0  26852  cxpeq  26931  angpieqvd  27005  dcubic  27020  asinsinb  27071  acoscosb  27072  atantanb  27098  rlimcnp  27139  isppw  27287  isppw2  27288  vmappw  27289  isnsqf  27308  ppieq0  27349  fsumdvdsdiag  27357  dvdsppwf1o  27359  fsumfldivdiag  27363  chpeq0  27381  chteq0  27382  dchrptlem1  27437  lgsdir2lem4  27501  lgsne0  27508  lgsqr  27524  lgsdchrval  27527  gausslemma2dlem1a  27538  lgsquadlem1  27553  m1lgs  27561  2sqreultblem  27621  2sqreunnltblem  27624  nodenselem8  27864  ltlesnd  27948  oldlim  28089  ltslpss  28110  leadds1  28191  ltnegs  28247  negleft  28260  negright  28261  muls0ord  28387  abslts  28451  onlts  28469  n0subs  28565  n0ltsp1le  28567  z12sge0  28685  iscgrglt  28792  brbtwn  29258  brcgr  29259  brbtwn2  29264  axcontlem7  29329  uhgr0vb  29431  edglnl  29502  ausgrusgrb  29524  ushgredgedg  29588  ushgredgedgloop  29590  usgr0vb  29596  usgr1v  29615  nbupgr  29703  nbumgrvtx  29705  nbuhgr2vtx1edgb  29711  edgusgrnbfin  29732  nb3grprlem1  29739  uvtxnbvtxm1  29765  cusgrfilem2  29815  uhgr0edg0rgrb  29933  cusgrm1rusgr  29941  spthonepeq  30110  usgr2pth  30122  wlkiswwlks  30234  wlkiswwlkupgr  30236  wlklnwwlkn  30242  wlklnwwlknupgr  30244  wwlksnextbi  30252  wwlksnredwwlkn0  30254  wwlksnextwrd  30255  wwlksnextprop  30270  usgrwwlks2on  30316  umgrwwlks2on  30317  elwspths2on  30320  elwspths2onw  30321  usgr2wspthons3  30325  elwwlks2  30327  elwspths2spth  30328  clwlkclwwlklem3  30361  loopclwwlkn1b  30402  clwwlknon1sn  30460  clwwlknonwwlknonb  30466  umgr3v3e3cycl  30544  eupth2lem3lem4  30591  frgr0v  30622  frgr3vlem2  30634  2clwwlk2clwwlk  30710  wlkl0  30727  grpoinvf  30893  nvmul0or  31011  nvz  31030  diporthcom  31077  ubthlem3  31233  hvmul0or  31386  his6  31460  hial0  31463  hial02  31464  orthcom  31469  normgt0  31488  ocin  31657  occon3  31658  shsel3  31676  shlub  31775  chssoc  31857  h1de2bi  31915  spansncol  31929  elspansn4  31934  spansnss2  31936  sumspansn  32010  lnopcnbd  32397  lnfncnbd  32418  riesz1  32426  elpjrn  32551  cvcon3  32645  dmdmd  32661  dmdbr3  32666  dmdbr4  32667  dmdbr5  32669  mdslmd1i  32690  atcveq0  32709  chcv1  32716  atssma  32739  atcv0eq  32740  atcv1  32741  disjeq1f  32927  br8d  32962  fpwrelmap  33087  xaddeq0  33107  eliccelico  33131  elicoelioo  33132  indf1ofs  33195  isarchiofld  33528  unitdivcld  34300  xrge0iifcnv  34332  lmxrge0  34351  eulerpartlemgh  34777  dstfrvunirn  34874  fnfvintima  35485  fnrelpredd  35491  rankfilimb  35505  fineqvnttrclse  35545  loop1cycl  35637  cusgracyclt3v  35656  cvmliftmolem2  35782  cvmlift2lem12  35814  satfvsucsuc  35865  satfdm  35869  fmlasuc  35886  satffunlem1lem2  35903  satffunlem2lem2  35906  mthmb  36081  climuzcnv  36171  br8  36256  br6  36257  br4  36258  funbreq  36270  axextbdist  36298  dfrdg4  36451  cgrcom  36490  cgrcoml  36496  cgrdegen  36504  btwncom  36514  brsegle  36608  brsegle2  36609  colinbtwnle  36618  btwnoutside  36625  broutsideof3  36626  outsidele  36632  lineunray  36647  lineelsb2  36648  elhf2  36675  ltnmul  36716  ltnadd  36718  elicc3  36856  nn0prpwlem  36861  opnbnd  36864  cldbnd  36865  opnregcld  36869  cldregopn  36870  fnessref  36896  refssfne  36897  neibastop2  36900  fnemeet2  36906  fnejoin2  36908  fgmin  36909  ontgval  36970  ordtop  36975  ordcmp  36986  nndivsub  36996  bj-cbval  37296  bj-cbvex  37297  bj-19.21t  37414  bj-19.23t  37415  bj-19.42t  37418  bj-sbft  37431  bj-nnf-cbval  37433  bj-cbv2hv  37460  bj-equsal1t  37485  bj-19.21t0  37493  bj-ceqsalt0  37547  bj-ceqsalt1  37548  bj-xpnzexb  37625  bj-axreprepsep  37740  cgsex2gd  37809  bj-idreseq  37834  bj-imdiridlem  37857  bj-finsumval0  37957  bj-fvimacnv0  37958  bj-isrvec2  37972  bj-bary1  37984  dfgcd3  37996  isbasisrelowllem1  38029  isbasisrelowllem2  38030  finxpsuclem  38071  wl-lem-exsb  38249  wl-mo3t  38259  matunitlindf  38297  poimirlem6  38305  poimirlem7  38306  poimirlem16  38315  poimirlem19  38318  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  cnambfre  38347  itg2addnc  38353  brabg2  38396  istotbnd3  38450  sstotbnd2  38453  sstotbnd  38454  sstotbnd3  38455  ssbnd  38467  ismtybnd  38486  reheibor  38518  grpoeqdivid  38560  grpokerinj  38572  rngosn3  38603  rngoueqz  38619  1idl  38705  0rngo  38706  divrngidl  38707  igenval2  38745  ispridlc  38749  isdmn3  38753  relcnveq3  39004  iss2  39021  elrelscnveq3  39304  funALTVeq  39462  disjeq  39511  prtlem10  39667  prter2  39683  dral1-o  39706  lshpinN  39791  lsatcveq0  39834  lsatcv0eq  39849  lsatcv1  39850  islshpcv  39855  lkr0f  39896  lkrshp4  39910  lshpkrlem1  39912  lshpset2N  39921  lfl1dim  39923  lfl1dim2N  39924  lub0N  39991  glb0N  39995  oplecon3b  40002  cmtcomN  40051  cmtbr3N  40056  cmtbr4N  40057  cvrnbtwn2  40077  cvrnbtwn3  40078  cvrcon3b  40079  cvrnbtwn4  40081  cvrcmp  40085  atcvreq0  40116  atnle  40119  atlatle  40122  cvlexchb1  40132  cvlcvr1  40141  hlrelat2  40205  exatleN  40206  cvrval3  40215  cvrval4N  40216  cvrexch  40222  atcvr0eq  40228  lnnat  40229  atcvrj0  40230  atcvrj2b  40234  atltcvr  40237  atbtwn  40248  ps-1  40279  3at  40292  islln2a  40319  llncmp  40324  islpln2a  40350  lplncmp  40364  islvol2aN  40394  4at  40415  lvolcmp  40419  pmaple  40563  lncmp  40585  paddss  40647  llnexchb2lem  40670  2polcon4bN  40720  ispsubcl2N  40749  lhpat3  40848  lautcvr  40894  ltrnid  40937  trlval2  40965  trlatn0  40974  ltrnideq  40977  trlnidatb  40979  cdlemeg49lebilem  41341  trlord  41371  cdlemg1a  41372  cdlemg1cex  41390  tendoid0  41627  dva1dim  41787  cdlemm10N  41920  diarnN  41931  cdlemn  42014  dihlspsnssN  42134  dihatexv  42140  dochkrshp  42188  dochkrshp4  42191  djhlsmcl  42216  lcfl6  42302  lcfl8  42304  lcfrvalsnN  42343  lcfrlem9  42352  mapdval2N  42432  mapdordlem2  42439  mapd1o  42450  mapd0  42467  mapdheq2biN  42532  nnproddivdvdsd  42795  primrootspoweq0  42901  aks6d1c1p1  42902  aks6d1c5lem1  42931  sticksstones11  42951  sticksstones22  42963  grpods  42989  unitscyglem2  42991  eqresfnbd  43031  expeq1d  43113  expeqidd  43114  dvdsexpnn  43122  zdivgd  43126  sn-remul0ord  43197  mulgt0b1d  43274  frlmfzowrdb  43306  frlmsnic  43336  evlselvlem  43348  prjspreln0  43369  elrfi  43453  diophrw  43518  eldioph2b  43522  diophin  43531  rexrabdioph  43549  rmxycomplete  43672  coprmdvdsb  43740  jm2.19  43748  jm2.26  43757  jm2.27  43763  limsuc2  43796  dgraa0p  43904  rngunsnply  43924  fiuneneq  43947  unielss  43973  oaabsb  44049  nnoeomeqom  44067  cantnfresb  44079  tfsconcatrn  44097  tfsconcat0b  44101  tfsconcatrev  44103  oadif1lem  44134  oadif1  44135  fzunt  44209  fzuntd  44210  fzunt1d  44211  fzuntgd  44212  pwelg  44314  nzss  45055  dvconstbi  45072  expgrowth  45073  bcc0  45078  axc11next  45144  pm14.24  45170  sbiota1  45172  sbcim2g  45275  sineq0ALT  45673  mapss2  45950  fsneqrn  45955  mapssbi  45957  rnmptbd2lem  45991  infnsuprnmpt  45993  rnmptbdlem  45998  xralrple2  46098  infxrunb2  46111  xralrple4  46116  xralrple3  46117  xrralrecnnle  46126  xrralrecnnge  46133  reclt0  46134  supxrunb3  46142  supxrleubrnmpt  46148  xrre4  46153  unb2ltle  46157  rexabslelem  46160  suprleubrnmpt  46164  infxrunb3rnmpt  46170  uzub  46173  supminfrnmpt  46187  iccintsng  46267  sqrlearg  46297  uzinico  46303  preimaiocmnf  46304  limcresiooub  46384  limclr  46397  climeldmeq  46407  limsuppnflem  46452  limsupmnflem  46462  limsupmnfuzlem  46468  limsupre3lem  46474  limsupre3uzlem  46477  liminfreuzlem  46544  dvnmul  46685  dvmptfprodlem  46686  ismbl3  46728  ismbl4  46735  fourierdlem50  46898  fourierdlem89  46937  fourierdlem91  46939  dfsalgen2  47083  sge0repnf  47128  sge0lefi  47140  sge0resplit  47148  sge0fodjrnlem  47158  voliunsge0lem  47214  hspdifhsp  47358  isvonmbl  47380  ovnovollem3  47400  vonvolmbl  47403  pimrecltpos  47450  preimaicomnf  47453  pimrecltneg  47466  issmflem  47469  issmfle  47487  issmfgt  47498  smfaddlem1  47505  issmfge  47512  smfresal  47530  smflimmpt  47552  smfinflem  47559  smflimsuplem7  47568  smflimsupmpt  47571  sigarcol  47606  confun  47704  or2expropbi  47799  fsetsniunop  47814  fcoresf1b  47835  f1cof1b  47842  funfocofob  47843  rexsb  47864  euoreqb  47874  ralbinrald  47887  rlimdmafv  47942  fafv2elrnb  48000  tz6.12c-afv2  48007  dfatbrafv2b  48010  fnbrafv2b  48013  rlimdmafv2  48023  f1oresf1o2  48056  el1fzopredsuc  48091  2ffzoeq  48093  nnmul2b  48096  modlt0b  48134  nndivides2  48149  imasetpreimafvbijlemfo  48182  iccpartiun  48211  ichnfb  48242  ich2exprop  48248  sprsymrelfolem2  48270  paireqne  48288  prprelprb  48294  reupr  48299  nprmmul2  48305  nprmmul3  48306  requad01  48414  requad1  48415  requad2  48416  dfodd6  48430  dfeven4  48431  evensumeven  48500  sbgoldbalt  48574  clnbgrel  48621  dfclnbgr6  48649  dfnbgr6  48650  isubgredg  48659  isuspgrim0  48687  isuspgrim  48689  gricushgr  48710  uhgrimisgrgriclem  48723  clnbgrgrim  48727  grimedg  48728  usgrgrtrirex  48743  uspgrlimlem2  48782  uspgrlim  48785  gpgedgiov  48858  gpgedg2ov  48859  gpgedg2iv  48860  gpgnbgrvtx0  48867  gpgnbgrvtx1  48868  isassintop  49003  uzlidlring  49028  rngcisoALTV  49070  ringcisoALTV  49104  isidom3  49138  domnmsuppn0  49177  lindslininds  49272  snlindsntor  49279  isldepslvec2  49293  affinecomb1  49510  prelrrx2b  49522  rrx2plord2  49530  eenglngeehlnm  49547  rrx2vlinest  49549  line2xlem  49561  line2x  49562  line2y  49563  itsclc0xyqsolb  49578  itsclquadb  49584  mpbiran3d  49603  opnneieqv  49717  iscnrm3lem2  49741  fullthinc2  50257  thincciso  50259  alsralrex  50618  alsraln0  50619