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  1850  alexbii  1865  equequ1  2057  equequ2  2058  spsbbi  2109  elequ1  2151  elequ2  2159  sbequ12  2286  sbft  2303  cbv2w  2366  exsb  2388  dral1v  2398  cbv2  2432  cbv2h  2435  ax12b  2453  dral1  2468  dral1ALT  2469  eupickb  2660  eupickbi  2661  2eu2  2677  ralbi  3117  rexbi  3118  ralbida  3273  ceqsalt  3483  rspcebdv  3570  rspceb2dv  3580  ceqex  3605  elabgtOLD  3626  mob2  3672  reu6  3683  sbcg  3810  2reu2  3845  csbiebt  3875  dfss2  4094  reupick  4274  reupick2  4276  uneqdifeq  4447  prnebg  4815  preqsnd  4818  prel12g  4823  iuneqconst  4962  disjeq2  5073  disjeq1  5076  disjss3  5101  reusv2lem2  5360  reusv2lem3  5361  alxfr  5368  ralxfrd  5369  ralxfrd2  5373  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  snopeqop  5477  euotd  5485  poeq2  5562  sotric  5588  sotrieq  5589  freq2  5618  seeq1  5620  seeq2  5621  iss  6026  tz7.7  6388  ordtri1  6396  ordelinel  6466  funeq  6559  funssres  6584  f0dom0  6766  fnbrfvb  6935  ssimaex  6970  fsneq  7034  fvimacnv  7052  elpreima  7057  feldmfvelcdm  7086  eldmrexrnb  7092  fsn  7136  fnsnbg  7169  fnsnbOLD  7171  fmptsng  7173  fmptsnd  7174  fprb  7199  tpres  7207  fconst2g  7209  fconst5  7212  elunirn  7255  f1ocnvfvb  7287  f1prex  7292  foeqcnvco  7308  f1eqcocnv  7309  fliftfun  7320  soisores  7335  isofr  7350  isose  7351  isopo  7354  isoso  7356  f1oiso2  7360  eusvobj2  7412  oprabidw  7451  oprabid  7452  f1opw2  7676  oneqmin  7814  ordelsuc  7831  ordsucelsuc  7833  ordunisuc2  7855  limsuc  7860  fndmexb  7918  resf1ext2b  7947  f1ovv  7970  mptcnfimad  7998  op1steq  8045  opreuopreu  8046  funeldmdif  8059  fvn0elsuppb  8198  extmptsuppeq  8205  rntpos  8256  smoiso2  8377  seqomlem2  8461  oaord  8555  oawordex  8565  oaordex  8566  omord2  8575  om00  8583  oeord  8597  nnaord  8628  nnmord  8641  nnawordex  8646  nnaordex  8647  nnaordex2  8648  eldifsucnn  8673  erexb  8743  swoord1  8750  swoord2  8751  ecelqsdmb  8807  iiner  8810  eceqoveq  8843  mapsnd  8914  ralxpmap  8924  omxpenlem  9097  domtriord  9142  mapxpen  9162  mapunen  9165  ssenen  9170  enfi  9202  nneneq  9221  nndomog  9228  onomeneq  9229  en1eqsnbi  9267  fodomfib  9320  f1opwfi  9345  fsuppunbi  9381  elfiun  9422  suplub2  9453  ordiso2  9509  ordiso  9510  oieu  9533  brwdom2  9567  brwdom3  9576  cantnflem1  9690  ttrclselem2  9727  elhf2  9910  cardidm  10040  carddom2  10058  pm54.43  10082  acnen  10132  acnen2  10134  alephord  10154  alephinit  10174  dfac5  10207  infdif2  10287  fictb  10322  coflim  10339  fincssdom  10401  fin23lem25  10402  isf32lem9  10439  isf34lem4  10455  fin1a2lem11  10488  axdc3lem2  10529  ficard  10649  fpwwe2lem11  10726  fpwwe2  10728  indpi  10992  nqereq  11020  1idpr  11114  ltapr  11130  leltne  11399  ltlen  11411  ltadd2  11414  addlsub  11732  addid0  11735  ltord1  11842  mul0or  11956  ldiv  12151  ltmul1  12167  mulge0b  12187  lt2msq  12202  nnsub  12382  nn0sub  12656  zrevaddcl  12741  zltp1le  12746  zdiv  12769  nneo  12783  zeo2  12786  zmax  13072  zbtwnre  13073  qrevaddcl  13099  xrlttri  13268  xrleltne  13274  xralrple  13335  xltneg  13347  xleadd1  13385  xlemul1  13420  supxrunb1  13449  supxrunb2  13450  ioo0  13501  iccid  13521  ico0  13522  ioc0  13523  icc0  13524  difreicc  13615  iccsplit  13616  zltaddlt1le  13636  0fz1  13677  uzsplit  13730  fzm1  13741  fzrevral  13746  ssfzo12bi  13896  elfznelfzob  13909  flge  13945  modid2  14038  modmuladd  14056  ssnn0fi  14128  seqf1olem1  14184  hashen  14491  hashdom  14523  hash2exprb  14616  pr2pwpr  14624  hashtpg  14630  hash3tpexb  14639  len0nnbi  14696  ccats1pfxeqbi  14891  reuccatpfxs1  14896  repsdf2  14929  scshwfzeqfzo  14977  relexpindlem  15216  shftlem  15221  shftuz  15222  abslt  15482  absle  15483  rexico  15521  cau3lem  15522  reusq0  15632  rlim2lt  15664  rlim3  15665  o1lo1  15704  rlimdm  15718  climshft  15743  o1dif  15797  isercolllem2  15833  isercoll  15835  zsum  15884  fsum  15886  fsum00  15965  incexclem  16005  zprod  16104  fprod  16108  dvdsval2  16425  moddvds  16433  negdvdsb  16442  dvdsnegb  16443  dvdscmulr  16454  dvdsmulcr  16455  dvdssub2  16471  dvdsaddre2b  16477  fzo0dvdseq  16493  mod2eq1n2dvds  16517  ltoddhalfle  16531  sumodd  16558  bitsf1ocnv  16614  sadcaddlem  16627  bitsuz  16644  dvdsgcdb  16718  gcdzeq  16725  dvdsexpnn  16740  lcmeq0  16775  lcmdvdsb  16788  lcmfeq0b  16805  lcmf  16808  lcmfdvdsb  16818  coprmgcdb  16824  cncongr  16844  isprm2lem  16856  dvdsprime  16862  dvdsprm  16879  isprm7  16884  coprm  16887  euclemma  16889  rpexp  16898  prmdvdsncoprmbd  16903  prmdiveq  16963  hashgcdlem  16965  odzdvds  16973  pythagtrip  17012  pc2dvds  17057  pcprmpw2  17060  pcprmpw  17061  vdwapun  17152  ramtcl2  17189  firest  17603  mrieqv2d  17813  isacs2  17827  isssc  17995  setciso  18266  posasymb  18493  pleval2  18509  pltval3  18511  lublecllem  18532  joinle  18558  meetle  18572  latdisd  18671  lubun  18689  clatleglb  18692  letsr  18767  intopsn  18832  gsumval2a  18874  frmdss2  19059  isgrpid2  19187  isgrpinv  19204  f1ghm0to0  19459  symg1bas  19605  oddvdsnn0  19758  oddvds  19761  odeq  19764  odeq1  19774  gexdvds  19798  pgpfi  19819  pgpssslw  19828  fislw  19839  sylow3lem2  19842  lsmelvalm  19865  lsmlub  19878  lsmss1b  19880  lsmss2b  19882  efgs1b  19950  cyggenod  20098  cyggexb  20113  dprdfeq0  20238  ablsimpgfind  20326  ringinvnz1ne0  20531  ringinvnzdiv  20532  unitmulclb  20611  dvreq1  20641  isnzr2  20768  0ringnnzr  20776  0ring01eqbi2  20783  0ring01eqbi  20784  rngciso  20890  ringciso  20924  rrgeq0  20952  domneq0  20960  isabvd  21069  issrngd  21112  lssats2  21275  lspsneq0  21287  lsmelval2  21360  lvecvs0or  21386  lspsneq  21400  lspsneu  21401  lidl1el  21505  rspprop  21524  lidldvgen  21658  pzriprnglem10  21796  pzriprnglem11  21797  znunit  21869  psgndif  21908  ipeq0  21944  ocvsscon  21981  pjdm2  22017  obselocv  22034  islinds4  22141  psdmul  22487  ply1coe1eq  22618  cply1coe0bi  22620  mat1dimelbas  22786  matunitlindf  22996  cramer  23009  toponcomb  23247  tgss3  23304  clsval2  23368  isopn3  23384  elcls3  23401  opncldf1  23402  neiint  23422  neips  23431  opnneissb  23432  opnssneib  23433  opnnei  23438  tpnei  23439  opnneiid  23444  restcld  23490  restopnb  23493  tgcn  23570  tgcnp  23571  subbascn  23572  iscnp4  23581  cnpnei  23582  cncls2  23591  cncls  23592  cnntr  23593  lmss  23616  hausnei2  23671  lpcls  23682  ordtt1  23697  cmpsub  23718  tgcmp  23719  1stcelcls  23780  locfincmp  23845  kgencn2  23876  ptpjpre1  23890  upxp  23942  txcn  23945  txlm  23967  tgqtop  24031  kqfvima  24049  isr0  24056  regr1lem2  24059  hmeoopn  24085  hmeocld  24086  ptuncnv  24126  fbunfip  24188  fgss2  24193  ufilb  24225  ufprim  24228  trufil  24229  cfinufil  24247  ufildr  24250  elfm2  24267  elfm3  24269  rnelfm  24272  fmfnfmlem4  24276  fmco  24280  flimtopon  24289  flimopn  24294  fbflim2  24296  flimrest  24302  flffbas  24314  cnpflf  24320  fclstopon  24331  fclsnei  24338  fclsbas  24340  fclsfnflim  24346  fclscmp  24349  ufilcmp  24351  isfcf  24353  fcfnei  24354  cnpfcf  24360  alexsubb  24365  alexsubALT  24370  cldsubg  24430  tgphaus  24436  tgpt0  24438  tsmsgsum  24458  tsmsres  24463  xbln0  24733  blssexps  24745  blssex  24746  isxms2  24767  prdsbl  24810  neibl  24820  metss  24827  met2ndc  24842  metrest  24843  metcnp3  24859  tngngp3  24975  nmoeq0  25055  xrsxmet  25129  reconn  25148  iccpnfcnv  25265  fgcfil  25592  iscau4  25600  cfilres  25617  iunmbl2  25878  ismbf3d  25975  mbfaddlem  25981  i1faddlem  26014  i1fmullem  26015  ellimc3  26199  dvfsumlem2  26347  tdeglem4  26378  deg1nn0clb  26408  deg1lt0  26409  dvdsq1p  26481  plypf1  26531  0dgrb  26565  plymul0or  26599  taylthlem2  26701  ulmshft  26717  ulmcaulem  26721  ulmcau  26722  cosord  26859  eff1olem  26876  lognegb  26918  eflogeq  26930  logdivlt  26949  efopn  26986  cxpeq0  27006  cxpeq  27085  angpieqvd  27159  dcubic  27174  asinsinb  27225  acoscosb  27226  atantanb  27252  rlimcnp  27293  isppw  27441  isppw2  27442  vmappw  27443  isnsqf  27462  ppieq0  27503  fsumdvdsdiag  27511  dvdsppwf1o  27513  fsumfldivdiag  27517  chpeq0  27535  chteq0  27536  dchrptlem1  27591  lgsdir2lem4  27655  lgsne0  27662  lgsqr  27678  lgsdchrval  27681  gausslemma2dlem1a  27692  lgsquadlem1  27707  m1lgs  27715  2sqreultblem  27775  2sqreunnltblem  27778  nodenselem8  28048  ltlesnd  28132  oldlim  28273  ltslpss  28294  leadds1  28375  ltnegs  28431  negleft  28444  negright  28445  muls0ord  28571  abslts  28635  onlts  28653  n0subs  28749  n0ltsp1le  28751  z12sge0  28869  iscgrglt  28977  brbtwn  29477  brcgr  29478  brbtwn2  29483  axcontlem7  29548  uhgr0vb  29650  edglnl  29721  ausgrusgrb  29746  ushgredgedg  29810  ushgredgedgloop  29812  usgr0vb  29818  usgr1v  29837  nbupgr  29925  nbumgrvtx  29927  nbuhgr2vtx1edgb  29933  edgusgrnbfin  29954  nb3grprlem1  29961  uvtxnbvtxm1  29987  cusgrfilem2  30037  uhgr0edg0rgrb  30155  cusgrm1rusgr  30163  spthonepeq  30338  usgr2pth  30350  wlkiswwlks  30465  wlkiswwlkupgr  30467  wlklnwwlkn  30473  wlklnwwlknupgr  30475  wwlksnextbi  30483  wwlksnredwwlkn0  30485  wwlksnextwrd  30486  wwlksnextprop  30501  usgrwwlks2on  30547  umgrwwlks2on  30548  elwspths2on  30551  elwspths2onw  30552  usgr2wspthons3  30556  elwwlks2  30558  elwspths2spth  30559  clwlkclwwlklem3  30592  loopclwwlkn1b  30633  clwwlknon1sn  30691  clwwlknonwwlknonb  30697  loop1cycl  30744  umgr3v3e3cycl  30785  eupth2lem3lem4  30832  frgr0v  30863  frgr3vlem2  30875  2clwwlk2clwwlk  30951  wlkl0  30968  grpoinvf  31134  nvmul0or  31252  nvz  31271  diporthcom  31318  ubthlem3  31474  hvmul0or  31627  his6  31701  hial0  31704  hial02  31705  orthcom  31710  normgt0  31729  ocin  31898  occon3  31899  shsel3  31917  shlub  32016  chssoc  32098  h1de2bi  32156  spansncol  32170  elspansn4  32175  spansnss2  32177  sumspansn  32251  lnopcnbd  32638  lnfncnbd  32659  riesz1  32667  elpjrn  32792  cvcon3  32886  dmdmd  32902  dmdbr3  32907  dmdbr4  32908  dmdbr5  32910  mdslmd1i  32931  atcveq0  32950  chcv1  32957  atssma  32980  atcv0eq  32981  atcv1  32982  disjeq1f  33167  br8d  33202  fpwrelmap  33325  xaddeq0  33345  eliccelico  33369  elicoelioo  33370  indf1ofs  33433  isarchiofld  33760  unitdivcld  34533  xrge0iifcnv  34565  lmxrge0  34584  eulerpartlemgh  35010  dstfrvunirn  35107  fnfvintima  35714  fnrelpredd  35720  rankfilimb  35728  fineqvnttrclse  35792  cusgracyclt3v  35921  cvmliftmolem2  36047  cvmlift2lem12  36079  satfvsucsuc  36130  satfdm  36134  fmlasuc  36151  satffunlem1lem2  36168  satffunlem2lem2  36171  mthmb  36346  climuzcnv  36436  br8  36521  br6  36522  br4  36523  funbreq  36534  axextbdist  36562  dfrdg4  36715  cgrcom  36755  cgrcoml  36761  cgrdegen  36769  btwncom  36779  brsegle  36873  brsegle2  36874  colinbtwnle  36883  btwnoutside  36890  broutsideof3  36891  outsidele  36897  lineunray  36912  lineelsb2  36913  ltnmul  36965  ltnadd  36967  elicc3  37105  nn0prpwlem  37110  opnbnd  37113  cldbnd  37114  opnregcld  37118  cldregopn  37119  fnessref  37145  refssfne  37146  neibastop2  37149  fnemeet2  37155  fnejoin2  37157  fgmin  37158  ontgval  37219  ordtop  37224  ordcmp  37235  nndivsub  37245  bj-cbval  37545  bj-cbvex  37546  bj-19.21t  37663  bj-19.23t  37664  bj-19.42t  37667  bj-sbft  37680  bj-nnf-cbval  37682  bj-cbv2hv  37709  bj-equsal1t  37734  bj-19.21t0  37742  bj-ceqsalt0  37796  bj-ceqsalt1  37797  bj-xpnzexb  37874  bj-axreprepsep  37991  cgsex2gd  38059  bj-idreseq  38084  bj-imdiridlem  38107  bj-finsumval0  38207  bj-fvimacnv0  38208  bj-isrvec2  38222  bj-bary1  38234  dfgcd3  38246  isbasisrelowllem1  38279  isbasisrelowllem2  38280  finxpsuclem  38321  wl-lem-exsb  38499  wl-mo3t  38509  poimirlem6  38545  poimirlem7  38546  poimirlem16  38555  poimirlem19  38558  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  cnambfre  38587  itg2addnc  38593  brabg2  38652  istotbnd3  38706  sstotbnd2  38709  sstotbnd  38710  sstotbnd3  38711  ssbnd  38723  ismtybnd  38742  reheibor  38774  grpoeqdivid  38816  grpokerinj  38828  rngosn3  38859  rngoueqz  38875  1idl  38961  0rngo  38962  divrngidl  38963  igenval2  39001  ispridlc  39005  isdmn3  39009  relcnveq3  39260  iss2  39277  elrelscnveq3  39560  funALTVeq  39718  disjeq  39767  prtlem10  39923  prter2  39939  dral1-o  39962  lshpinN  40047  lsatcveq0  40090  lsatcv0eq  40105  lsatcv1  40106  islshpcv  40111  lkr0f  40152  lkrshp4  40166  lshpkrlem1  40168  lshpset2N  40177  lfl1dim  40179  lfl1dim2N  40180  lub0N  40247  glb0N  40251  oplecon3b  40258  cmtcomN  40307  cmtbr3N  40312  cmtbr4N  40313  cvrnbtwn2  40333  cvrnbtwn3  40334  cvrcon3b  40335  cvrnbtwn4  40337  cvrcmp  40341  atcvreq0  40372  atnle  40375  atlatle  40378  cvlexchb1  40388  cvlcvr1  40397  hlrelat2  40461  exatleN  40462  cvrval3  40471  cvrval4N  40472  cvrexch  40478  atcvr0eq  40484  lnnat  40485  atcvrj0  40486  atcvrj2b  40490  atltcvr  40493  atbtwn  40504  ps-1  40535  3at  40548  islln2a  40575  llncmp  40580  islpln2a  40606  lplncmp  40620  islvol2aN  40650  4at  40671  lvolcmp  40675  pmaple  40819  lncmp  40841  paddss  40903  llnexchb2lem  40926  2polcon4bN  40976  ispsubcl2N  41005  lhpat3  41104  lautcvr  41150  ltrnid  41193  trlval2  41221  trlatn0  41230  ltrnideq  41233  trlnidatb  41235  cdlemeg49lebilem  41597  trlord  41627  cdlemg1a  41628  cdlemg1cex  41646  tendoid0  41883  dva1dim  42043  cdlemm10N  42176  diarnN  42187  cdlemn  42270  dihlspsnssN  42390  dihatexv  42396  dochkrshp  42444  dochkrshp4  42447  djhlsmcl  42472  lcfl6  42558  lcfl8  42560  lcfrvalsnN  42599  lcfrlem9  42608  mapdval2N  42688  mapdordlem2  42695  mapd1o  42706  mapd0  42723  mapdheq2biN  42788  nnproddivdvdsd  43051  primrootspoweq0  43157  aks6d1c1p1  43158  aks6d1c5lem1  43187  sticksstones11  43207  sticksstones22  43219  grpods  43245  unitscyglem2  43247  eqresfnbd  43287  expeq1d  43382  expeqidd  43383  zdivgd  43389  sn-remul0ord  43460  mulgt0b1d  43537  frlmfzowrdb  43572  frlmsnic  43605  evlselvlem  43617  prjspreln0  43638  elrfi  43705  diophrw  43770  eldioph2b  43774  diophin  43783  rexrabdioph  43801  rmxycomplete  43924  coprmdvdsb  43992  jm2.19  44000  jm2.26  44009  jm2.27  44015  limsuc2  44048  dgraa0p  44151  rngunsnply  44171  fiuneneq  44194  unielss  44220  oaabsb  44296  nnoeomeqom  44314  cantnfresb  44326  tfsconcatrn  44344  tfsconcat0b  44348  tfsconcatrev  44350  oadif1lem  44381  oadif1  44382  fzunt  44456  fzuntd  44457  fzunt1d  44458  fzuntgd  44459  pwelg  44561  nzss  45301  dvconstbi  45318  expgrowth  45319  bcc0  45324  axc11next  45390  pm14.24  45416  sbiota1  45418  sbcim2g  45521  sineq0ALT  45919  mapss2  46219  fsneqrn  46224  mapssbi  46226  rnmptbd2lem  46260  infnsuprnmpt  46262  rnmptbdlem  46267  xralrple2  46366  infxrunb2  46379  xralrple4  46384  xralrple3  46385  xrralrecnnle  46394  xrralrecnnge  46401  reclt0  46402  supxrunb3  46410  supxrleubrnmpt  46416  xrre4  46421  unb2ltle  46425  rexabslelem  46428  suprleubrnmpt  46432  infxrunb3rnmpt  46438  uzub  46441  supminfrnmpt  46455  iccintsng  46535  sqrlearg  46565  uzinico  46571  preimaiocmnf  46572  limcresiooub  46652  limclr  46665  climeldmeq  46675  limsuppnflem  46720  limsupmnflem  46730  limsupmnfuzlem  46736  limsupre3lem  46742  limsupre3uzlem  46745  liminfreuzlem  46812  dvnmul  46953  dvmptfprodlem  46954  ismbl3  46996  ismbl4  47003  fourierdlem50  47166  fourierdlem89  47205  fourierdlem91  47207  dfsalgen2  47351  sge0repnf  47396  sge0lefi  47408  sge0resplit  47416  sge0fodjrnlem  47426  voliunsge0lem  47482  hspdifhsp  47626  isvonmbl  47648  ovnovollem3  47668  vonvolmbl  47671  pimrecltpos  47718  preimaicomnf  47721  pimrecltneg  47734  issmflem  47737  issmfle  47755  issmfgt  47766  smfaddlem1  47773  issmfge  47780  smfresal  47798  smflimmpt  47820  smfinflem  47827  smflimsuplem7  47836  smflimsupmpt  47839  sigarcol  47874  tmachlem-agreeprod  47947  confun  48009  or2expropbi  48104  fsetsniunop  48119  fcoresf1b  48140  f1cof1b  48147  funfocofob  48148  rexsb  48169  euoreqb  48179  ralbinrald  48192  rlimdmafv  48247  fafv2elrnb  48305  tz6.12c-afv2  48312  dfatbrafv2b  48315  fnbrafv2b  48318  rlimdmafv2  48328  f1oresf1o2  48361  el1fzopredsuc  48396  2ffzoeq  48398  nnmul2b  48401  modlt0b  48439  nndivides2  48454  imasetpreimafvbijlemfo  48487  iccpartiun  48516  ichnfb  48547  ich2exprop  48553  sprsymrelfolem2  48575  paireqne  48593  prprelprb  48599  reupr  48604  nprmmul2  48610  nprmmul3  48611  requad01  48719  requad1  48720  requad2  48721  dfodd6  48735  dfeven4  48736  evensumeven  48805  sbgoldbalt  48879  clnbgrel  48926  dfclnbgr6  48954  dfnbgr6  48955  isubgredg  48964  isuspgrim0  48992  isuspgrim  48994  gricushgr  49015  uhgrimisgrgriclem  49028  clnbgrgrim  49032  grimedg  49033  usgrgrtrirex  49048  uspgrlimlem2  49087  uspgrlim  49090  gpgedgiov  49163  gpgedg2ov  49164  gpgedg2iv  49165  gpgnbgrvtx0  49172  gpgnbgrvtx1  49173  isassintop  49307  uzlidlring  49332  rngcisoALTV  49374  ringcisoALTV  49408  isidom3  49442  domnmsuppn0  49481  lindslininds  49576  snlindsntor  49583  isldepslvec2  49597  affinecomb1  49814  prelrrx2b  49826  rrx2plord2  49834  eenglngeehlnm  49851  rrx2vlinest  49853  line2xlem  49865  line2x  49866  line2y  49867  itsclc0xyqsolb  49882  itsclquadb  49888  mpbiran3d  49907  opnneibid  50019  iscnrm3lem2  50043  fullthinc2  50559  thincciso  50561  alsralrex  50908  alsraln0  50909