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  8199  extmptsuppeq  8206  rntpos  8257  smoiso2  8378  seqomlem2  8462  oaord  8556  oawordex  8566  oaordex  8567  omord2  8576  om00  8584  oeord  8598  nnaord  8629  nnmord  8642  nnawordex  8647  nnaordex  8648  nnaordex2  8649  eldifsucnn  8674  erexb  8744  swoord1  8751  swoord2  8752  ecelqsdmb  8808  iiner  8811  eceqoveq  8844  mapsnd  8915  ralxpmap  8925  omxpenlem  9098  domtriord  9143  mapxpen  9163  mapunen  9166  ssenen  9171  enfi  9203  nneneq  9222  nndomog  9229  onomeneq  9230  en1eqsnbi  9268  fodomfib  9321  f1opwfi  9346  fsuppunbi  9382  elfiun  9423  suplub2  9454  ordiso2  9510  ordiso  9511  oieu  9534  brwdom2  9568  brwdom3  9577  cantnflem1  9691  ttrclselem2  9728  elhf2  9911  cardidm  10041  carddom2  10059  pm54.43  10083  acnen  10133  acnen2  10135  alephord  10155  alephinit  10175  dfac5  10208  infdif2  10288  fictb  10323  coflim  10340  fincssdom  10402  fin23lem25  10403  isf32lem9  10440  isf34lem4  10456  fin1a2lem11  10489  axdc3lem2  10530  ficard  10650  fpwwe2lem11  10727  fpwwe2  10729  indpi  10993  nqereq  11021  1idpr  11115  ltapr  11131  leltne  11400  ltlen  11412  ltadd2  11415  addlsub  11733  addid0  11736  ltord1  11843  mul0or  11957  ldiv  12152  ltmul1  12168  mulge0b  12188  lt2msq  12203  nnsub  12383  nn0sub  12657  zrevaddcl  12742  zltp1le  12747  zdiv  12770  nneo  12784  zeo2  12787  zmax  13073  zbtwnre  13074  qrevaddcl  13100  xrlttri  13269  xrleltne  13275  xralrple  13336  xltneg  13348  xleadd1  13386  xlemul1  13421  supxrunb1  13450  supxrunb2  13451  ioo0  13502  iccid  13522  ico0  13523  ioc0  13524  icc0  13525  difreicc  13616  iccsplit  13617  zltaddlt1le  13637  0fz1  13678  uzsplit  13731  fzm1  13742  fzrevral  13747  ssfzo12bi  13897  elfznelfzob  13910  flge  13946  modid2  14039  modmuladd  14057  ssnn0fi  14129  seqf1olem1  14185  hashen  14492  hashdom  14524  hash2exprb  14617  pr2pwpr  14625  hashtpg  14631  hash3tpexb  14640  len0nnbi  14697  ccats1pfxeqbi  14892  reuccatpfxs1  14897  repsdf2  14930  scshwfzeqfzo  14978  relexpindlem  15217  shftlem  15222  shftuz  15223  abslt  15483  absle  15484  rexico  15522  cau3lem  15523  reusq0  15633  rlim2lt  15665  rlim3  15666  o1lo1  15705  rlimdm  15719  climshft  15744  o1dif  15798  isercolllem2  15834  isercoll  15836  zsum  15885  fsum  15887  fsum00  15966  incexclem  16006  zprod  16105  fprod  16109  dvdsval2  16426  moddvds  16434  negdvdsb  16443  dvdsnegb  16444  dvdscmulr  16455  dvdsmulcr  16456  dvdssub2  16472  dvdsaddre2b  16478  fzo0dvdseq  16494  mod2eq1n2dvds  16518  ltoddhalfle  16532  sumodd  16559  bitsf1ocnv  16615  sadcaddlem  16628  bitsuz  16645  dvdsgcdb  16719  gcdzeq  16726  dvdsexpnn  16741  lcmeq0  16776  lcmdvdsb  16789  lcmfeq0b  16806  lcmf  16809  lcmfdvdsb  16819  coprmgcdb  16825  cncongr  16845  isprm2lem  16857  dvdsprime  16863  dvdsprm  16880  isprm7  16885  coprm  16888  euclemma  16890  rpexp  16899  prmdvdsncoprmbd  16904  prmdiveq  16964  hashgcdlem  16966  odzdvds  16974  pythagtrip  17013  pc2dvds  17058  pcprmpw2  17061  pcprmpw  17062  vdwapun  17153  ramtcl2  17190  firest  17604  mrieqv2d  17814  isacs2  17828  isssc  17996  setciso  18267  posasymb  18494  pleval2  18510  pltval3  18512  lublecllem  18533  joinle  18559  meetle  18573  latdisd  18672  lubun  18690  clatleglb  18693  letsr  18768  intopsn  18833  gsumval2a  18875  frmdss2  19060  isgrpid2  19188  isgrpinv  19205  f1ghm0to0  19460  symg1bas  19606  oddvdsnn0  19759  oddvds  19762  odeq  19765  odeq1  19775  gexdvds  19799  pgpfi  19820  pgpssslw  19829  fislw  19840  sylow3lem2  19843  lsmelvalm  19866  lsmlub  19879  lsmss1b  19881  lsmss2b  19883  efgs1b  19951  cyggenod  20099  cyggexb  20114  dprdfeq0  20239  ablsimpgfind  20327  ringinvnz1ne0  20532  ringinvnzdiv  20533  unitmulclb  20612  dvreq1  20642  isnzr2  20769  0ringnnzr  20777  0ring01eqbi2  20784  0ring01eqbi  20785  rngciso  20891  ringciso  20925  rrgeq0  20953  domneq0  20961  isabvd  21070  issrngd  21113  lssats2  21276  lspsneq0  21288  lsmelval2  21361  lvecvs0or  21387  lspsneq  21401  lspsneu  21402  lidl1el  21506  rspprop  21525  lidldvgen  21659  pzriprnglem10  21797  pzriprnglem11  21798  znunit  21870  psgndif  21909  ipeq0  21945  ocvsscon  21982  pjdm2  22018  obselocv  22035  islinds4  22142  psdmul  22488  ply1coe1eq  22619  cply1coe0bi  22621  mat1dimelbas  22787  matunitlindf  22997  cramer  23010  toponcomb  23248  tgss3  23305  clsval2  23369  isopn3  23385  elcls3  23402  opncldf1  23403  neiint  23423  neips  23432  opnneissb  23433  opnssneib  23434  opnnei  23439  tpnei  23440  opnneiid  23445  restcld  23491  restopnb  23494  tgcn  23571  tgcnp  23572  subbascn  23573  iscnp4  23582  cnpnei  23583  cncls2  23592  cncls  23593  cnntr  23594  lmss  23617  hausnei2  23672  lpcls  23683  ordtt1  23698  cmpsub  23719  tgcmp  23720  1stcelcls  23781  locfincmp  23846  kgencn2  23877  ptpjpre1  23891  upxp  23943  txcn  23946  txlm  23968  tgqtop  24032  kqfvima  24050  isr0  24057  regr1lem2  24060  hmeoopn  24086  hmeocld  24087  ptuncnv  24127  fbunfip  24189  fgss2  24194  ufilb  24226  ufprim  24229  trufil  24230  cfinufil  24248  ufildr  24251  elfm2  24268  elfm3  24270  rnelfm  24273  fmfnfmlem4  24277  fmco  24281  flimtopon  24290  flimopn  24295  fbflim2  24297  flimrest  24303  flffbas  24315  cnpflf  24321  fclstopon  24332  fclsnei  24339  fclsbas  24341  fclsfnflim  24347  fclscmp  24350  ufilcmp  24352  isfcf  24354  fcfnei  24355  cnpfcf  24361  alexsubb  24366  alexsubALT  24371  cldsubg  24431  tgphaus  24437  tgpt0  24439  tsmsgsum  24459  tsmsres  24464  xbln0  24734  blssexps  24746  blssex  24747  isxms2  24768  prdsbl  24811  neibl  24821  metss  24828  met2ndc  24843  metrest  24844  metcnp3  24860  tngngp3  24976  nmoeq0  25056  xrsxmet  25130  reconn  25149  iccpnfcnv  25266  fgcfil  25593  iscau4  25601  cfilres  25618  iunmbl2  25879  ismbf3d  25976  mbfaddlem  25982  i1faddlem  26015  i1fmullem  26016  ellimc3  26200  dvfsumlem2  26348  tdeglem4  26379  deg1nn0clb  26409  deg1lt0  26410  dvdsq1p  26482  plypf1  26532  0dgrb  26566  plymul0or  26600  taylthlem2  26702  ulmshft  26718  ulmcaulem  26722  ulmcau  26723  cosord  26860  eff1olem  26877  lognegb  26919  eflogeq  26931  logdivlt  26950  efopn  26987  cxpeq0  27007  cxpeq  27086  angpieqvd  27160  dcubic  27175  asinsinb  27226  acoscosb  27227  atantanb  27253  rlimcnp  27294  isppw  27442  isppw2  27443  vmappw  27444  isnsqf  27463  ppieq0  27504  fsumdvdsdiag  27512  dvdsppwf1o  27514  fsumfldivdiag  27518  chpeq0  27536  chteq0  27537  dchrptlem1  27592  lgsdir2lem4  27656  lgsne0  27663  lgsqr  27679  lgsdchrval  27682  gausslemma2dlem1a  27693  lgsquadlem1  27708  m1lgs  27716  2sqreultblem  27776  2sqreunnltblem  27779  nodenselem8  28049  ltlesnd  28133  oldlim  28274  ltslpss  28295  leadds1  28376  ltnegs  28432  negleft  28445  negright  28446  muls0ord  28572  abslts  28636  onlts  28654  n0subs  28750  n0ltsp1le  28752  z12sge0  28870  iscgrglt  28978  brbtwn  29478  brcgr  29479  brbtwn2  29484  axcontlem7  29549  uhgr0vb  29651  edglnl  29722  ausgrusgrb  29747  ushgredgedg  29811  ushgredgedgloop  29813  usgr0vb  29819  usgr1v  29838  nbupgr  29926  nbumgrvtx  29928  nbuhgr2vtx1edgb  29934  edgusgrnbfin  29955  nb3grprlem1  29962  uvtxnbvtxm1  29988  cusgrfilem2  30038  uhgr0edg0rgrb  30156  cusgrm1rusgr  30164  spthonepeq  30339  usgr2pth  30351  wlkiswwlks  30466  wlkiswwlkupgr  30468  wlklnwwlkn  30474  wlklnwwlknupgr  30476  wwlksnextbi  30484  wwlksnredwwlkn0  30486  wwlksnextwrd  30487  wwlksnextprop  30502  usgrwwlks2on  30548  umgrwwlks2on  30549  elwspths2on  30552  elwspths2onw  30553  usgr2wspthons3  30557  elwwlks2  30559  elwspths2spth  30560  clwlkclwwlklem3  30593  loopclwwlkn1b  30634  clwwlknon1sn  30692  clwwlknonwwlknonb  30698  loop1cycl  30745  umgr3v3e3cycl  30786  eupth2lem3lem4  30833  frgr0v  30864  frgr3vlem2  30876  2clwwlk2clwwlk  30952  wlkl0  30969  grpoinvf  31135  nvmul0or  31253  nvz  31272  diporthcom  31319  ubthlem3  31475  hvmul0or  31628  his6  31702  hial0  31705  hial02  31706  orthcom  31711  normgt0  31730  ocin  31899  occon3  31900  shsel3  31918  shlub  32017  chssoc  32099  h1de2bi  32157  spansncol  32171  elspansn4  32176  spansnss2  32178  sumspansn  32252  lnopcnbd  32639  lnfncnbd  32660  riesz1  32668  elpjrn  32793  cvcon3  32887  dmdmd  32903  dmdbr3  32908  dmdbr4  32909  dmdbr5  32911  mdslmd1i  32932  atcveq0  32951  chcv1  32958  atssma  32981  atcv0eq  32982  atcv1  32983  disjeq1f  33210  br8d  33245  fpwrelmap  33368  xaddeq0  33388  eliccelico  33412  elicoelioo  33413  indf1ofs  33476  isarchiofld  33803  unitdivcld  34576  xrge0iifcnv  34608  lmxrge0  34627  eulerpartlemgh  35053  dstfrvunirn  35150  fnfvintima  35757  fnrelpredd  35763  rankfilimb  35771  fineqvnttrclse  35835  cusgracyclt3v  35964  cvmliftmolem2  36090  cvmlift2lem12  36122  satfvsucsuc  36173  satfdm  36177  fmlasuc  36194  satffunlem1lem2  36211  satffunlem2lem2  36214  mthmb  36389  climuzcnv  36479  br8  36564  br6  36565  br4  36566  funbreq  36577  axextbdist  36605  dfrdg4  36758  cgrcom  36798  cgrcoml  36804  cgrdegen  36812  btwncom  36822  brsegle  36916  brsegle2  36917  colinbtwnle  36926  btwnoutside  36933  broutsideof3  36934  outsidele  36940  lineunray  36955  lineelsb2  36956  ltnmul  37008  ltnadd  37010  elicc3  37148  nn0prpwlem  37153  opnbnd  37156  cldbnd  37157  opnregcld  37161  cldregopn  37162  fnessref  37188  refssfne  37189  neibastop2  37192  fnemeet2  37198  fnejoin2  37200  fgmin  37201  ontgval  37262  ordtop  37267  ordcmp  37278  nndivsub  37288  bj-cbval  37588  bj-cbvex  37589  bj-19.21t  37706  bj-19.23t  37707  bj-19.42t  37710  bj-sbft  37723  bj-nnf-cbval  37725  bj-cbv2hv  37752  bj-equsal1t  37777  bj-19.21t0  37785  bj-ceqsalt0  37839  bj-ceqsalt1  37840  bj-xpnzexb  37917  bj-axreprepsep  38034  cgsex2gd  38102  bj-idreseq  38127  bj-imdiridlem  38150  bj-finsumval0  38250  bj-fvimacnv0  38251  bj-isrvec2  38265  bj-bary1  38277  dfgcd3  38289  isbasisrelowllem1  38322  isbasisrelowllem2  38323  finxpsuclem  38364  wl-lem-exsb  38542  wl-mo3t  38552  poimirlem6  38588  poimirlem7  38589  poimirlem16  38598  poimirlem19  38601  poimirlem22  38604  poimirlem23  38605  poimirlem24  38606  cnambfre  38630  itg2addnc  38636  brabg2  38695  istotbnd3  38749  sstotbnd2  38752  sstotbnd  38753  sstotbnd3  38754  ssbnd  38766  ismtybnd  38785  reheibor  38817  grpoeqdivid  38859  grpokerinj  38871  rngosn3  38902  rngoueqz  38918  1idl  39004  0rngo  39005  divrngidl  39006  igenval2  39044  ispridlc  39048  isdmn3  39052  relcnveq3  39303  iss2  39320  elrelscnveq3  39603  funALTVeq  39761  disjeq  39810  prtlem10  39966  prter2  39982  dral1-o  40005  lshpinN  40090  lsatcveq0  40133  lsatcv0eq  40148  lsatcv1  40149  islshpcv  40154  lkr0f  40195  lkrshp4  40209  lshpkrlem1  40211  lshpset2N  40220  lfl1dim  40222  lfl1dim2N  40223  lub0N  40290  glb0N  40294  oplecon3b  40301  cmtcomN  40350  cmtbr3N  40355  cmtbr4N  40356  cvrnbtwn2  40376  cvrnbtwn3  40377  cvrcon3b  40378  cvrnbtwn4  40380  cvrcmp  40384  atcvreq0  40415  atnle  40418  atlatle  40421  cvlexchb1  40431  cvlcvr1  40440  hlrelat2  40504  exatleN  40505  cvrval3  40514  cvrval4N  40515  cvrexch  40521  atcvr0eq  40527  lnnat  40528  atcvrj0  40529  atcvrj2b  40533  atltcvr  40536  atbtwn  40547  ps-1  40578  3at  40591  islln2a  40618  llncmp  40623  islpln2a  40649  lplncmp  40663  islvol2aN  40693  4at  40714  lvolcmp  40718  pmaple  40862  lncmp  40884  paddss  40946  llnexchb2lem  40969  2polcon4bN  41019  ispsubcl2N  41048  lhpat3  41147  lautcvr  41193  ltrnid  41236  trlval2  41264  trlatn0  41273  ltrnideq  41276  trlnidatb  41278  cdlemeg49lebilem  41640  trlord  41670  cdlemg1a  41671  cdlemg1cex  41689  tendoid0  41926  dva1dim  42086  cdlemm10N  42219  diarnN  42230  cdlemn  42313  dihlspsnssN  42433  dihatexv  42439  dochkrshp  42487  dochkrshp4  42490  djhlsmcl  42515  lcfl6  42601  lcfl8  42603  lcfrvalsnN  42642  lcfrlem9  42651  mapdval2N  42731  mapdordlem2  42738  mapd1o  42749  mapd0  42766  mapdheq2biN  42831  nnproddivdvdsd  43094  primrootspoweq0  43200  aks6d1c1p1  43201  aks6d1c5lem1  43230  sticksstones11  43250  sticksstones22  43262  grpods  43288  unitscyglem2  43290  eqresfnbd  43330  expeq1d  43425  expeqidd  43426  zdivgd  43432  sn-remul0ord  43503  mulgt0b1d  43580  frlmfzowrdb  43615  frlmsnic  43648  evlselvlem  43660  prjspreln0  43681  elrfi  43749  diophrw  43814  eldioph2b  43818  diophin  43827  rexrabdioph  43845  rmxycomplete  43968  coprmdvdsb  44036  jm2.19  44044  jm2.26  44053  jm2.27  44059  limsuc2  44092  dgraa0p  44195  rngunsnply  44215  fiuneneq  44238  unielss  44264  oaabsb  44340  nnoeomeqom  44358  cantnfresb  44370  tfsconcatrn  44388  tfsconcat0b  44392  tfsconcatrev  44394  oadif1lem  44425  oadif1  44426  fzunt  44500  fzuntd  44501  fzunt1d  44502  fzuntgd  44503  pwelg  44605  nzss  45345  dvconstbi  45362  expgrowth  45363  bcc0  45368  axc11next  45434  pm14.24  45460  sbiota1  45462  sbcim2g  45565  sineq0ALT  45963  mapss2  46263  fsneqrn  46268  mapssbi  46270  rnmptbd2lem  46304  infnsuprnmpt  46306  rnmptbdlem  46311  xralrple2  46410  infxrunb2  46423  xralrple4  46428  xralrple3  46429  xrralrecnnle  46438  xrralrecnnge  46445  reclt0  46446  supxrunb3  46454  supxrleubrnmpt  46460  xrre4  46465  unb2ltle  46469  rexabslelem  46472  suprleubrnmpt  46476  infxrunb3rnmpt  46482  uzub  46485  supminfrnmpt  46499  iccintsng  46579  sqrlearg  46609  uzinico  46615  preimaiocmnf  46616  limcresiooub  46696  limclr  46709  climeldmeq  46719  limsuppnflem  46764  limsupmnflem  46774  limsupmnfuzlem  46780  limsupre3lem  46786  limsupre3uzlem  46789  liminfreuzlem  46856  dvnmul  46997  dvmptfprodlem  46998  ismbl3  47040  ismbl4  47047  fourierdlem50  47210  fourierdlem89  47249  fourierdlem91  47251  dfsalgen2  47395  sge0repnf  47440  sge0lefi  47452  sge0resplit  47460  sge0fodjrnlem  47470  voliunsge0lem  47526  hspdifhsp  47670  isvonmbl  47692  ovnovollem3  47712  vonvolmbl  47715  pimrecltpos  47762  preimaicomnf  47765  pimrecltneg  47778  issmflem  47781  issmfle  47799  issmfgt  47810  smfaddlem1  47817  issmfge  47824  smfresal  47842  smflimmpt  47864  smfinflem  47871  smflimsuplem7  47880  smflimsupmpt  47883  sigarcol  47918  tmachlem-agreeprod  47991  confun  48053  or2expropbi  48148  fsetsniunop  48163  fcoresf1b  48184  f1cof1b  48191  funfocofob  48192  rexsb  48213  euoreqb  48223  ralbinrald  48236  rlimdmafv  48291  fafv2elrnb  48349  tz6.12c-afv2  48356  dfatbrafv2b  48359  fnbrafv2b  48362  rlimdmafv2  48372  f1oresf1o2  48405  el1fzopredsuc  48440  2ffzoeq  48442  nnmul2b  48445  modlt0b  48483  nndivides2  48498  imasetpreimafvbijlemfo  48531  iccpartiun  48560  ichnfb  48591  ich2exprop  48597  sprsymrelfolem2  48619  paireqne  48637  prprelprb  48643  reupr  48648  nprmmul2  48654  nprmmul3  48655  requad01  48763  requad1  48764  requad2  48765  dfodd6  48779  dfeven4  48780  evensumeven  48849  sbgoldbalt  48923  clnbgrel  48970  dfclnbgr6  48998  dfnbgr6  48999  isubgredg  49008  isuspgrim0  49036  isuspgrim  49038  gricushgr  49059  uhgrimisgrgriclem  49072  clnbgrgrim  49076  grimedg  49077  usgrgrtrirex  49092  uspgrlimlem2  49131  uspgrlim  49134  gpgedgiov  49207  gpgedg2ov  49208  gpgedg2iv  49209  gpgnbgrvtx0  49216  gpgnbgrvtx1  49217  isassintop  49351  uzlidlring  49376  rngcisoALTV  49418  ringcisoALTV  49452  isidom3  49486  domnmsuppn0  49525  lindslininds  49620  snlindsntor  49627  isldepslvec2  49641  affinecomb1  49858  prelrrx2b  49870  rrx2plord2  49878  eenglngeehlnm  49895  rrx2vlinest  49897  line2xlem  49909  line2x  49910  line2y  49911  itsclc0xyqsolb  49926  itsclquadb  49932  mpbiran3d  49951  opnneibid  50063  iscnrm3lem2  50087  fullthinc2  50603  thincciso  50605  alsralrex  50952  alsraln0  50953