Theorem mpbir2and 709

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses

Ref	Expression
mpbir2and.1	⊢ (𝜑 → 𝜒)
mpbir2and.2	⊢ (𝜑 → 𝜃)
mpbir2and.3	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbir2and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir2and

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir2and.2	. . 3 ⊢ (𝜑 → 𝜃)
3	1, 2	jca 510	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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  df-an 395

This theorem is referenced by:  elpreimad  7059  fveqressseq  7080  fmptsng  7167  fmptsnd  7168  fnprb  7211  fntpb  7212  fpr3g  8272  frrlem4  8276  1ellim  8500  isfsuppd  9368  fdmfifsupp  9375  fczfsuppd  9383  fsuppmptif  9396  fsuppco2  9400  fsuppcor  9401  dffi3  9428  suppr  9468  infpr  9500  ordtypelem7  9521  cantnf0  9672  cantnfp1lem1  9675  cantnfp1lem2  9676  cantnfp1lem3  9677  cantnflem1a  9682  cantnflem1d  9685  cantnflem1  9686  cantnf  9690  rankpwi  9820  carduni  9978  fin23lem32  10341  fpwwe2lem5  10632  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  inttsk  10771  grutsk1  10818  add20  11730  supaddc  12185  supadd  12186  supmul  12190  suprzcl  12646  uzid  12841  uzwo3  12931  rpnnen1lem5  12969  xrletrid  13138  xrre  13152  xrre3  13154  xleadd1a  13236  xlemul1a  13271  elioc2  13391  elico2  13392  elicc2  13393  elfz1eq  13516  fzadd2  13540  fznatpl1  13559  elfz1uz  13575  nn0fz0  13603  fzctr  13617  fzo1fzo0n0  13687  fzoaddel  13689  elincfzoext  13694  flid  13777  flval3  13784  fladdz  13794  fldiv  13829  modid  13865  hashf1lem1  14419  hashf1lem1OLD  14420  pfxccatin12d  14699  repswpfx  14739  2cshw  14767  pfx2  14902  wwlktovf1  14912  sqeqd  15117  01sqrexlem7  15199  max0add  15261  abs2difabs  15285  rddif  15291  fzomaxdiflem  15293  rexico  15304  icodiamlt  15386  limsupgre  15429  rlim3  15446  icco1  15488  rlimclim  15494  rlimuni  15498  rlimresb  15513  isercolllem2  15616  isercolllem3  15617  isercoll  15618  caucvgrlem  15623  caurcvgr  15624  iseraltlem3  15634  fsum00  15748  o1fsum  15763  bitsfzolem  16379  bitsfzo  16380  bitsmod  16381  bitscmp  16383  gcd0id  16464  gcdneg  16467  bezoutlem4  16488  nn0seqcvgd  16511  lcmneg  16544  lcmfunsnlem2lem2  16580  qredeq  16598  prmind2  16626  eulerthlem2  16719  pcpremul  16780  pcidlem  16809  pcgcd1  16814  fldivp1  16834  pcfaclem  16835  4sqlem17  16898  vdwlem1  16918  vdwlem6  16923  vdwlem12  16929  vdwlem13  16930  0ram  16957  ram0  16959  ramub1lem1  16963  invco  17722  sectmon  17733  monsect  17734  invid  17738  ssctr  17776  ssceq  17777  0ssc  17791  0subcat  17792  catsubcat  17793  issubc3  17803  fullsubc  17804  funcinv  17827  fthmon  17882  fuccocl  17921  fucidcl  17922  invfuc  17931  2initoinv  17964  2termoinv  17971  elhomai  17987  setcmon  18041  setcepi  18042  catcisolem  18064  curf2cl  18188  yonedalem4c  18234  yonedalem3  18237  yoniso  18242  lublecl  18318  isacs3lem  18499  tsrdir  18561  rabsubmgmd  18629  submgmid  18631  subsubmgm  18635  mgmhmima  18640  mgmhmeql  18641  mnd1  18701  sgrp2nmndlem4  18845  sgrp2nmndlem5  18846  0subg  19067  nmznsg  19084  ghmpreima  19152  ghmeql  19153  ghmnsgpreima  19155  kerf1ghm  19161  cntzsgrpcl  19239  cntzsubm  19243  cntzsubg  19244  cntzmhm  19246  symgextfo  19331  symgfixf1  19346  symgfixfolem1  19347  odlem2  19448  finodsubmsubg  19476  gexlem2  19491  gexcl2  19498  sylow1lem5  19511  subgslw  19525  slwhash  19533  fislw  19534  sylow3lem1  19536  lsmsubg  19563  efgredlemd  19653  efgredlem  19656  efgcpbllemb  19664  frgpuplem  19681  cyggeninv  19792  iscygd  19796  iscygodd  19797  gsumzadd  19831  gsumconst  19843  gsumpt  19871  gsum2dlem2  19880  gsum2d  19881  gsum2d2lem  19882  dprdfcntz  19926  eldprdi  19929  subgdmdprd  19945  subgdprd  19946  dprdpr  19961  ablfac1c  19982  ablfac1eu  19984  ablfaclem3  19998  ring1  20198  subrngint  20448  rhmimasubrng  20454  cntzsubrng  20455  rhmeql  20493  rhmima  20494  cntzsubr  20496  issubdrg  20544  imadrhmcl  20556  isabvd  20571  abvdiv  20588  lsslsp  20770  lmhmima  20802  lmhmpreima  20803  lmhmeql  20810  lsmcl  20838  lspfixed  20886  rnglidlrng  21036  rngqiprngim  21063  rng2idl1cntr  21064  qsssubdrg  21204  gzrngunit  21211  pzriprnglem8  21257  evpmodpmf1o  21368  ocvpj  21491  dsmm0cl  21514  dsmmacl  21515  dsmmsubg  21517  dsmmlss  21518  frlmsplit2  21547  uvcff  21565  lindfrn  21595  f1lindf  21596  lindsss  21598  issubassa  21640  issubassa2  21665  snifpsrbag  21694  psrbaglesupp  21696  psrbaglesuppOLD  21697  psrbaglecl  21698  psrbagleclOLD  21699  psrbagaddcl  21700  psrbagaddclOLD  21701  psrbagcon  21702  psrbagconOLD  21703  mplsubglem  21777  mpllsslem  21778  mplassa  21800  subrgmpl  21806  mplcoe5  21814  mplbas2  21816  mplind  21850  mpfind  21889  ismhp2  21904  mhpmulcl  21911  mhplss  21917  ply1assa  21942  coe1tmmul2  22018  coe1tmmul  22019  cply1coe0bi  22044  dmatid  22217  dmatsubcl  22220  dmatscmcl  22225  scmatid  22236  scmataddcl  22238  scmatsubcl  22239  scmatmulcl  22240  smatvscl  22246  scmatrhmcl  22250  mat0scmat  22260  mat1scmat  22261  mdet0pr  22314  chmaidscmat  22570  distop  22718  indistopon  22724  ppttop  22730  epttop  22732  mretopd  22816  toponmre  22817  neiss  22833  opnneissb  22838  ssnei2  22840  innei  22849  neiptoptop  22855  ordtcld1  22921  ordtcld2  22922  lmconst  22985  cnpnei  22988  iscncl  22993  cnss1  23000  cnss2  23001  cncnpi  23002  cncnp  23004  cnconst2  23007  cnrest  23009  cnpresti  23012  cnpdis  23017  paste  23018  lmcnp  23028  cnhaus  23078  hauscmp  23131  2ndcomap  23182  1stcelcls  23185  1stccnp  23186  llyrest  23209  nllyrest  23210  llyidm  23212  nllyidm  23213  ssref  23236  reftr  23238  refun0  23239  dissnref  23252  kgentopon  23262  kgenidm  23271  kgencn3  23282  txcld  23327  neitx  23331  tx1cn  23333  tx2cn  23334  ptcld  23337  xkoccn  23343  txcnp  23344  ptcnp  23346  txcnmpt  23348  ptcn  23351  txdis1cn  23359  ptrescn  23363  txkgen  23376  xkoco1cn  23381  xkoco2cn  23382  xkococn  23384  xkoinjcn  23411  qtoptop2  23423  qtopuni  23426  qtopid  23429  qtopkgen  23434  basqtop  23435  tgqtop  23436  qtopss  23439  qtopeu  23440  qtoprest  23441  kqopn  23458  kqcld  23459  kqreglem2  23466  reghmph  23517  ordthmeolem  23525  qtopf1  23540  opnfbas  23566  isfil2  23580  fbasweak  23589  fsubbas  23591  filconn  23607  fbasrn  23608  rnelfmlem  23676  flimss2  23696  flimss1  23697  hausflim  23705  flimclslem  23708  flimsncls  23710  cnpflfi  23723  flfcnp2  23731  fclsfnflim  23751  cnextfvval  23789  cnextfres1  23792  symgtgp  23830  opnsubg  23832  ghmcnp  23839  qustgpopn  23844  qustgplem  23845  qustgphaus  23847  tsmsfbas  23852  ustfilxp  23937  utoptop  23959  utopbas  23960  restutopopn  23963  iducn  24008  cstucnd  24009  ucncn  24010  fmucnd  24017  cfilufg  24018  trcfilu  24019  cfiluweak  24020  neipcfilu  24021  psmetres2  24040  isxmetd  24052  xmetpsmet  24074  imasf1oxmet  24101  xblss2ps  24127  xblss2  24128  xblcntrps  24136  xblcntr  24137  blcld  24234  metustfbas  24286  cfilucfil  24288  restmetu  24299  ngptgp  24365  tngngpd  24390  nrmtngnrm  24395  tngnrg  24411  nlmvscn  24424  nrginvrcn  24429  nmo0  24472  nmoeq0  24473  nmoid  24479  nghmcn  24482  0nmhm  24492  blcvx  24534  iccntr  24557  xrge0tsms  24570  xmetdcn2  24573  metdstri  24587  metdscn  24592  rescncf  24637  cncfco  24647  oprpiece1res2  24697  cnheibor  24701  cnllycmp  24702  bndth  24704  ishtpyd  24721  isphtpyd  24732  pcoval2  24763  nmhmcn  24867  ipcn  24994  lmnn  25011  cfilss  25018  iscfil3  25021  cfilfcls  25022  cmetcaulem  25036  iscmet3lem2  25040  cfilres  25044  lmcau  25061  flimcfil  25062  cncmet  25070  rlmbn  25109  minveclem3b  25176  pjthlem1  25185  pjth2  25188  ivthlem3  25202  ovolssnul  25236  ovolctb  25239  ovoliunnul  25256  ovolsca  25264  ovolicopnf  25273  voliunlem2  25300  volsup  25305  dyadmaxlem  25346  vitalilem5  25361  mbfres  25393  mbfss  25395  mbfmulc2re  25397  mbfadd  25410  mbfmulc2  25412  mbflim  25417  i1faddlem  25442  i1fmullem  25443  mbfmul  25476  itg2mulc  25497  itg2cnlem1  25511  ibl0  25536  iblposlem  25541  itgreval  25546  iblneg  25552  iblss  25554  iblss2  25555  itgle  25559  iblconst  25567  iblabs  25578  iblabsr  25579  iblmulc2  25580  bddmulibl  25588  limciun  25643  limcun  25644  dvres2lem  25659  dvidlem  25664  dvcnp2  25669  dvcnp2OLD  25670  dvcn  25671  cpnres  25687  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  dvcjbr  25701  dvrec  25707  dvcnvlem  25728  dvferm  25740  dvlip2  25747  dveq0  25752  dv11cn  25753  dvivthlem1  25760  lhop1  25766  lhop2  25767  lhop  25768  dvcnvre  25771  dvfsumlem3  25780  dvfsumlem4  25781  dvfsumrlim  25783  dvfsum2  25786  ftc1a  25789  ftc1lem4  25791  ftc1lem6  25793  ftc1  25794  coe1mul3  25852  deg1addle2  25855  deg1sublt  25863  fta1blem  25921  drnguc1p  25923  ig1prsp  25930  plyco0  25941  plyeq0lem  25959  dgrub  25983  dgreq  25993  dgradd2  26018  dgrmul  26020  dgrcolem2  26024  dgrco  26025  plycpn  26038  plydivlem4  26045  plydiveu  26047  vieta1lem2  26060  vieta1  26061  aalioulem2  26082  aalioulem3  26083  aaliou3lem7  26098  tayl0  26110  ulmcn  26147  ulmdvlem3  26150  psercn  26174  abelth  26189  pilem3  26201  efif1olem1  26287  abslogimle  26318  argregt0  26354  argrege0  26355  logf1o2  26394  cxpsqrtlem  26446  cxpcn3  26492  abscxpbnd  26497  logreclem  26503  ang180lem2  26551  ang180lem3  26552  xrlimcnp  26709  harmonicbnd4  26751  fsumharmonic  26752  lgamgulmlem5  26773  lgambdd  26777  basellem4  26824  dvdsppwf1o  26926  dvdsflf1o  26927  fsumfldivdiaglem  26929  chpeq0  26947  chteq0  26948  chtub  26951  chpub  26959  dchrelbasd  26978  dchrmulcl  26988  dchrinv  27000  bposlem1  27023  bposlem2  27024  lgsdirprm  27070  lgsqrlem2  27086  lgsqrlem3  27087  lgsdchr  27094  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgsquadlem1  27119  2sqlem8  27165  2sqblem  27170  2sqmod  27175  chebbnd1lem1  27208  dchrisumlem1  27228  dchrisumlem2  27229  dchrisumlem3  27230  dchrisum0fno1  27250  pntrmax  27303  pntpbnd1a  27324  pntibndlem3  27331  pntlemn  27339  pntlemi  27343  pntlem3  27348  pntleml  27350  ostth1  27372  ostth2  27376  ostth3  27377  nosepon  27404  nolesgn2ores  27411  nogesgn1ores  27413  nosupres  27446  nosupbnd1lem2  27448  nosupbnd2lem1  27454  noinfres  27461  noinfbnd1lem2  27463  noinfbnd2lem1  27469  cofcutrtime  27652  ercgrg  28035  motco  28058  cnvmot  28059  legso  28117  mirmot  28193  colopp  28287  hphl  28289  lmicom  28306  lmimid  28312  lmimot  28316  hypcgrlem1  28317  hypcgrlem2  28318  trgcopyeulem  28323  inagswap  28359  inaghl  28363  cgrg3col4  28371  brbtwn2  28430  axlowdimlem3  28469  axlowdimlem16  28482  axcontlem8  28496  fusgrfis  28854  nbgr2vtx1edg  28874  0vtxrgr  29100  0vtxrusgr  29101  ewlkle  29129  wlk1ewlk  29164  uspgr2wlkeq2  29171  wlkp1lem8  29204  trlontrl  29235  pthonpth  29272  pthdlem2  29292  wlklnwwlkln1  29389  wlknewwlksn  29408  wwlksnred  29413  wwlksnredwwlkn0  29417  2trlond  29460  2pthond  29463  elwwlks2ons3im  29475  clwlkclwwlklem2a1  29512  clwlkclwwlkf1  29530  clwwlkel  29566  clwwlkwwlksb  29574  wwlksext2clwwlk  29577  1ewlk  29635  0trlon  29644  0pthon  29647  1pthond  29664  3trlond  29693  3pthond  29695  3spthond  29697  eupthres  29735  2clwwlk2clwwlk  29870  numclwwlk1lem2foa  29874  numclwwlk1lem2f1  29877  nvabs  30192  vacn  30214  nmcvcn  30215  nmblore  30306  0lno  30310  0blo  30312  nmlno0lem  30313  occl  30824  pjhthlem1  30911  pjpjpre  30939  nmopre  31390  nmlnop0iALT  31515  nmophmi  31551  leoprf2  31647  stlesi  31761  disjdifprg  32073  disjun0  32093  fsuppcurry1  32217  fsuppcurry2  32218  fpwrelmap  32225  fzspl  32268  dfmgc2lem  32432  pwrssmgc  32437  xrge0tsmsd  32479  ogrpaddlt  32505  ogrpsublt  32509  psgnfzto1stlem  32529  fzto1st1  32531  evpmid  32577  pnfinf  32599  rmfsupp2  32657  ornglmullt  32695  orngrmullt  32696  orngmullt  32697  ofldlt1  32701  isarchiofld  32705  dvdsruassoi  32763  nsgmgc  32797  drngidl  32825  qsdrngi  32883  deg1addlt  32945  ply1degltdimlem  32995  lbsdiflsp0  32999  fedgmul  33004  fldexttr  33025  fldextid  33026  irngnzply1lem  33043  algextdeglem8  33069  qtopt1  33113  reff  33117  locfinreflem  33118  metideq  33171  metider  33172  pstmxmet  33175  qqhval2lem  33259  qqhcn  33269  qqhucn  33270  pwsiga  33426  prsiga  33427  measle0  33504  mbfmcst  33556  1stmbfm  33557  2ndmbfm  33558  imambfm  33559  cnmbfm  33560  mbfmco  33561  mbfmco2  33562  0elcarsg  33604  carsgclctun  33618  sibfof  33637  oddpwdc  33651  eulerpartlemmf  33672  eulerpartlemgs2  33677  0rrv  33748  ballotlemfc0  33789  ballotlemfcc  33790  signstfveq0  33886  breprexplemc  33942  bnj1452  34361  usgrgt2cycl  34419  acycgr1v  34438  derangen  34461  subfacval3  34478  cvmseu  34565  cvmliftmolem2  34571  cvmliftlem7  34580  cvmliftlem15  34587  cvmlift2lem9a  34592  cvmlift2lem9  34600  cvmlift2lem10  34601  cvmlift2lem11  34602  cvmlift2lem12  34603  cvmlift3lem6  34613  cvmlift3lem8  34615  ex-sategoelel  34710  ex-sategoelelomsuc  34715  mclsppslem  34872  mclspps  34873  wsuclem  35101  fness  35537  fnetr  35539  fnessref  35545  refssfne  35546  neibastop1  35547  neibastop2  35549  tailfb  35565  filnetlem3  35568  bj-finsumval0  36469  bj-rvecvec  36483  dfgcd3  36508  lindsadd  36784  poimirlem13  36804  poimirlem15  36806  poimirlem24  36815  poimirlem28  36819  mblfinlem2  36829  ovoliunnfl  36833  volsupnfl  36836  mbfresfi  36837  iblabsnc  36855  iblmulc2nc  36856  ftc1cnnclem  36862  ftc1cnnc  36863  ftc1anc  36872  sdclem2  36913  metf1o  36926  ismtyhmeolem  36975  ismtyres  36979  heibor1lem  36980  bfplem2  36994  bfp  36995  rrncmslem  37003  iccbnd  37011  icccmpALT  37012  rngogrphom  37142  rngoisoco  37153  keridl  37203  lsmcv2  38202  lsatcv0  38204  lcvexchlem4  38210  lcvexchlem5  38211  l1cvpat  38227  lfl0f  38242  lfladdcl  38244  lflnegcl  38248  lkrlss  38268  eqlkr  38272  lkrlsp  38275  lkrlsp2  38276  lshpkrcl  38289  lkrin  38337  1cvrjat  38649  llni  38682  llnle  38692  lplni  38706  lplnle  38714  llncvrlpln2  38731  2atmat  38735  lvoli  38749  lplncvrlvol2  38789  elpaddri  38976  paddclN  39016  pclclN  39065  pclfinN  39074  0psubclN  39117  1psubclN  39118  atpsubclN  39119  pmapsubclN  39120  osumclN  39141  pexmidN  39143  pexmidlem6N  39149  lhp2lt  39175  lautcnv  39264  idlaut  39270  lautco  39271  idldil  39288  ldilcnv  39289  ldilco  39290  ltrncnv  39320  idltrn  39324  cdleme16d  39455  cdleme50laut  39721  cdleme50ldil  39722  cdleme50ltrn  39731  ltrnco  39893  dian0  40213  dia0eldmN  40214  dia1eldmN  40215  dialss  40220  diaintclN  40232  docaclN  40298  doca2N  40300  djajN  40311  dibintclN  40341  diblss  40344  dicvaddcl  40364  dicvscacl  40365  dicn0  40366  cdlemn11a  40381  dihord2cN  40395  dihord11b  40396  dihord6apre  40430  dihmeetlem1N  40464  dihglblem5apreN  40465  dihpN  40510  dihjatcclem4  40595  dochkr1  40652  islpoldN  40658  lcfrlem31  40747  mapdpglem18  40863  mapdheq2  40903  mapdheq4  40906  mapdh6aN  40909  hdmap1l6a  40983  hdmap14lem4a  41045  lcmineqlem4  41203  frlmfzoccat  41385  drnginvmuld  41405  psrbagres  41417  evlselvlem  41460  evlselv  41461  fsuppind  41464  fsuppssind  41467  prjspvs  41654  irrapxlem4  41865  pell1234qrdich  41901  pell1qr1  41911  pell14qrgap  41915  pellqrexplicit  41917  rmspecfund  41949  fzmaxdif  42022  acongeq  42024  jm2.23  42037  jm3.1  42061  lmhmlnmsplit  42131  hbt  42174  dgrsub2  42179  proot1ex  42245  cantnfub  42373  cantnfresb  42376  cantnf2  42377  tfsconcatfv2  42392  tfsconcatrn  42394  tfsconcatb0  42396  naddcnff  42414  naddcnffo  42416  naddcnfid1  42419  naddcnfid2  42420  clublem  42663  dftrcl3  42773  mnugrud  43345  hashnzfz2  43382  dvconstbi  43395  ubelsupr  44006  restopn3  44146  wessf1ornlem  44182  lefldiveq  44300  iccintsng  44534  climsuse  44622  mullimc  44630  limcdm0  44632  limccog  44634  mullimcf  44637  constlimc  44638  idlimc  44640  limcperiod  44642  limsupre  44655  limcleqr  44658  neglimc  44661  addlimc  44662  0ellimcdiv  44663  xlimliminflimsup  44876  cncfshift  44888  cncfperiod  44893  cncfuni  44900  icccncfext  44901  cncfiooicclem1  44907  fperdvper  44933  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  mbfres2cn  44972  iblsplit  44980  stoweidlem7  45021  stoweidlem13  45027  stoweidlem26  45040  wallispilem3  45081  stirlinglem6  45093  stirlinglem10  45097  dirkercncf  45121  fourierdlem6  45127  fourierdlem11  45132  fourierdlem12  45133  fourierdlem15  45136  fourierdlem26  45147  fourierdlem42  45163  fourierdlem50  45170  fourierdlem51  45171  fourierdlem52  45172  fourierdlem54  45174  fourierdlem62  45182  fourierdlem79  45199  fourierdlem102  45222  fourierdlem114  45234  etransclem23  45271  zgeltp1eq  46315  setsnidel  46343  preimafvsnel  46345  iccpartres  46384  prpair  46467  fpprel2  46707  isassintop  46886  rnghmsscmap2  46959  rnghmsscmap  46960  rnghmsubcsetc  46963  zrzeroorngc  46988  rhmsscmap2  47005  rhmsscmap  47006  rhmsubcsetc  47009  rhmsscrnghm  47012  rhmsubcrngc  47015  srhmsubc  47062  fldhmsubc  47070  rhmsubc  47076  srhmsubcALTV  47080  fldhmsubcALTV  47088  rhmsubcALTV  47094  rmfsupp  47138  mndpfsupp  47140  scmfsupp  47142  mptcfsupp  47144  lcoel0  47196  lincsumcl  47199  lincscmcl  47200  lcoss  47204  lindsrng01  47236  lincreslvec3  47250  lindssnlvec  47254  zgtp1leeq  47289  lubsscl  47680  glbsscl  47681  idmon  47723  idepi  47724  thinciso  47767