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  654  impbida  813  dedlem0b  1060  dedlema  1061  dedlemb  1062  albi  1851  alexbii  1866  equequ1  2060  equequ2  2061  spsbbi  2112  elequ1  2154  elequ2  2162  sbequ12  2290  sbft  2307  cbv2w  2370  exsb  2391  dral1v  2401  cbv2  2435  cbv2h  2438  ax12b  2456  dral1  2471  dral1ALT  2472  eupickb  2663  eupickbi  2664  2eu2  2680  ralbi  3121  rexbi  3122  ralbida  3277  ceqsalt  3487  rspcebdv  3574  rspceb2dv  3584  ceqex  3609  elabgtOLD  3630  mob2  3676  reu6  3687  sbcg  3814  2reu2  3850  csbiebt  3880  dfss2  4097  reupick  4277  reupick2  4279  uneqdifeq  4451  prnebg  4814  preqsnd  4817  prel12g  4822  iuneqconst  4966  disjeq2  5077  disjeq1  5080  disjss3  5105  reusv2lem2  5365  reusv2lem3  5366  alxfr  5373  ralxfrd  5374  ralxfrd2  5378  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  cotsexgw  5467  snopeqop  5482  euotd  5490  poeq2  5567  sotric  5593  sotrieq  5594  freq2  5623  seeq1  5625  seeq2  5626  iss  6038  tz7.7  6403  ordtri1  6411  ordelinel  6481  funeq  6576  funssres  6601  f0dom0  6785  fnbrfvb  6955  ssimaex  6990  fsneq  7054  fvimacnv  7072  elpreimaOLD  7078  feldmfvelcdm  7107  eldmrexrnb  7113  fsn  7157  fnsnbg  7190  fmptsng  7193  fmptsnd  7194  fprb  7219  tpres  7227  fconst2g  7229  fconst5  7232  elunirn  7275  f1ocnvfvb  7307  f1prex  7312  foeqcnvco  7328  f1eqcocnv  7329  fliftfun  7340  soisores  7355  isofr  7370  isose  7371  isopo  7374  isoso  7376  f1oiso2  7380  eusvobj2  7432  oprabidw  7471  oprabid  7472  f1opw2  7697  oneqmin  7835  ordelsuc  7852  ordsucelsuc  7854  ordunisuc2  7876  limsuc  7881  fndmexb  7939  resf1ext2b  7968  f1ovv  7991  mptcnfimad  8019  op1steq  8066  opreuopreu  8067  funeldmdif  8081  fvn0elsuppb  8223  extmptsuppeq  8230  rntpos  8281  smoiso2  8402  seqomlem2  8486  oaord  8580  oawordex  8590  oaordex  8591  omord2  8600  om00  8608  oeord  8622  nnaord  8653  nnmord  8666  nnawordex  8671  nnaordex  8672  nnaordex2  8673  eldifsucnn  8698  erexb  8768  swoord1  8775  swoord2  8776  ecelqsdmb  8832  iiner  8835  eceqoveq  8868  mapsnd  8939  ralxpmap  8949  omxpenlem  9122  domtriord  9167  mapxpen  9187  mapunen  9190  ssenen  9195  enfi  9227  nneneq  9246  nndomog  9253  onomeneq  9254  en1eqsnbi  9292  fodomfib  9345  f1opwfi  9370  fsuppunbi  9405  elfiun  9446  suplub2  9477  ordiso2  9533  ordiso  9534  oieu  9557  brwdom2  9591  brwdom3  9600  cantnflem1  9714  ttrclselem2  9751  elhf2  9934  cardidm  10064  carddom2  10082  pm54.43  10106  acnen  10156  acnen2  10158  alephord  10178  alephinit  10198  dfac5  10231  infdif2  10311  fictb  10346  coflim  10363  fincssdom  10425  fin23lem25  10426  isf32lem9  10463  isf34lem4  10479  fin1a2lem11  10512  axdc3lem2  10553  ficard  10673  fpwwe2lem11  10750  fpwwe2  10752  indpi  11016  nqereq  11044  1idpr  11138  ltapr  11154  leltne  11423  ltlen  11435  ltadd2  11438  addlsub  11756  addid0  11759  ltord1  11866  mul0or  11980  ldiv  12175  ltmul1  12191  mulge0b  12211  lt2msq  12226  nnsub  12406  nn0sub  12680  zrevaddcl  12765  zltp1le  12770  zdiv  12793  nneo  12807  zeo2  12810  zmax  13096  zbtwnre  13097  qrevaddcl  13123  xrlttri  13292  xrleltne  13298  xralrple  13359  xltneg  13371  xleadd1  13409  xlemul1  13444  supxrunb1  13473  supxrunb2  13474  ioo0  13525  iccid  13545  ico0  13546  ioc0  13547  icc0  13548  difreicc  13639  iccsplit  13640  zltaddlt1le  13660  0fz1  13701  uzsplit  13754  fzm1  13765  fzrevral  13770  ssfzo12bi  13920  elfznelfzob  13933  flge  13969  modid2  14062  modmuladd  14080  ssnn0fi  14152  seqf1olem1  14208  hashen  14515  hashdom  14547  hash2exprb  14640  pr2pwpr  14648  hashtpg  14654  hash3tpexb  14663  len0nnbi  14720  ccats1pfxeqbi  14916  reuccatpfxs1  14921  repsdf2  14954  scshwfzeqfzo  15002  relexpindlem  15242  shftlem  15247  shftuz  15248  abslt  15508  absle  15509  rexico  15547  cau3lem  15548  reusq0  15658  rlim2lt  15690  rlim3  15691  o1lo1  15730  rlimdm  15744  climshft  15769  o1dif  15823  isercolllem2  15859  isercoll  15861  zsum  15910  fsum  15912  fsum00  15991  incexclem  16031  zprod  16130  fprod  16134  dvdsval2  16451  moddvds  16459  negdvdsb  16468  dvdsnegb  16469  dvdscmulr  16480  dvdsmulcr  16481  dvdssub2  16497  dvdsaddre2b  16503  fzo0dvdseq  16519  mod2eq1n2dvds  16543  ltoddhalfle  16557  sumodd  16584  bitsf1ocnv  16640  sadcaddlem  16653  bitsuz  16670  dvdsgcdb  16744  gcdzeq  16751  dvdsexpnn  16766  lcmeq0  16801  lcmdvdsb  16814  lcmfeq0b  16831  lcmf  16834  lcmfdvdsb  16844  coprmgcdb  16850  cncongr  16870  isprm2lem  16882  dvdsprime  16888  dvdsprm  16905  isprm7  16910  coprm  16913  euclemma  16915  rpexp  16924  prmdvdsncoprmbd  16929  prmdiveq  16989  hashgcdlem  16991  odzdvds  16999  pythagtrip  17038  pc2dvds  17083  pcprmpw2  17086  pcprmpw  17087  vdwapun  17178  ramtcl2  17215  firest  17629  mrieqv2d  17839  isacs2  17853  isssc  18021  setciso  18292  posasymb  18519  pleval2  18535  pltval3  18537  lublecllem  18558  joinle  18584  meetle  18598  latdisd  18697  lubun  18715  clatleglb  18718  letsr  18793  intopsn  18858  gsumval2a  18900  frmdss2  19085  isgrpid2  19213  isgrpinv  19230  f1ghm0to0  19485  symg1bas  19632  oddvdsnn0  19785  oddvds  19788  odeq  19791  odeq1  19801  gexdvds  19825  pgpfi  19846  pgpssslw  19855  fislw  19866  sylow3lem2  19869  lsmelvalm  19892  lsmlub  19905  lsmss1b  19907  lsmss2b  19909  efgs1b  19977  cyggenod  20125  cyggexb  20140  dprdfeq0  20265  ablsimpgfind  20353  ringinvnz1ne0  20558  ringinvnzdiv  20559  unitmulclb  20638  dvreq1  20668  isnzr2  20795  0ringnnzr  20803  0ring01eqbi2  20810  0ring01eqbi  20811  rngciso  20917  ringciso  20951  rrgeq0  20979  domneq0  20987  isabvd  21096  issrngd  21139  lssats2  21302  lspsneq0  21314  lsmelval2  21387  lvecvs0or  21413  lspsneq  21427  lspsneu  21428  lidl1el  21532  rspprop  21551  lidldvgen  21685  pzriprnglem10  21823  pzriprnglem11  21824  znunit  21896  psgndif  21935  ipeq0  21971  ocvsscon  22008  pjdm2  22044  obselocv  22061  islinds4  22168  psdmul  22514  ply1coe1eq  22645  cply1coe0bi  22647  mat1dimelbas  22813  matunitlindf  23023  cramer  23036  toponcomb  23274  tgss3  23331  clsval2  23395  isopn3  23411  elcls3  23428  opncldf1  23429  neiint  23449  neips  23458  opnneissb  23459  opnssneib  23460  opnnei  23465  tpnei  23466  opnneiid  23471  restcld  23517  restopnb  23520  tgcn  23597  tgcnp  23598  subbascn  23599  iscnp4  23608  cnpnei  23609  cncls2  23618  cncls  23619  cnntr  23620  lmss  23643  hausnei2  23698  lpcls  23709  ordtt1  23724  cmpsub  23745  tgcmp  23746  1stcelcls  23807  locfincmp  23872  kgencn2  23903  ptpjpre1  23917  upxp  23969  txcn  23972  txlm  23994  tgqtop  24058  kqfvima  24076  isr0  24083  regr1lem2  24086  hmeoopn  24112  hmeocld  24113  ptuncnv  24153  fbunfip  24215  fgss2  24220  ufilb  24252  ufprim  24255  trufil  24256  cfinufil  24274  ufildr  24277  elfm2  24294  elfm3  24296  rnelfm  24299  fmfnfmlem4  24303  fmco  24307  flimtopon  24316  flimopn  24321  fbflim2  24323  flimrest  24329  flffbas  24341  cnpflf  24347  fclstopon  24358  fclsnei  24365  fclsbas  24367  fclsfnflim  24373  fclscmp  24376  ufilcmp  24378  isfcf  24380  fcfnei  24381  cnpfcf  24387  alexsubb  24392  alexsubALT  24397  cldsubg  24457  tgphaus  24463  tgpt0  24465  tsmsgsum  24485  tsmsres  24490  xbln0  24760  blssexps  24772  blssex  24773  isxms2  24794  prdsbl  24837  neibl  24847  metss  24854  met2ndc  24869  metrest  24870  metcnp3  24886  tngngp3  25002  nmoeq0  25082  xrsxmet  25156  reconn  25175  iccpnfcnv  25292  fgcfil  25619  iscau4  25627  cfilres  25644  iunmbl2  25905  ismbf3d  26002  mbfaddlem  26008  i1faddlem  26041  i1fmullem  26042  ellimc3  26226  dvfsumlem2  26374  tdeglem4  26405  deg1nn0clb  26435  deg1lt0  26436  dvdsq1p  26508  plypf1  26558  0dgrb  26592  plymul0or  26626  taylthlem2  26728  ulmshft  26744  ulmcaulem  26748  ulmcau  26749  cosord  26886  eff1olem  26903  lognegb  26945  eflogeq  26957  logdivlt  26976  efopn  27013  cxpeq0  27033  cxpeq  27112  angpieqvd  27186  dcubic  27201  asinsinb  27252  acoscosb  27253  atantanb  27279  rlimcnp  27320  isppw  27468  isppw2  27469  vmappw  27470  isnsqf  27489  ppieq0  27530  fsumdvdsdiag  27538  dvdsppwf1o  27540  fsumfldivdiag  27544  chpeq0  27562  chteq0  27563  dchrptlem1  27618  lgsdir2lem4  27682  lgsne0  27689  lgsqr  27705  lgsdchrval  27708  gausslemma2dlem1a  27719  lgsquadlem1  27734  m1lgs  27742  2sqreultblem  27802  2sqreunnltblem  27805  nodenselem8  28075  ltlesnd  28159  oldlim  28300  ltslpss  28321  leadds1  28402  ltnegs  28458  negleft  28471  negright  28472  muls0ord  28598  abslts  28662  onlts  28680  n0subs  28776  n0ltsp1le  28778  z12sge0  28896  iscgrglt  29004  brbtwn  29504  brcgr  29505  brbtwn2  29510  axcontlem7  29575  uhgr0vb  29677  edglnl  29748  ausgrusgrb  29773  ushgredgedg  29837  ushgredgedgloop  29839  usgr0vb  29845  usgr1v  29864  nbupgr  29952  nbumgrvtx  29954  nbuhgr2vtx1edgb  29960  edgusgrnbfin  29981  nb3grprlem1  29988  uvtxnbvtxm1  30014  cusgrfilem2  30064  uhgr0edg0rgrb  30182  cusgrm1rusgr  30190  spthonepeq  30365  usgr2pth  30377  wlkiswwlks  30492  wlkiswwlkupgr  30494  wlklnwwlkn  30500  wlklnwwlknupgr  30502  wwlksnextbi  30510  wwlksnredwwlkn0  30512  wwlksnextwrd  30513  wwlksnextprop  30528  usgrwwlks2on  30574  umgrwwlks2on  30575  elwspths2on  30578  elwspths2onw  30579  usgr2wspthons3  30583  elwwlks2  30585  elwspths2spth  30586  clwlkclwwlklem3  30619  loopclwwlkn1b  30660  clwwlknon1sn  30718  clwwlknonwwlknonb  30724  loop1cycl  30771  umgr3v3e3cycl  30812  eupth2lem3lem4  30859  frgr0v  30890  frgr3vlem2  30902  2clwwlk2clwwlk  30978  wlkl0  30995  grpoinvf  31161  nvmul0or  31279  nvz  31298  diporthcom  31345  ubthlem3  31501  hvmul0or  31654  his6  31728  hial0  31731  hial02  31732  orthcom  31737  normgt0  31756  ocin  31925  occon3  31926  shsel3  31944  shlub  32043  chssoc  32125  h1de2bi  32183  spansncol  32197  elspansn4  32202  spansnss2  32204  sumspansn  32278  lnopcnbd  32665  lnfncnbd  32686  riesz1  32694  elpjrn  32819  cvcon3  32913  dmdmd  32929  dmdbr3  32934  dmdbr4  32935  dmdbr5  32937  mdslmd1i  32958  atcveq0  32977  chcv1  32984  atssma  33007  atcv0eq  33008  atcv1  33009  disjeq1f  33236  br8d  33271  fpwrelmap  33392  xaddeq0  33412  eliccelico  33436  elicoelioo  33437  indf1ofs  33500  isarchiofld  33827  unitdivcld  34600  xrge0iifcnv  34632  lmxrge0  34651  eulerpartlemgh  35077  dstfrvunirn  35174  reu6f  35776  fnfvintima  35783  fnrelpredd  35801  rankfilimb  35809  erscottd  35842  fineqvnttrclse  35891  cusgracyclt3v  36077  srepdflem1  36084  cvmliftmolem2  36213  cvmlift2lem12  36245  satfvsucsuc  36296  satfdm  36300  fmlasuc  36317  satffunlem1lem2  36334  satffunlem2lem2  36337  mthmb  36512  climuzcnv  36602  br8  36698  br6  36699  br4  36700  funbreq  36711  axextbdist  36739  dfrdg4  36892  cgrcom  36932  cgrcoml  36938  cgrdegen  36946  btwncom  36956  brsegle  37050  brsegle2  37051  colinbtwnle  37060  btwnoutside  37067  broutsideof3  37068  outsidele  37074  lineunray  37089  lineelsb2  37090  ltnmul  37142  ltnadd  37144  elicc3  37282  nn0prpwlem  37287  opnbnd  37290  cldbnd  37291  opnregcld  37295  cldregopn  37296  fnessref  37322  refssfne  37323  neibastop2  37326  fnemeet2  37332  fnejoin2  37334  fgmin  37335  ontgval  37396  ordtop  37401  ordcmp  37412  nndivsub  37422  bj-cbval  37722  bj-cbvex  37723  bj-19.21t  37840  bj-19.23t  37841  bj-19.42t  37844  bj-sbft  37857  bj-nnf-cbval  37859  bj-cbv2hv  37886  bj-equsal1t  37911  bj-19.21t0  37919  bj-ceqsalt0  37973  bj-ceqsalt1  37974  bj-xpnzexb  38051  bj-axreprepsep  38181  cgsex2gd  38249  bj-idreseq  38274  bj-imdiridlem  38297  bj-finsumval0  38397  bj-fvimacnv0  38398  bj-isrvec2  38412  bj-bary1  38424  dfgcd3  38436  isbasisrelowllem1  38469  isbasisrelowllem2  38470  finxpsuclem  38511  wl-lem-exsb  38689  wl-mo3t  38699  poimirlem6  38735  poimirlem7  38736  poimirlem16  38745  poimirlem19  38748  poimirlem22  38751  poimirlem23  38752  poimirlem24  38753  cnambfre  38777  itg2addnc  38783  brabg2  38842  istotbnd3  38896  sstotbnd2  38899  sstotbnd  38900  sstotbnd3  38901  ssbnd  38913  ismtybnd  38932  reheibor  38964  grpoeqdivid  39006  grpokerinj  39018  rngosn3  39049  rngoueqz  39065  1idl  39151  0rngo  39152  divrngidl  39153  igenval2  39191  ispridlc  39195  isdmn3  39199  relcnveq3  39450  iss2  39467  elrelscnveq3  39750  funALTVeq  39908  disjeq  39957  prtlem10  40113  prter2  40129  dral1-o  40152  lshpinN  40237  lsatcveq0  40280  lsatcv0eq  40295  lsatcv1  40296  islshpcv  40301  lkr0f  40342  lkrshp4  40356  lshpkrlem1  40358  lshpset2N  40367  lfl1dim  40369  lfl1dim2N  40370  lub0N  40437  glb0N  40441  oplecon3b  40448  cmtcomN  40497  cmtbr3N  40502  cmtbr4N  40503  cvrnbtwn2  40523  cvrnbtwn3  40524  cvrcon3b  40525  cvrnbtwn4  40527  cvrcmp  40531  atcvreq0  40562  atnle  40565  atlatle  40568  cvlexchb1  40578  cvlcvr1  40587  hlrelat2  40651  exatleN  40652  cvrval3  40661  cvrval4N  40662  cvrexch  40668  atcvr0eq  40674  lnnat  40675  atcvrj0  40676  atcvrj2b  40680  atltcvr  40683  atbtwn  40694  ps-1  40725  3at  40738  islln2a  40765  llncmp  40770  islpln2a  40796  lplncmp  40810  islvol2aN  40840  4at  40861  lvolcmp  40865  pmaple  41009  lncmp  41031  paddss  41093  llnexchb2lem  41116  2polcon4bN  41166  ispsubcl2N  41195  lhpat3  41294  lautcvr  41340  ltrnid  41383  trlval2  41411  trlatn0  41420  ltrnideq  41423  trlnidatb  41425  cdlemeg49lebilem  41787  trlord  41817  cdlemg1a  41818  cdlemg1cex  41836  tendoid0  42073  dva1dim  42233  cdlemm10N  42366  diarnN  42377  cdlemn  42460  dihlspsnssN  42580  dihatexv  42586  dochkrshp  42634  dochkrshp4  42637  djhlsmcl  42662  lcfl6  42748  lcfl8  42750  lcfrvalsnN  42789  lcfrlem9  42798  mapdval2N  42878  mapdordlem2  42885  mapd1o  42896  mapd0  42913  mapdheq2biN  42978  nnproddivdvdsd  43241  primrootspoweq0  43347  aks6d1c1p1  43348  aks6d1c5lem1  43377  sticksstones11  43397  sticksstones22  43409  grpods  43435  unitscyglem2  43437  eqresfnbd  43477  expeq1d  43572  expeqidd  43573  zdivgd  43579  sn-remul0ord  43650  mulgt0b1d  43727  frlmfzowrdb  43762  frlmsnic  43795  evlselvlem  43807  prjspreln0  43828  elrfi  43896  diophrw  43961  eldioph2b  43965  diophin  43974  rexrabdioph  43992  rmxycomplete  44115  coprmdvdsb  44183  jm2.19  44191  jm2.26  44200  jm2.27  44206  limsuc2  44239  dgraa0p  44341  rngunsnply  44361  fiuneneq  44384  unielss  44410  oaabsb  44486  nnoeomeqom  44504  cantnfresb  44516  tfsconcatrn  44534  tfsconcat0b  44538  tfsconcatrev  44540  oadif1lem  44571  oadif1  44572  fzunt  44646  fzuntd  44647  fzunt1d  44648  fzuntgd  44649  pwelg  44751  nzss  45491  dvconstbi  45508  expgrowth  45509  bcc0  45514  axc11next  45580  pm14.24  45605  sbiota1  45607  sbcim2g  45710  sineq0ALT  46108  mapss2  46422  fsneqrn  46427  mapssbi  46429  rnmptbd2lem  46463  infnsuprnmpt  46465  rnmptbdlem  46470  xralrple2  46569  infxrunb2  46582  xralrple4  46587  xralrple3  46588  xrralrecnnle  46597  xrralrecnnge  46604  reclt0  46605  supxrunb3  46613  supxrleubrnmpt  46619  xrre4  46624  unb2ltle  46628  rexabslelem  46631  suprleubrnmpt  46635  infxrunb3rnmpt  46641  uzub  46644  supminfrnmpt  46658  iccintsng  46738  sqrlearg  46768  uzinico  46774  preimaiocmnf  46775  limcresiooub  46855  limclr  46868  climeldmeq  46878  limsuppnflem  46923  limsupmnflem  46933  limsupmnfuzlem  46939  limsupre3lem  46945  limsupre3uzlem  46948  liminfreuzlem  47015  dvnmul  47156  dvmptfprodlem  47157  ismbl3  47199  ismbl4  47206  fourierdlem50  47369  fourierdlem89  47408  fourierdlem91  47410  dfsalgen2  47554  sge0repnf  47599  sge0lefi  47611  sge0resplit  47619  sge0fodjrnlem  47629  voliunsge0lem  47685  hspdifhsp  47829  isvonmbl  47851  ovnovollem3  47871  vonvolmbl  47874  pimrecltpos  47921  preimaicomnf  47924  pimrecltneg  47937  issmflem  47940  issmfle  47958  issmfgt  47969  smfaddlem1  47976  issmfge  47983  smfresal  48001  smflimmpt  48023  smfinflem  48030  smflimsuplem7  48039  smflimsupmpt  48042  sigarcol  48077  tmachlem-agreeprod  48150  confun  48212  or2expropbi  48307  fsetsniunop  48322  fcoresf1b  48343  f1cof1b  48350  funfocofob  48351  rexsb  48373  euoreqb  48383  ralbinrald  48396  rlimdmafv  48450  fafv2elrnb  48508  tz6.12c-afv2  48515  dfatbrafv2b  48518  fnbrafv2b  48521  rlimdmafv2  48531  f1oresf1o2  48564  el1fzopredsuc  48599  2ffzoeq  48601  nnmul2b  48604  modlt0b  48642  nndivides2  48657  imasetpreimafvbijlemfo  48690  iccpartiun  48719  ichnfb  48750  ich2exprop  48756  sprsymrelfolem2  48778  paireqne  48796  prprelprb  48802  reupr  48807  nprmmul2  48813  nprmmul3  48814  requad01  48922  requad1  48923  requad2  48924  dfodd6  48938  dfeven4  48939  evensumeven  49008  sbgoldbalt  49082  clnbgrel  49129  dfclnbgr6  49157  dfnbgr6  49158  isubgredg  49167  isuspgrim0  49195  isuspgrim  49197  gricushgr  49218  uhgrimisgrgriclem  49231  clnbgrgrim  49235  grimedg  49236  usgrgrtrirex  49251  uspgrlimlem2  49290  uspgrlim  49293  gpgedgiov  49366  gpgedg2ov  49367  gpgedg2iv  49368  gpgnbgrvtx0  49375  gpgnbgrvtx1  49376  isassintop  49510  uzlidlring  49535  rngcisoALTV  49577  ringcisoALTV  49611  isidom3  49645  domnmsuppn0  49684  lindslininds  49779  snlindsntor  49786  isldepslvec2  49800  affinecomb1  50017  rrx2plord2  50038  line2xlem  50068  line2x  50069  line2y  50070  itsclc0xyqsolb  50085  itsclquadb  50091  mpbiran3d  50110  opnneibid  50228  iscnrm3lem2  50252  fullthinc2  50789  thincciso  50791  alsralrex  51186  alsraln0  51187