Theorem impbid 211

Description: Deduce an equivalence from two implications. Deduction associated with impbi 207 and impbii 208. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 210. (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 210	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 52	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bicom1  220  impbid1  224  impcon4bid  226  pm5.74  270  imbi1d  341  pm5.501  366  anbiim  640  impbida  800  dedlem0b  1043  dedlema  1044  dedlemb  1045  albi  1813  alexbii  1828  equequ1  2021  equequ2  2022  spsbbi  2069  elequ1  2106  elequ2  2114  sbequ12  2239  sbft  2257  cbv2w  2329  exsb  2351  dral1v  2362  dral1vOLD  2363  cbv2  2398  cbv2h  2401  ax12b  2419  dral1  2434  dral1ALT  2435  eupickb  2627  eupickbi  2628  2eu2  2644  ralbi  3100  rexbi  3101  ralbida  3264  ceqsalt  3503  rspcebdv  3603  rspceb2dv  3613  ceqex  3638  elabgt  3660  mob2  3710  reu6  3721  sbciegftOLD  3815  sbcg  3855  2reu2  3891  csbiebt  3922  sseq1  4005  ss2abdv  4058  ssdifsym  4264  reupick  4319  reupick2  4321  ab0OLD  4376  uneqdifeq  4493  prnebg  4857  preqsnd  4860  prel12g  4865  iuneqconst  5007  disjeq2  5117  disjeq1  5120  disjss3  5147  reusv2lem2  5399  reusv2lem3  5400  alxfr  5407  ralxfrd  5408  ralxfrd2  5412  copsexgw  5492  copsexg  5493  snopeqop  5508  euotd  5515  poeq2  5594  sotric  5618  sotrieq  5619  freq2  5649  seeq1  5650  seeq2  5651  iss  6039  tz7.7  6395  ordtri1  6402  ordelinel  6470  iotavalOLD  6522  funeq  6573  funssres  6597  f0dom0  6781  tz6.12cOLD  6924  fnbrfvb  6950  ssimaex  6983  fvimacnv  7062  elpreima  7067  feldmfvelcdm  7096  eldmrexrnb  7102  fsn  7144  fnsnb  7175  fmptsng  7177  fmptsnd  7178  fprb  7206  tpres  7213  fconst2g  7215  fconst5  7218  elunirn  7261  f1ocnvfvb  7288  f1prex  7293  foeqcnvco  7309  f1eqcocnv  7310  f1eqcocnvOLD  7311  fliftfun  7320  soisores  7335  isofr  7350  isose  7351  isopo  7354  isoso  7356  f1oiso2  7360  eusvobj2  7412  oprabidw  7451  oprabid  7452  f1opw2  7676  oneqmin  7803  ordsucOLD  7817  ordelsuc  7823  ordsucelsuc  7825  ordunisuc2  7848  limsuc  7853  fndmexb  7914  f1ovv  7961  mptcnfimad  7990  op1steq  8037  opreuopreu  8038  funeldmdif  8052  fvn0elsuppb  8186  extmptsuppeq  8193  rntpos  8245  smoiso2  8390  seqomlem2  8472  oaord  8568  oawordex  8578  oaordex  8579  omord2  8588  om00  8596  oeord  8609  nnaord  8640  nnmord  8653  nnawordex  8658  nnaordex  8659  nnaordex2  8660  eldifsucnn  8685  erexb  8750  swoord1  8756  swoord2  8757  iiner  8808  eceqoveq  8841  mapsnd  8905  ralxpmap  8915  omxpenlem  9098  domtriord  9148  mapxpen  9168  mapunen  9171  ssenen  9176  enfi  9215  nneneq  9234  nndomog  9241  nneneqOLD  9246  nndomogOLD  9251  onomeneq  9253  onomeneqOLD  9254  en1eqsnbi  9301  fodomfib  9351  f1opwfi  9381  fsuppunbi  9413  elfiun  9454  suplub2  9485  ordiso2  9539  ordiso  9540  oieu  9563  brwdom2  9597  brwdom3  9606  cantnflem1  9713  ttrclselem2  9750  cardidm  9983  carddom2  10001  pm54.43  10025  pr2neOLD  10029  acnen  10077  acnen2  10079  alephord  10099  alephinit  10119  dfac5  10152  infdif2  10234  fictb  10269  coflim  10285  fincssdom  10347  fin23lem25  10348  isf32lem9  10385  isf34lem4  10401  fin1a2lem11  10434  axdc3lem2  10475  ficard  10589  fpwwe2lem11  10665  fpwwe2  10667  indpi  10931  nqereq  10959  1idpr  11053  ltapr  11069  leltne  11334  ltlen  11346  ltadd2  11349  addlsub  11661  addid0  11664  ltord1  11771  mul0or  11885  ldiv  12079  ltmul1  12095  mulge0b  12115  lt2msq  12130  negfi  12194  nnsub  12287  nn0sub  12553  zrevaddcl  12638  zltp1le  12643  zdiv  12663  nneo  12677  zeo2  12680  zmax  12960  zbtwnre  12961  qrevaddcl  12986  xrlttri  13151  xrleltne  13157  xralrple  13217  xltneg  13229  xleadd1  13267  xlemul1  13302  supxrunb1  13331  supxrunb2  13332  ioo0  13382  iccid  13402  ico0  13403  ioc0  13404  icc0  13405  difreicc  13494  iccsplit  13495  zltaddlt1le  13515  0fz1  13554  uzsplit  13606  fzm1  13614  fzrevral  13619  ssfzo12bi  13760  elfznelfzob  13771  flge  13803  modid2  13896  modmuladd  13911  ssnn0fi  13983  seqf1olem1  14039  hashen  14339  hashdom  14371  hash2exprb  14465  pr2pwpr  14473  hashtpg  14479  len0nnbi  14534  ccats1pfxeqbi  14725  reuccatpfxs1  14730  repsdf2  14761  scshwfzeqfzo  14810  relexpindlem  15043  shftlem  15048  shftuz  15049  abslt  15294  absle  15295  rexico  15333  cau3lem  15334  reusq0  15442  rlim2lt  15474  rlim3  15475  o1lo1  15514  rlimdm  15528  climshft  15553  o1dif  15607  isercolllem2  15645  isercoll  15647  zsum  15697  fsum  15699  fsum00  15777  incexclem  15815  zprod  15914  fprod  15918  dvdsval2  16234  moddvds  16242  negdvdsb  16250  dvdsnegb  16251  dvdscmulr  16262  dvdsmulcr  16263  dvdssub2  16278  dvdsaddre2b  16284  fzo0dvdseq  16300  mod2eq1n2dvds  16324  ltoddhalfle  16338  sumodd  16365  bitsf1ocnv  16419  sadcaddlem  16432  bitsuz  16449  dvdsgcdb  16521  gcdzeq  16528  dvdssqlem  16537  lcmeq0  16571  lcmdvdsb  16584  lcmfeq0b  16601  lcmf  16604  lcmfdvdsb  16614  coprmgcdb  16620  cncongr  16640  isprm2lem  16652  dvdsprime  16658  dvdsprm  16674  isprm7  16679  coprm  16682  euclemma  16684  rpexp  16694  prmdvdsncoprmbd  16699  prmdiveq  16755  hashgcdlem  16757  odzdvds  16764  pythagtrip  16803  pc2dvds  16848  pcprmpw2  16851  pcprmpw  16852  vdwapun  16943  ramtcl2  16980  firest  17414  mrieqv2d  17619  isacs2  17633  isssc  17803  setciso  18080  posasymb  18311  pleval2  18329  pltval3  18331  lublecllem  18352  joinle  18378  meetle  18392  latdisd  18489  lubun  18507  clatleglb  18510  letsr  18585  intopsn  18614  gsumval2a  18645  frmdss2  18815  isgrpid2  18933  isgrpinv  18950  f1ghm0to0  19199  symg1bas  19345  oddvdsnn0  19499  oddvds  19502  odeq  19505  odeq1  19515  gexdvds  19539  pgpfi  19560  pgpssslw  19569  fislw  19580  sylow3lem2  19583  lsmelvalm  19606  lsmlub  19619  lsmss1b  19621  lsmss2b  19623  efgs1b  19691  cyggenod  19839  cyggexb  19854  dprdfeq0  19979  ablsimpgfind  20067  ringinvnz1ne0  20236  ringinvnzdiv  20237  unitmulclb  20320  dvreq1  20350  isnzr2  20457  0ringnnzr  20462  0ring01eqbi  20469  rngciso  20571  ringciso  20605  drngmul0or  20653  isabvd  20700  issrngd  20741  lssats2  20884  lspsneq0  20896  lsmelval2  20970  lvecvs0or  20996  lspsneq  21010  lspsneu  21011  lidl1el  21122  lidldvgen  21224  rrgeq0  21237  domneq0  21244  pzriprnglem10  21416  pzriprnglem11  21417  znunit  21497  psgndif  21534  ipeq0  21570  ocvsscon  21607  pjdm2  21645  obselocv  21662  islinds4  21769  psdmul  22090  ply1coe1eq  22219  cply1coe0bi  22221  mat1dimelbas  22386  cramer  22606  toponcomb  22844  tgss3  22902  clsval2  22967  isopn3  22983  elcls3  23000  opncldf1  23001  neiint  23021  neips  23030  opnneissb  23031  opnssneib  23032  opnnei  23037  tpnei  23038  opnneiid  23043  restcld  23089  restopnb  23092  tgcn  23169  tgcnp  23170  subbascn  23171  iscnp4  23180  cnpnei  23181  cncls2  23190  cncls  23191  cnntr  23192  lmss  23215  hausnei2  23270  lpcls  23281  ordtt1  23296  cmpsub  23317  tgcmp  23318  1stcelcls  23378  locfincmp  23443  kgencn2  23474  ptpjpre1  23488  upxp  23540  txcn  23543  txlm  23565  tgqtop  23629  kqfvima  23647  isr0  23654  regr1lem2  23657  hmeoopn  23683  hmeocld  23684  ptuncnv  23724  fbunfip  23786  fgss2  23791  ufilb  23823  ufprim  23826  trufil  23827  cfinufil  23845  ufildr  23848  elfm2  23865  elfm3  23867  rnelfm  23870  fmfnfmlem4  23874  fmco  23878  flimtopon  23887  flimopn  23892  fbflim2  23894  flimrest  23900  flffbas  23912  cnpflf  23918  fclstopon  23929  fclsnei  23936  fclsbas  23938  fclsfnflim  23944  fclscmp  23947  ufilcmp  23949  isfcf  23951  fcfnei  23952  cnpfcf  23958  alexsubb  23963  alexsubALT  23968  cldsubg  24028  tgphaus  24034  tgpt0  24036  tsmsgsum  24056  tsmsres  24061  xbln0  24333  blssexps  24345  blssex  24346  isxms2  24367  prdsbl  24413  neibl  24423  metss  24430  met2ndc  24445  metrest  24446  metcnp3  24462  tngngp3  24586  nmoeq0  24666  xrsxmet  24738  reconn  24757  iccpnfcnv  24882  fgcfil  25212  iscau4  25220  cfilres  25237  iunmbl2  25499  ismbf3d  25596  mbfaddlem  25602  i1faddlem  25635  i1fmullem  25636  ellimc3  25821  dvfsumlem2  25974  tdeglem4  26008  tdeglem4OLD  26009  deg1nn0clb  26039  deg1lt0  26040  dvdsq1p  26110  plypf1  26159  0dgrb  26193  plymul0or  26228  taylthlem2  26322  ulmshft  26339  ulmcaulem  26343  ulmcau  26344  cosord  26478  eff1olem  26495  lognegb  26537  eflogeq  26549  logdivlt  26568  efopn  26605  cxpeq0  26625  cxpeq  26705  angpieqvd  26776  dcubic  26791  asinsinb  26842  acoscosb  26843  atantanb  26869  rlimcnp  26910  isppw  27059  isppw2  27060  vmappw  27061  isnsqf  27080  ppieq0  27121  fsumdvdsdiag  27129  dvdsppwf1o  27131  fsumfldivdiag  27135  chpeq0  27154  chteq0  27155  dchrptlem1  27210  lgsdir2lem4  27274  lgsne0  27281  lgsqr  27297  lgsdchrval  27300  gausslemma2dlem1a  27311  lgsquadlem1  27326  m1lgs  27334  2sqreultblem  27394  2sqreunnltblem  27397  nodenselem8  27637  sltlend  27717  oldlim  27826  sltlpss  27846  sleadd1  27919  sltneg  27970  muls0ord  28098  absslt  28156  iscgrglt  28331  brbtwn  28723  brcgr  28724  brbtwn2  28729  axcontlem7  28794  uhgr0vb  28898  edglnl  28969  ausgrusgrb  28991  ushgredgedg  29055  ushgredgedgloop  29057  usgr0vb  29063  usgr1v  29082  nbupgr  29170  nbumgrvtx  29172  nbuhgr2vtx1edgb  29178  edgusgrnbfin  29199  nb3grprlem1  29206  uvtxnbvtxm1  29232  cusgrfilem2  29283  uhgr0edg0rgrb  29401  cusgrm1rusgr  29409  spthonepeq  29579  usgr2pth  29591  wlkiswwlks  29700  wlkiswwlkupgr  29702  wlklnwwlkn  29708  wlklnwwlknupgr  29710  wwlksnextbi  29718  wwlksnredwwlkn0  29720  wwlksnextwrd  29721  wwlksnextprop  29736  umgrwwlks2on  29781  elwspths2on  29784  usgr2wspthons3  29788  elwwlks2  29790  elwspths2spth  29791  clwlkclwwlklem3  29824  loopclwwlkn1b  29865  clwwlknon1sn  29923  clwwlknonwwlknonb  29929  umgr3v3e3cycl  30007  eupth2lem3lem4  30054  frgr0v  30085  frgr3vlem2  30097  2clwwlk2clwwlk  30173  wlkl0  30190  grpoinvf  30355  nvmul0or  30473  nvz  30492  diporthcom  30539  ubthlem3  30695  hvmul0or  30848  his6  30922  hial0  30925  hial02  30926  orthcom  30931  normgt0  30950  ocin  31119  occon3  31120  shsel3  31138  shlub  31237  chssoc  31319  h1de2bi  31377  spansncol  31391  elspansn4  31396  spansnss2  31398  sumspansn  31472  lnopcnbd  31859  lnfncnbd  31880  riesz1  31888  elpjrn  32013  cvcon3  32107  dmdmd  32123  dmdbr3  32128  dmdbr4  32129  dmdbr5  32131  mdslmd1i  32152  atcveq0  32171  chcv1  32178  atssma  32201  atcv0eq  32202  atcv1  32203  bian1d  32270  disjeq1f  32376  br8d  32413  fpwrelmap  32528  xaddeq0  32536  eliccelico  32558  elicoelioo  32559  isarchiofld  33045  unitdivcld  33502  xrge0iifcnv  33534  lmxrge0  33553  indf1ofs  33645  eulerpartlemgh  33998  dstfrvunirn  34094  fnrelpredd  34712  loop1cycl  34747  cusgracyclt3v  34766  cvmliftmolem2  34892  cvmlift2lem12  34924  satfvsucsuc  34975  satfdm  34979  fmlasuc  34996  satffunlem1lem2  35013  satffunlem2lem2  35016  mthmb  35191  climuzcnv  35275  br8  35350  br6  35351  br4  35352  funbreq  35365  axextbdist  35396  dfrdg4  35547  cgrcom  35586  cgrcoml  35592  cgrdegen  35600  btwncom  35610  brsegle  35704  brsegle2  35705  colinbtwnle  35714  btwnoutside  35721  broutsideof3  35722  outsidele  35728  lineunray  35743  lineelsb2  35744  elhf2  35771  elicc3  35801  nn0prpwlem  35806  opnbnd  35809  cldbnd  35810  opnregcld  35814  cldregopn  35815  fnessref  35841  refssfne  35842  neibastop2  35845  fnemeet2  35851  fnejoin2  35853  fgmin  35854  ontgval  35915  ordtop  35920  ordcmp  35931  nndivsub  35941  bj-19.21t  36246  bj-19.23t  36247  bj-19.42t  36250  bj-sbft  36252  bj-cbv2hv  36274  bj-equsal1t  36299  bj-19.21t0  36307  bj-ceqsalt0  36362  bj-ceqsalt1  36363  bj-xpnzexb  36440  bj-idreseq  36641  bj-imdiridlem  36664  bj-finsumval0  36764  bj-fvimacnv0  36765  bj-isrvec2  36779  bj-bary1  36791  dfgcd3  36803  isbasisrelowllem1  36834  isbasisrelowllem2  36835  finxpsuclem  36876  wl-lem-exsb  37033  wl-mo3t  37043  wl-ax11-lem1  37052  matunitlindf  37091  poimirlem6  37099  poimirlem7  37100  poimirlem16  37109  poimirlem19  37112  poimirlem22  37115  poimirlem23  37116  poimirlem24  37117  cnambfre  37141  itg2addnc  37147  brabg2  37190  istotbnd3  37244  sstotbnd2  37247  sstotbnd  37248  sstotbnd3  37249  ssbnd  37261  ismtybnd  37280  reheibor  37312  grpoeqdivid  37354  grpokerinj  37366  rngosn3  37397  rngoueqz  37413  1idl  37499  0rngo  37500  divrngidl  37501  igenval2  37539  ispridlc  37543  isdmn3  37547  relcnveq3  37793  iss2  37816  elrelscnveq3  37963  funALTVeq  38172  disjeq  38206  prtlem10  38337  prter2  38353  dral1-o  38376  lshpinN  38461  lsatcveq0  38504  lsatcv0eq  38519  lsatcv1  38520  islshpcv  38525  lkr0f  38566  lkrshp4  38580  lshpkrlem1  38582  lshpset2N  38591  lfl1dim  38593  lfl1dim2N  38594  lub0N  38661  glb0N  38665  oplecon3b  38672  cmtcomN  38721  cmtbr3N  38726  cmtbr4N  38727  cvrnbtwn2  38747  cvrnbtwn3  38748  cvrcon3b  38749  cvrnbtwn4  38751  cvrcmp  38755  atcvreq0  38786  atnle  38789  atlatle  38792  cvlexchb1  38802  cvlcvr1  38811  hlrelat2  38876  exatleN  38877  cvrval3  38886  cvrval4N  38887  cvrexch  38893  atcvr0eq  38899  lnnat  38900  atcvrj0  38901  atcvrj2b  38905  atltcvr  38908  atbtwn  38919  ps-1  38950  3at  38963  islln2a  38990  llncmp  38995  islpln2a  39021  lplncmp  39035  islvol2aN  39065  4at  39086  lvolcmp  39090  pmaple  39234  lncmp  39256  paddss  39318  llnexchb2lem  39341  2polcon4bN  39391  ispsubcl2N  39420  lhpat3  39519  lautcvr  39565  ltrnid  39608  trlval2  39636  trlatn0  39645  ltrnideq  39648  trlnidatb  39650  cdlemeg49lebilem  40012  trlord  40042  cdlemg1a  40043  cdlemg1cex  40061  tendoid0  40298  dva1dim  40458  cdlemm10N  40591  diarnN  40602  cdlemn  40685  dihlspsnssN  40805  dihatexv  40811  dochkrshp  40859  dochkrshp4  40862  djhlsmcl  40887  lcfl6  40973  lcfl8  40975  lcfrvalsnN  41014  lcfrlem9  41023  mapdval2N  41103  mapdordlem2  41110  mapd1o  41121  mapd0  41138  mapdheq2biN  41203  nnproddivdvdsd  41471  primrootspoweq0  41577  aks6d1c1p1  41578  aks6d1c5lem1  41607  sticksstones11  41628  sticksstones22  41640  fnsnbt  41721  eqresfnbd  41723  frlmfzowrdb  41744  frlmsnic  41770  evlselvlem  41819  dvdsexpnn  41900  zdivgd  41907  mulgt0b2d  42015  prjspreln0  42033  elrfi  42114  diophrw  42179  eldioph2b  42183  diophin  42192  rexrabdioph  42214  rmxycomplete  42338  coprmdvdsb  42406  jm2.19  42414  jm2.26  42423  jm2.27  42429  limsuc2  42465  dgraa0p  42573  rngunsnply  42597  fiuneneq  42620  unielss  42646  oaabsb  42723  nnoeomeqom  42741  cantnfresb  42753  tfsconcatrn  42771  tfsconcat0b  42775  tfsconcatrev  42777  oadif1lem  42808  oadif1  42809  fzunt  42885  fzuntd  42886  fzunt1d  42887  fzuntgd  42888  pwelg  42990  nzss  43754  dvconstbi  43771  expgrowth  43772  bcc0  43777  axc11next  43843  pm14.24  43869  sbiota1  43871  sbcim2g  43977  sineq0ALT  44376  pwssfi  44409  mapss2  44578  fsneq  44579  fsneqrn  44584  mapssbi  44586  ssmapsn  44589  rnmptbd2lem  44624  infnsuprnmpt  44626  rnmptbdlem  44631  xralrple2  44736  infxrunb2  44750  xralrple4  44755  xralrple3  44756  xrralrecnnle  44765  xrralrecnnge  44772  reclt0  44773  supxrunb3  44781  supxrleubrnmpt  44788  xrre4  44793  unb2ltle  44797  rexabslelem  44800  suprleubrnmpt  44804  infxrunb3rnmpt  44810  uzub  44813  supminfrnmpt  44827  iccintsng  44908  sqrlearg  44938  uzinico  44945  preimaiocmnf  44946  limcresiooub  45030  limclr  45043  climeldmeq  45053  limsuppnflem  45098  limsupmnflem  45108  limsupmnfuzlem  45114  limsupre3lem  45120  limsupre3uzlem  45123  liminfreuzlem  45190  dvnmul  45331  dvmptfprodlem  45332  ismbl3  45374  ismbl4  45381  fourierdlem50  45544  fourierdlem89  45583  fourierdlem91  45585  dfsalgen2  45729  sge0repnf  45774  sge0lefi  45786  sge0resplit  45794  sge0fodjrnlem  45804  voliunsge0lem  45860  hspdifhsp  46004  isvonmbl  46026  ovnovollem3  46046  vonvolmbl  46049  pimrecltpos  46096  preimaicomnf  46099  pimrecltneg  46112  issmflem  46115  issmfle  46133  issmfgt  46144  smfaddlem1  46151  issmfge  46158  smfresal  46176  smflimmpt  46198  smfinflem  46205  smflimsuplem7  46214  smflimsupmpt  46217  sigarcol  46252  confun  46321  or2expropbi  46416  fsetsniunop  46431  fcoresf1b  46452  f1cof1b  46457  funfocofob  46458  rexsb  46479  euoreqb  46489  ralbinrald  46502  rlimdmafv  46557  fafv2elrnb  46615  tz6.12c-afv2  46622  dfatbrafv2b  46625  fnbrafv2b  46628  rlimdmafv2  46638  f1oresf1o2  46671  el1fzopredsuc  46705  2ffzoeq  46708  imasetpreimafvbijlemfo  46745  iccpartiun  46774  ichnfb  46805  ich2exprop  46811  sprsymrelfolem2  46833  paireqne  46851  prprelprb  46857  reupr  46862  requad01  46961  requad1  46962  requad2  46963  dfodd6  46977  dfeven4  46978  evensumeven  47047  sbgoldbalt  47121  isuspgrim0  47170  isuspgrim  47173  gricushgr  47183  isassintop  47272  uzlidlring  47297  rngcisoALTV  47339  ringcisoALTV  47373  domnmsuppn0  47433  lindslininds  47532  snlindsntor  47539  isldepslvec2  47553  affinecomb1  47775  prelrrx2b  47787  rrx2plord2  47795  eenglngeehlnm  47812  rrx2vlinest  47814  line2xlem  47826  line2x  47827  line2y  47828  itsclc0xyqsolb  47843  itsclquadb  47849  mpbiran3d  47869  opnneieqv  47929  iscnrm3lem2  47953  fullthinc2  48053  thincciso  48055