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  3093  rexbi  3094  ralbida  3249  ceqsalt  3464  rspcebdv  3559  rspceb2dv  3569  ceqex  3595  elabgtOLD  3616  mob2  3662  reu6  3673  sbciegftOLD  3767  sbcg  3802  2reu2  3837  csbiebt  3867  dfss2  3908  reupick  4270  reupick2  4272  uneqdifeq  4433  prnebg  4800  preqsnd  4803  prel12g  4808  iuneqconst  4946  disjeq2  5057  disjeq1  5060  disjss3  5085  reusv2lem2  5338  reusv2lem3  5339  alxfr  5346  ralxfrd  5347  ralxfrd2  5351  copsexgw  5440  copsexg  5441  snopeqop  5456  euotd  5463  poeq2  5538  sotric  5564  sotrieq  5565  freq2  5594  seeq1  5596  seeq2  5597  iss  5996  tz7.7  6345  ordtri1  6352  ordelinel  6422  funeq  6514  funssres  6538  f0dom0  6720  fnbrfvb  6886  ssimaex  6921  fvimacnv  7001  elpreima  7006  feldmfvelcdm  7034  eldmrexrnb  7040  fsn  7084  fnsnbg  7114  fnsnbOLD  7116  fmptsng  7118  fmptsnd  7119  fprb  7144  tpres  7151  fconst2g  7153  fconst5  7156  elunirn  7201  f1ocnvfvb  7229  f1prex  7234  foeqcnvco  7250  f1eqcocnv  7251  fliftfun  7262  soisores  7277  isofr  7292  isose  7293  isopo  7296  isoso  7298  f1oiso2  7302  eusvobj2  7354  oprabidw  7393  oprabid  7394  f1opw2  7617  oneqmin  7749  ordelsuc  7766  ordsucelsuc  7768  ordunisuc2  7790  limsuc  7795  fndmexb  7852  resf1ext2b  7881  f1ovv  7906  mptcnfimad  7934  op1steq  7981  opreuopreu  7982  funeldmdif  7996  fvn0elsuppb  8126  extmptsuppeq  8133  rntpos  8184  smoiso2  8304  seqomlem2  8385  oaord  8477  oawordex  8487  oaordex  8488  omord2  8497  om00  8505  oeord  8519  nnaord  8550  nnmord  8563  nnawordex  8568  nnaordex  8569  nnaordex2  8570  eldifsucnn  8595  erexb  8664  swoord1  8671  swoord2  8672  ecelqsdmb  8728  iiner  8731  eceqoveq  8764  mapsnd  8829  ralxpmap  8839  omxpenlem  9011  domtriord  9056  mapxpen  9076  mapunen  9079  ssenen  9084  enfi  9116  nneneq  9135  nndomog  9142  onomeneq  9143  en1eqsnbi  9181  fodomfib  9234  fodomfibOLD  9236  f1opwfi  9261  fsuppunbi  9297  elfiun  9338  suplub2  9369  ordiso2  9425  ordiso  9426  oieu  9449  brwdom2  9483  brwdom3  9492  cantnflem1  9605  ttrclselem2  9642  cardidm  9878  carddom2  9896  pm54.43  9920  acnen  9970  acnen2  9972  alephord  9992  alephinit  10012  dfac5  10046  infdif2  10126  fictb  10161  coflim  10178  fincssdom  10240  fin23lem25  10241  isf32lem9  10278  isf34lem4  10294  fin1a2lem11  10327  axdc3lem2  10368  ficard  10482  fpwwe2lem11  10559  fpwwe2  10561  indpi  10825  nqereq  10853  1idpr  10947  ltapr  10963  leltne  11230  ltlen  11242  ltadd2  11245  addlsub  11561  addid0  11564  ltord1  11671  mul0or  11785  ldiv  11984  ltmul1  12000  mulge0b  12021  lt2msq  12036  nnsub  12216  nn0sub  12482  zrevaddcl  12567  zltp1le  12572  zdiv  12594  nneo  12608  zeo2  12611  zmax  12890  zbtwnre  12891  qrevaddcl  12916  xrlttri  13085  xrleltne  13091  xralrple  13152  xltneg  13164  xleadd1  13202  xlemul1  13237  supxrunb1  13266  supxrunb2  13267  ioo0  13318  iccid  13338  ico0  13339  ioc0  13340  icc0  13341  difreicc  13432  iccsplit  13433  zltaddlt1le  13453  0fz1  13493  uzsplit  13545  fzm1  13556  fzrevral  13561  ssfzo12bi  13711  elfznelfzob  13724  flge  13759  modid2  13852  modmuladd  13870  ssnn0fi  13942  seqf1olem1  13998  hashen  14304  hashdom  14336  hash2exprb  14428  pr2pwpr  14436  hashtpg  14442  hash3tpexb  14451  len0nnbi  14508  ccats1pfxeqbi  14699  reuccatpfxs1  14704  repsdf2  14735  scshwfzeqfzo  14783  relexpindlem  15020  shftlem  15025  shftuz  15026  abslt  15272  absle  15273  rexico  15311  cau3lem  15312  reusq0  15422  rlim2lt  15454  rlim3  15455  o1lo1  15494  rlimdm  15508  climshft  15533  o1dif  15587  isercolllem2  15623  isercoll  15625  zsum  15675  fsum  15677  fsum00  15756  incexclem  15796  zprod  15897  fprod  15901  dvdsval2  16219  moddvds  16227  negdvdsb  16236  dvdsnegb  16237  dvdscmulr  16248  dvdsmulcr  16249  dvdssub2  16265  dvdsaddre2b  16271  fzo0dvdseq  16287  mod2eq1n2dvds  16311  ltoddhalfle  16325  sumodd  16352  bitsf1ocnv  16408  sadcaddlem  16421  bitsuz  16438  dvdsgcdb  16509  gcdzeq  16516  dvdssqlem  16530  lcmeq0  16564  lcmdvdsb  16577  lcmfeq0b  16594  lcmf  16597  lcmfdvdsb  16607  coprmgcdb  16613  cncongr  16633  isprm2lem  16645  dvdsprime  16651  dvdsprm  16668  isprm7  16673  coprm  16676  euclemma  16678  rpexp  16687  prmdvdsncoprmbd  16692  prmdiveq  16751  hashgcdlem  16753  odzdvds  16761  pythagtrip  16800  pc2dvds  16845  pcprmpw2  16848  pcprmpw  16849  vdwapun  16940  ramtcl2  16977  firest  17390  mrieqv2d  17600  isacs2  17614  isssc  17782  setciso  18053  posasymb  18280  pleval2  18296  pltval3  18298  lublecllem  18319  joinle  18345  meetle  18359  latdisd  18458  lubun  18476  clatleglb  18479  letsr  18554  intopsn  18617  gsumval2a  18648  frmdss2  18826  isgrpid2  18947  isgrpinv  18964  f1ghm0to0  19215  symg1bas  19361  oddvdsnn0  19514  oddvds  19517  odeq  19520  odeq1  19530  gexdvds  19554  pgpfi  19575  pgpssslw  19584  fislw  19595  sylow3lem2  19598  lsmelvalm  19621  lsmlub  19634  lsmss1b  19636  lsmss2b  19638  efgs1b  19706  cyggenod  19854  cyggexb  19869  dprdfeq0  19994  ablsimpgfind  20082  ringinvnz1ne0  20276  ringinvnzdiv  20277  unitmulclb  20356  dvreq1  20386  isnzr2  20490  0ringnnzr  20497  0ring01eqbi  20504  rngciso  20610  ringciso  20644  rrgeq0  20672  domneq0  20680  drngmul0orOLD  20733  isabvd  20784  issrngd  20827  lssats2  20990  lspsneq0  21002  lsmelval2  21076  lvecvs0or  21102  lspsneq  21116  lspsneu  21117  lidl1el  21220  lidldvgen  21328  pzriprnglem10  21484  pzriprnglem11  21485  znunit  21557  psgndif  21596  ipeq0  21632  ocvsscon  21669  pjdm2  21705  obselocv  21722  islinds4  21829  psdmul  22146  ply1coe1eq  22279  cply1coe0bi  22281  mat1dimelbas  22450  cramer  22670  toponcomb  22908  tgss3  22965  clsval2  23029  isopn3  23045  elcls3  23062  opncldf1  23063  neiint  23083  neips  23092  opnneissb  23093  opnssneib  23094  opnnei  23099  tpnei  23100  opnneiid  23105  restcld  23151  restopnb  23154  tgcn  23231  tgcnp  23232  subbascn  23233  iscnp4  23242  cnpnei  23243  cncls2  23252  cncls  23253  cnntr  23254  lmss  23277  hausnei2  23332  lpcls  23343  ordtt1  23358  cmpsub  23379  tgcmp  23380  1stcelcls  23440  locfincmp  23505  kgencn2  23536  ptpjpre1  23550  upxp  23602  txcn  23605  txlm  23627  tgqtop  23691  kqfvima  23709  isr0  23716  regr1lem2  23719  hmeoopn  23745  hmeocld  23746  ptuncnv  23786  fbunfip  23848  fgss2  23853  ufilb  23885  ufprim  23888  trufil  23889  cfinufil  23907  ufildr  23910  elfm2  23927  elfm3  23929  rnelfm  23932  fmfnfmlem4  23936  fmco  23940  flimtopon  23949  flimopn  23954  fbflim2  23956  flimrest  23962  flffbas  23974  cnpflf  23980  fclstopon  23991  fclsnei  23998  fclsbas  24000  fclsfnflim  24006  fclscmp  24009  ufilcmp  24011  isfcf  24013  fcfnei  24014  cnpfcf  24020  alexsubb  24025  alexsubALT  24030  cldsubg  24090  tgphaus  24096  tgpt0  24098  tsmsgsum  24118  tsmsres  24123  xbln0  24393  blssexps  24405  blssex  24406  isxms2  24427  prdsbl  24470  neibl  24480  metss  24487  met2ndc  24502  metrest  24503  metcnp3  24519  tngngp3  24635  nmoeq0  24715  xrsxmet  24789  reconn  24808  iccpnfcnv  24925  fgcfil  25252  iscau4  25260  cfilres  25277  iunmbl2  25538  ismbf3d  25635  mbfaddlem  25641  i1faddlem  25674  i1fmullem  25675  ellimc3  25860  dvfsumlem2  26008  tdeglem4  26039  deg1nn0clb  26069  deg1lt0  26070  dvdsq1p  26142  plypf1  26191  0dgrb  26225  plymul0or  26261  taylthlem2  26355  ulmshft  26372  ulmcaulem  26376  ulmcau  26377  cosord  26512  eff1olem  26529  lognegb  26571  eflogeq  26583  logdivlt  26602  efopn  26639  cxpeq0  26659  cxpeq  26738  angpieqvd  26812  dcubic  26827  asinsinb  26878  acoscosb  26879  atantanb  26905  rlimcnp  26946  isppw  27095  isppw2  27096  vmappw  27097  isnsqf  27116  ppieq0  27157  fsumdvdsdiag  27165  dvdsppwf1o  27167  fsumfldivdiag  27171  chpeq0  27189  chteq0  27190  dchrptlem1  27245  lgsdir2lem4  27309  lgsne0  27316  lgsqr  27332  lgsdchrval  27335  gausslemma2dlem1a  27346  lgsquadlem1  27361  m1lgs  27369  2sqreultblem  27429  2sqreunnltblem  27432  nodenselem8  27673  ltlesnd  27757  oldlim  27897  ltslpss  27918  leadds1  27999  ltnegs  28055  negleft  28068  negright  28069  muls0ord  28195  abslts  28259  onlts  28277  n0subs  28373  n0ltsp1le  28375  z12sge0  28493  iscgrglt  28600  brbtwn  28986  brcgr  28987  brbtwn2  28992  axcontlem7  29057  uhgr0vb  29159  edglnl  29230  ausgrusgrb  29252  ushgredgedg  29316  ushgredgedgloop  29318  usgr0vb  29324  usgr1v  29343  nbupgr  29431  nbumgrvtx  29433  nbuhgr2vtx1edgb  29439  edgusgrnbfin  29460  nb3grprlem1  29467  uvtxnbvtxm1  29493  cusgrfilem2  29544  uhgr0edg0rgrb  29662  cusgrm1rusgr  29670  spthonepeq  29839  usgr2pth  29851  wlkiswwlks  29963  wlkiswwlkupgr  29965  wlklnwwlkn  29971  wlklnwwlknupgr  29973  wwlksnextbi  29981  wwlksnredwwlkn0  29983  wwlksnextwrd  29984  wwlksnextprop  29999  usgrwwlks2on  30045  umgrwwlks2on  30046  elwspths2on  30049  elwspths2onw  30050  usgr2wspthons3  30054  elwwlks2  30056  elwspths2spth  30057  clwlkclwwlklem3  30090  loopclwwlkn1b  30131  clwwlknon1sn  30189  clwwlknonwwlknonb  30195  umgr3v3e3cycl  30273  eupth2lem3lem4  30320  frgr0v  30351  frgr3vlem2  30363  2clwwlk2clwwlk  30439  wlkl0  30456  grpoinvf  30622  nvmul0or  30740  nvz  30759  diporthcom  30806  ubthlem3  30962  hvmul0or  31115  his6  31189  hial0  31192  hial02  31193  orthcom  31198  normgt0  31217  ocin  31386  occon3  31387  shsel3  31405  shlub  31504  chssoc  31586  h1de2bi  31644  spansncol  31658  elspansn4  31663  spansnss2  31665  sumspansn  31739  lnopcnbd  32126  lnfncnbd  32147  riesz1  32155  elpjrn  32280  cvcon3  32374  dmdmd  32390  dmdbr3  32395  dmdbr4  32396  dmdbr5  32398  mdslmd1i  32419  atcveq0  32438  chcv1  32445  atssma  32468  atcv0eq  32469  atcv1  32470  bian1dOLD  32545  disjeq1f  32662  br8d  32700  fpwrelmap  32825  xaddeq0  32845  eliccelico  32869  elicoelioo  32870  indf1ofs  32945  isarchiofld  33279  unitdivcld  34065  xrge0iifcnv  34097  lmxrge0  34116  eulerpartlemgh  34542  dstfrvunirn  34639  fnrelpredd  35254  rankfilimb  35265  fineqvnttrclse  35288  loop1cycl  35339  cusgracyclt3v  35358  cvmliftmolem2  35484  cvmlift2lem12  35516  satfvsucsuc  35567  satfdm  35571  fmlasuc  35588  satffunlem1lem2  35605  satffunlem2lem2  35608  mthmb  35783  climuzcnv  35873  br8  35958  br6  35959  br4  35960  funbreq  35972  axextbdist  36000  dfrdg4  36153  cgrcom  36192  cgrcoml  36198  cgrdegen  36206  btwncom  36216  brsegle  36310  brsegle2  36311  colinbtwnle  36320  btwnoutside  36327  broutsideof3  36328  outsidele  36334  lineunray  36349  lineelsb2  36350  elhf2  36377  elicc3  36519  nn0prpwlem  36524  opnbnd  36527  cldbnd  36528  opnregcld  36532  cldregopn  36533  fnessref  36559  refssfne  36560  neibastop2  36563  fnemeet2  36569  fnejoin2  36571  fgmin  36572  ontgval  36633  ordtop  36638  ordcmp  36649  nndivsub  36659  bj-cbval  36960  bj-cbvex  36961  bj-19.21t  37078  bj-19.23t  37079  bj-19.42t  37082  bj-sbft  37095  bj-nnf-cbval  37097  bj-cbv2hv  37124  bj-equsal1t  37149  bj-19.21t0  37157  bj-ceqsalt0  37211  bj-ceqsalt1  37212  bj-xpnzexb  37288  bj-axreprepsep  37402  cgsex2gd  37471  bj-idreseq  37496  bj-imdiridlem  37519  bj-finsumval0  37619  bj-fvimacnv0  37620  bj-isrvec2  37634  bj-bary1  37646  dfgcd3  37658  isbasisrelowllem1  37689  isbasisrelowllem2  37690  finxpsuclem  37731  wl-lem-exsb  37909  wl-mo3t  37919  matunitlindf  37957  poimirlem6  37965  poimirlem7  37966  poimirlem16  37975  poimirlem19  37978  poimirlem22  37981  poimirlem23  37982  poimirlem24  37983  cnambfre  38007  itg2addnc  38013  brabg2  38056  istotbnd3  38110  sstotbnd2  38113  sstotbnd  38114  sstotbnd3  38115  ssbnd  38127  ismtybnd  38146  reheibor  38178  grpoeqdivid  38220  grpokerinj  38232  rngosn3  38263  rngoueqz  38279  1idl  38365  0rngo  38366  divrngidl  38367  igenval2  38405  ispridlc  38409  isdmn3  38413  relcnveq3  38666  iss2  38683  elrelscnveq3  38966  funALTVeq  39124  disjeq  39173  prtlem10  39329  prter2  39345  dral1-o  39368  lshpinN  39453  lsatcveq0  39496  lsatcv0eq  39511  lsatcv1  39512  islshpcv  39517  lkr0f  39558  lkrshp4  39572  lshpkrlem1  39574  lshpset2N  39583  lfl1dim  39585  lfl1dim2N  39586  lub0N  39653  glb0N  39657  oplecon3b  39664  cmtcomN  39713  cmtbr3N  39718  cmtbr4N  39719  cvrnbtwn2  39739  cvrnbtwn3  39740  cvrcon3b  39741  cvrnbtwn4  39743  cvrcmp  39747  atcvreq0  39778  atnle  39781  atlatle  39784  cvlexchb1  39794  cvlcvr1  39803  hlrelat2  39867  exatleN  39868  cvrval3  39877  cvrval4N  39878  cvrexch  39884  atcvr0eq  39890  lnnat  39891  atcvrj0  39892  atcvrj2b  39896  atltcvr  39899  atbtwn  39910  ps-1  39941  3at  39954  islln2a  39981  llncmp  39986  islpln2a  40012  lplncmp  40026  islvol2aN  40056  4at  40077  lvolcmp  40081  pmaple  40225  lncmp  40247  paddss  40309  llnexchb2lem  40332  2polcon4bN  40382  ispsubcl2N  40411  lhpat3  40510  lautcvr  40556  ltrnid  40599  trlval2  40627  trlatn0  40636  ltrnideq  40639  trlnidatb  40641  cdlemeg49lebilem  41003  trlord  41033  cdlemg1a  41034  cdlemg1cex  41052  tendoid0  41289  dva1dim  41449  cdlemm10N  41582  diarnN  41593  cdlemn  41676  dihlspsnssN  41796  dihatexv  41802  dochkrshp  41850  dochkrshp4  41853  djhlsmcl  41878  lcfl6  41964  lcfl8  41966  lcfrvalsnN  42005  lcfrlem9  42014  mapdval2N  42094  mapdordlem2  42101  mapd1o  42112  mapd0  42129  mapdheq2biN  42194  nnproddivdvdsd  42457  primrootspoweq0  42563  aks6d1c1p1  42564  aks6d1c5lem1  42593  sticksstones11  42613  sticksstones22  42625  grpods  42651  unitscyglem2  42653  eqresfnbd  42691  expeq1d  42774  expeqidd  42775  dvdsexpnn  42783  zdivgd  42787  sn-remul0ord  42858  mulgt0b1d  42935  frlmfzowrdb  42967  frlmsnic  43003  evlselvlem  43037  prjspreln0  43060  elrfi  43144  diophrw  43209  eldioph2b  43213  diophin  43222  rexrabdioph  43244  rmxycomplete  43367  coprmdvdsb  43435  jm2.19  43443  jm2.26  43452  jm2.27  43458  limsuc2  43491  dgraa0p  43599  rngunsnply  43619  fiuneneq  43642  unielss  43668  oaabsb  43744  nnoeomeqom  43762  cantnfresb  43774  tfsconcatrn  43792  tfsconcat0b  43796  tfsconcatrev  43798  oadif1lem  43829  oadif1  43830  fzunt  43904  fzuntd  43905  fzunt1d  43906  fzuntgd  43907  pwelg  44009  nzss  44766  dvconstbi  44783  expgrowth  44784  bcc0  44789  axc11next  44855  pm14.24  44881  sbiota1  44883  sbcim2g  44987  sineq0ALT  45385  mapss2  45656  fsneq  45657  fsneqrn  45662  mapssbi  45664  rnmptbd2lem  45699  infnsuprnmpt  45701  rnmptbdlem  45706  xralrple2  45806  infxrunb2  45819  xralrple4  45824  xralrple3  45825  xrralrecnnle  45834  xrralrecnnge  45841  reclt0  45842  supxrunb3  45850  supxrleubrnmpt  45856  xrre4  45861  unb2ltle  45865  rexabslelem  45868  suprleubrnmpt  45872  infxrunb3rnmpt  45878  uzub  45881  supminfrnmpt  45895  iccintsng  45975  sqrlearg  46005  uzinico  46011  preimaiocmnf  46012  limcresiooub  46092  limclr  46105  climeldmeq  46115  limsuppnflem  46160  limsupmnflem  46170  limsupmnfuzlem  46176  limsupre3lem  46182  limsupre3uzlem  46185  liminfreuzlem  46252  dvnmul  46393  dvmptfprodlem  46394  ismbl3  46436  ismbl4  46443  fourierdlem50  46606  fourierdlem89  46645  fourierdlem91  46647  dfsalgen2  46791  sge0repnf  46836  sge0lefi  46848  sge0resplit  46856  sge0fodjrnlem  46866  voliunsge0lem  46922  hspdifhsp  47066  isvonmbl  47088  ovnovollem3  47108  vonvolmbl  47111  pimrecltpos  47158  preimaicomnf  47161  pimrecltneg  47174  issmflem  47177  issmfle  47195  issmfgt  47206  smfaddlem1  47213  issmfge  47220  smfresal  47238  smflimmpt  47260  smfinflem  47267  smflimsuplem7  47276  smflimsupmpt  47279  sigarcol  47314  confun  47403  or2expropbi  47498  fsetsniunop  47513  fcoresf1b  47534  f1cof1b  47541  funfocofob  47542  rexsb  47563  euoreqb  47573  ralbinrald  47586  rlimdmafv  47641  fafv2elrnb  47699  tz6.12c-afv2  47706  dfatbrafv2b  47709  fnbrafv2b  47712  rlimdmafv2  47722  f1oresf1o2  47755  el1fzopredsuc  47790  2ffzoeq  47792  nnmul2b  47795  modlt0b  47833  nndivides2  47848  imasetpreimafvbijlemfo  47881  iccpartiun  47910  ichnfb  47941  ich2exprop  47947  sprsymrelfolem2  47969  paireqne  47987  prprelprb  47993  reupr  47998  nprmmul2  48004  nprmmul3  48005  requad01  48113  requad1  48114  requad2  48115  dfodd6  48129  dfeven4  48130  evensumeven  48199  sbgoldbalt  48273  clnbgrel  48320  dfclnbgr6  48348  dfnbgr6  48349  isubgredg  48358  isuspgrim0  48386  isuspgrim  48388  gricushgr  48409  uhgrimisgrgriclem  48422  clnbgrgrim  48426  grimedg  48427  usgrgrtrirex  48442  uspgrlimlem2  48481  uspgrlim  48484  gpgedgiov  48557  gpgedg2ov  48558  gpgedg2iv  48559  gpgnbgrvtx0  48566  gpgnbgrvtx1  48567  isassintop  48702  uzlidlring  48727  rngcisoALTV  48769  ringcisoALTV  48803  domnmsuppn0  48861  lindslininds  48956  snlindsntor  48963  isldepslvec2  48977  affinecomb1  49194  prelrrx2b  49206  rrx2plord2  49214  eenglngeehlnm  49231  rrx2vlinest  49233  line2xlem  49245  line2x  49246  line2y  49247  itsclc0xyqsolb  49262  itsclquadb  49268  mpbiran3d  49288  opnneieqv  49402  iscnrm3lem2  49426  fullthinc2  49942  thincciso  49944