Theorem mpbir2and 712

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 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 257	1 ⊢ (𝜑 → 𝜓)

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

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 396

This theorem is referenced by:  elpreimad  7062  fveqressseq  7083  fmptsng  7171  fmptsnd  7172  fnprb  7214  fntpb  7215  fpr3g  8284  frrlem4  8288  1ellim  8512  isfsuppd  9382  fdmfifsupp  9390  fczfsuppd  9401  fsuppmptif  9414  fsuppco2  9418  fsuppcor  9419  dffi3  9446  suppr  9486  infpr  9518  ordtypelem7  9539  cantnf0  9690  cantnfp1lem1  9693  cantnfp1lem2  9694  cantnfp1lem3  9695  cantnflem1a  9700  cantnflem1d  9703  cantnflem1  9704  cantnf  9708  rankpwi  9838  carduni  9996  fin23lem32  10359  fpwwe2lem5  10650  fpwwe2lem11  10656  fpwwe2lem12  10657  fpwwe2  10658  inttsk  10789  grutsk1  10836  add20  11748  supaddc  12203  supadd  12204  supmul  12208  suprzcl  12664  uzid  12859  uzwo3  12949  rpnnen1lem5  12987  xrletrid  13158  xrre  13172  xrre3  13174  xleadd1a  13256  xlemul1a  13291  elioc2  13411  elico2  13412  elicc2  13413  elfz1eq  13536  fzadd2  13560  fznatpl1  13579  elfz1uz  13595  nn0fz0  13623  fzctr  13637  fzo1fzo0n0  13707  fzoaddel  13709  elincfzoext  13714  flid  13797  flval3  13804  fladdz  13814  fldiv  13849  modid  13885  hashf1lem1  14439  hashf1lem1OLD  14440  pfxccatin12d  14719  repswpfx  14759  2cshw  14787  pfx2  14922  wwlktovf1  14932  sqeqd  15137  01sqrexlem7  15219  max0add  15281  abs2difabs  15305  rddif  15311  fzomaxdiflem  15313  rexico  15324  icodiamlt  15406  limsupgre  15449  rlim3  15466  icco1  15508  rlimclim  15514  rlimuni  15518  rlimresb  15533  isercolllem2  15636  isercolllem3  15637  isercoll  15638  caucvgrlem  15643  caurcvgr  15644  iseraltlem3  15654  fsum00  15768  o1fsum  15783  bitsfzolem  16400  bitsfzo  16401  bitsmod  16402  bitscmp  16404  gcd0id  16485  gcdneg  16488  bezoutlem4  16509  nn0seqcvgd  16532  lcmneg  16565  lcmfunsnlem2lem2  16601  qredeq  16619  prmind2  16647  eulerthlem2  16742  pcpremul  16803  pcidlem  16832  pcgcd1  16837  fldivp1  16857  pcfaclem  16858  4sqlem17  16921  vdwlem1  16941  vdwlem6  16946  vdwlem12  16952  vdwlem13  16953  0ram  16980  ram0  16982  ramub1lem1  16986  invco  17745  sectmon  17756  monsect  17757  invid  17761  ssctr  17799  ssceq  17800  0ssc  17814  0subcat  17815  catsubcat  17816  issubc3  17826  fullsubc  17827  funcinv  17850  fthmon  17907  fuccocl  17947  fucidcl  17948  invfuc  17957  2initoinv  17990  2termoinv  17997  elhomai  18013  setcmon  18067  setcepi  18068  catcisolem  18090  curf2cl  18214  yonedalem4c  18260  yonedalem3  18263  yoniso  18268  lublecl  18344  isacs3lem  18525  tsrdir  18587  rabsubmgmd  18655  submgmid  18657  subsubmgm  18661  mgmhmima  18666  mgmhmeql  18667  mnd1  18727  sgrp2nmndlem4  18871  sgrp2nmndlem5  18872  0subg  19097  nmznsg  19114  ghmpreima  19183  ghmeql  19184  ghmnsgpreima  19186  kerf1ghm  19192  cntzsgrpcl  19276  cntzsubm  19280  cntzsubg  19281  cntzmhm  19283  symgextfo  19368  symgfixf1  19383  symgfixfolem1  19384  odlem2  19485  finodsubmsubg  19513  gexlem2  19528  gexcl2  19535  sylow1lem5  19548  subgslw  19562  slwhash  19570  fislw  19571  sylow3lem1  19573  lsmsubg  19600  efgredlemd  19690  efgredlem  19693  efgcpbllemb  19701  frgpuplem  19718  cyggeninv  19829  iscygd  19833  iscygodd  19834  gsumzadd  19868  gsumconst  19880  gsumpt  19908  gsum2dlem2  19917  gsum2d  19918  gsum2d2lem  19919  dprdfcntz  19963  eldprdi  19966  subgdmdprd  19982  subgdprd  19983  dprdpr  19998  ablfac1c  20019  ablfac1eu  20021  ablfaclem3  20035  ring1  20235  subrngint  20486  rhmimasubrng  20492  cntzsubrng  20493  rhmeql  20531  rhmima  20532  cntzsubr  20534  rnghmsscmap2  20551  rnghmsscmap  20552  rnghmsubcsetc  20555  zrzeroorngc  20566  rhmsscmap2  20580  rhmsscmap  20581  rhmsubcsetc  20584  rhmsscrnghm  20587  rhmsubcrngc  20590  srhmsubc  20602  rhmsubc  20611  issubdrg  20657  fldhmsubc  20662  imadrhmcl  20674  isabvd  20689  abvdiv  20706  lsslsp  20888  lsslspOLD  20889  lmhmima  20921  lmhmpreima  20922  lmhmeql  20929  lsmcl  20957  lspfixed  21005  rnglidlrng  21131  rngqiprngim  21183  rng2idl1cntr  21184  qsssubdrg  21346  gzrngunit  21353  pzriprnglem8  21401  evpmodpmf1o  21515  ocvpj  21638  dsmm0cl  21661  dsmmacl  21662  dsmmsubg  21664  dsmmlss  21665  frlmsplit2  21694  uvcff  21712  lindfrn  21742  f1lindf  21743  lindsss  21745  issubassa  21787  issubassa2  21812  snifpsrbag  21842  psrbaglesupp  21844  psrbaglesuppOLD  21845  psrbaglecl  21846  psrbagleclOLD  21847  psrbagaddcl  21848  psrbagaddclOLD  21849  psrbagcon  21850  psrbagconOLD  21851  mplsubglem  21928  mpllsslem  21929  mplassa  21951  subrgmpl  21957  mplcoe5  21965  mplbas2  21967  mplind  22001  mpfind  22040  ismhp2  22053  mhpmulcl  22060  mhplss  22066  ply1assa  22105  coe1tmmul2  22182  coe1tmmul  22183  cply1coe0bi  22208  dmatid  22384  dmatsubcl  22387  dmatscmcl  22392  scmatid  22403  scmataddcl  22405  scmatsubcl  22406  scmatmulcl  22407  smatvscl  22413  scmatrhmcl  22417  mat0scmat  22427  mat1scmat  22428  mdet0pr  22481  chmaidscmat  22737  distop  22885  indistopon  22891  ppttop  22897  epttop  22899  mretopd  22983  toponmre  22984  neiss  23000  opnneissb  23005  ssnei2  23007  innei  23016  neiptoptop  23022  ordtcld1  23088  ordtcld2  23089  lmconst  23152  cnpnei  23155  iscncl  23160  cnss1  23167  cnss2  23168  cncnpi  23169  cncnp  23171  cnconst2  23174  cnrest  23176  cnpresti  23179  cnpdis  23184  paste  23185  lmcnp  23195  cnhaus  23245  hauscmp  23298  2ndcomap  23349  1stcelcls  23352  1stccnp  23353  llyrest  23376  nllyrest  23377  llyidm  23379  nllyidm  23380  ssref  23403  reftr  23405  refun0  23406  dissnref  23419  kgentopon  23429  kgenidm  23438  kgencn3  23449  txcld  23494  neitx  23498  tx1cn  23500  tx2cn  23501  ptcld  23504  xkoccn  23510  txcnp  23511  ptcnp  23513  txcnmpt  23515  ptcn  23518  txdis1cn  23526  ptrescn  23530  txkgen  23543  xkoco1cn  23548  xkoco2cn  23549  xkococn  23551  xkoinjcn  23578  qtoptop2  23590  qtopuni  23593  qtopid  23596  qtopkgen  23601  basqtop  23602  tgqtop  23603  qtopss  23606  qtopeu  23607  qtoprest  23608  kqopn  23625  kqcld  23626  kqreglem2  23633  reghmph  23684  ordthmeolem  23692  qtopf1  23707  opnfbas  23733  isfil2  23747  fbasweak  23756  fsubbas  23758  filconn  23774  fbasrn  23775  rnelfmlem  23843  flimss2  23863  flimss1  23864  hausflim  23872  flimclslem  23875  flimsncls  23877  cnpflfi  23890  flfcnp2  23898  fclsfnflim  23918  cnextfvval  23956  cnextfres1  23959  symgtgp  23997  opnsubg  23999  ghmcnp  24006  qustgpopn  24011  qustgplem  24012  qustgphaus  24014  tsmsfbas  24019  ustfilxp  24104  utoptop  24126  utopbas  24127  restutopopn  24130  iducn  24175  cstucnd  24176  ucncn  24177  fmucnd  24184  cfilufg  24185  trcfilu  24186  cfiluweak  24187  neipcfilu  24188  psmetres2  24207  isxmetd  24219  xmetpsmet  24241  imasf1oxmet  24268  xblss2ps  24294  xblss2  24295  xblcntrps  24303  xblcntr  24304  blcld  24401  metustfbas  24453  cfilucfil  24455  restmetu  24466  ngptgp  24532  tngngpd  24557  nrmtngnrm  24562  tngnrg  24578  nlmvscn  24591  nrginvrcn  24596  nmo0  24639  nmoeq0  24640  nmoid  24646  nghmcn  24649  0nmhm  24659  blcvx  24701  iccntr  24724  xrge0tsms  24737  xmetdcn2  24740  metdstri  24754  metdscn  24759  rescncf  24804  cncfco  24814  oprpiece1res2  24864  cnheibor  24868  cnllycmp  24869  bndth  24871  ishtpyd  24888  isphtpyd  24899  pcoval2  24930  nmhmcn  25034  ipcn  25161  lmnn  25178  cfilss  25185  iscfil3  25188  cfilfcls  25189  cmetcaulem  25203  iscmet3lem2  25207  cfilres  25211  lmcau  25228  flimcfil  25229  cncmet  25237  rlmbn  25276  minveclem3b  25343  pjthlem1  25352  pjth2  25355  ivthlem3  25369  ovolssnul  25403  ovolctb  25406  ovoliunnul  25423  ovolsca  25431  ovolicopnf  25440  voliunlem2  25467  volsup  25472  dyadmaxlem  25513  vitalilem5  25528  mbfres  25560  mbfss  25562  mbfmulc2re  25564  mbfadd  25577  mbfmulc2  25579  mbflim  25584  i1faddlem  25609  i1fmullem  25610  mbfmul  25643  itg2mulc  25664  itg2cnlem1  25678  ibl0  25703  iblposlem  25708  itgreval  25713  iblneg  25719  iblss  25721  iblss2  25722  itgle  25726  iblconst  25734  iblabs  25745  iblabsr  25746  iblmulc2  25747  bddmulibl  25755  limciun  25810  limcun  25811  dvres2lem  25826  dvidlem  25831  dvcnp2  25836  dvcnp2OLD  25837  dvcn  25838  cpnres  25854  dvaddbr  25855  dvmulbr  25856  dvmulbrOLD  25857  dvcobr  25864  dvcobrOLD  25865  dvcjbr  25868  dvrec  25874  dvcnvlem  25895  dvferm  25907  dvlip2  25915  dveq0  25920  dv11cn  25921  dvivthlem1  25928  lhop1  25934  lhop2  25935  lhop  25936  dvcnvre  25939  dvfsumlem3  25950  dvfsumlem4  25951  dvfsumrlim  25953  dvfsum2  25956  ftc1a  25959  ftc1lem4  25961  ftc1lem6  25963  ftc1  25964  coe1mul3  26022  deg1addle2  26025  deg1sublt  26033  fta1blem  26092  drnguc1p  26095  ig1prsp  26102  plyco0  26113  plyeq0lem  26131  dgrub  26155  dgreq  26165  dgradd2  26190  dgrmul  26192  dgrcolem2  26196  dgrco  26197  plycpn  26211  plydivlem4  26218  plydiveu  26220  vieta1lem2  26233  vieta1  26234  aalioulem2  26255  aalioulem3  26256  aaliou3lem7  26271  tayl0  26283  ulmcn  26322  ulmdvlem3  26325  psercn  26350  abelth  26365  pilem3  26377  efif1olem1  26463  abslogimle  26494  argregt0  26531  argrege0  26532  logf1o2  26571  cxpsqrtlem  26623  cxpcn3  26670  abscxpbnd  26675  logreclem  26681  ang180lem2  26729  ang180lem3  26730  xrlimcnp  26887  harmonicbnd4  26930  fsumharmonic  26931  lgamgulmlem5  26952  lgambdd  26956  basellem4  27003  dvdsppwf1o  27105  dvdsflf1o  27106  fsumfldivdiaglem  27108  chpeq0  27128  chteq0  27129  chtub  27132  chpub  27140  dchrelbasd  27159  dchrmulcl  27169  dchrinv  27181  bposlem1  27204  bposlem2  27205  lgsdirprm  27251  lgsqrlem2  27267  lgsqrlem3  27268  lgsdchr  27275  lgseisenlem1  27295  lgseisenlem2  27296  lgseisenlem3  27297  lgsquadlem1  27300  2sqlem8  27346  2sqblem  27351  2sqmod  27356  chebbnd1lem1  27389  dchrisumlem1  27409  dchrisumlem2  27410  dchrisumlem3  27411  dchrisum0fno1  27431  pntrmax  27484  pntpbnd1a  27505  pntibndlem3  27512  pntlemn  27520  pntlemi  27524  pntlem3  27529  pntleml  27531  ostth1  27553  ostth2  27557  ostth3  27558  nosepon  27585  nolesgn2ores  27592  nogesgn1ores  27594  nosupres  27627  nosupbnd1lem2  27629  nosupbnd2lem1  27635  noinfres  27642  noinfbnd1lem2  27644  noinfbnd2lem1  27650  cofcutrtime  27834  divmuldivsd  28117  nnsgt0  28194  ercgrg  28308  motco  28331  cnvmot  28332  legso  28390  mirmot  28466  colopp  28560  hphl  28562  lmicom  28579  lmimid  28585  lmimot  28589  hypcgrlem1  28590  hypcgrlem2  28591  trgcopyeulem  28596  inagswap  28632  inaghl  28636  cgrg3col4  28644  brbtwn2  28703  axlowdimlem3  28742  axlowdimlem16  28755  axcontlem8  28769  fusgrfis  29130  nbgr2vtx1edg  29150  0vtxrgr  29377  0vtxrusgr  29378  ewlkle  29406  wlk1ewlk  29441  uspgr2wlkeq2  29448  wlkp1lem8  29481  trlontrl  29512  pthonpth  29549  pthdlem2  29569  wlklnwwlkln1  29666  wlknewwlksn  29685  wwlksnred  29690  wwlksnredwwlkn0  29694  2trlond  29737  2pthond  29740  elwwlks2ons3im  29752  clwlkclwwlklem2a1  29789  clwlkclwwlkf1  29807  clwwlkel  29843  clwwlkwwlksb  29851  wwlksext2clwwlk  29854  1ewlk  29912  0trlon  29921  0pthon  29924  1pthond  29941  3trlond  29970  3pthond  29972  3spthond  29974  eupthres  30012  2clwwlk2clwwlk  30147  numclwwlk1lem2foa  30151  numclwwlk1lem2f1  30154  nvabs  30469  vacn  30491  nmcvcn  30492  nmblore  30583  0lno  30587  0blo  30589  nmlno0lem  30590  occl  31101  pjhthlem1  31188  pjpjpre  31216  nmopre  31667  nmlnop0iALT  31792  nmophmi  31828  leoprf2  31924  stlesi  32038  disjdifprg  32350  disjun0  32370  fsuppcurry1  32491  fsuppcurry2  32492  fpwrelmap  32499  fzspl  32542  dfmgc2lem  32704  pwrssmgc  32709  xrge0tsmsd  32749  ogrpaddlt  32775  ogrpsublt  32779  psgnfzto1stlem  32799  fzto1st1  32801  evpmid  32847  pnfinf  32869  rmfsupp2  32923  ornglmullt  32962  orngrmullt  32963  orngmullt  32964  ofldlt1  32968  isarchiofld  32972  dvdsruassoi  33028  nsgmgc  33062  drngidl  33084  qsdrngi  33142  deg1addlt  33202  ply1degltdimlem  33252  lbsdiflsp0  33256  fedgmul  33261  fldexttr  33282  fldextid  33283  irngnzply1lem  33300  irredminply  33320  algextdeglem8  33328  qtopt1  33372  reff  33376  locfinreflem  33377  metideq  33430  metider  33431  pstmxmet  33434  qqhval2lem  33518  qqhcn  33528  qqhucn  33529  pwsiga  33685  prsiga  33686  measle0  33763  mbfmcst  33815  1stmbfm  33816  2ndmbfm  33817  imambfm  33818  cnmbfm  33819  mbfmco  33820  mbfmco2  33821  0elcarsg  33863  carsgclctun  33877  sibfof  33896  oddpwdc  33910  eulerpartlemmf  33931  eulerpartlemgs2  33936  0rrv  34007  ballotlemfc0  34048  ballotlemfcc  34049  signstfveq0  34145  breprexplemc  34200  bnj1452  34619  usgrgt2cycl  34676  acycgr1v  34695  derangen  34718  subfacval3  34735  cvmseu  34822  cvmliftmolem2  34828  cvmliftlem7  34837  cvmliftlem15  34844  cvmlift2lem9a  34849  cvmlift2lem9  34857  cvmlift2lem10  34858  cvmlift2lem11  34859  cvmlift2lem12  34860  cvmlift3lem6  34870  cvmlift3lem8  34872  ex-sategoelel  34967  ex-sategoelelomsuc  34972  mclsppslem  35129  mclspps  35130  wsuclem  35357  fness  35769  fnetr  35771  fnessref  35777  refssfne  35778  neibastop1  35779  neibastop2  35781  tailfb  35797  filnetlem3  35800  bj-finsumval0  36700  bj-rvecvec  36714  dfgcd3  36739  lindsadd  37021  poimirlem13  37041  poimirlem15  37043  poimirlem24  37052  poimirlem28  37056  mblfinlem2  37066  ovoliunnfl  37070  volsupnfl  37073  mbfresfi  37074  iblabsnc  37092  iblmulc2nc  37093  ftc1cnnclem  37099  ftc1cnnc  37100  ftc1anc  37109  sdclem2  37150  metf1o  37163  ismtyhmeolem  37212  ismtyres  37216  heibor1lem  37217  bfplem2  37231  bfp  37232  rrncmslem  37240  iccbnd  37248  icccmpALT  37249  rngogrphom  37379  rngoisoco  37390  keridl  37440  lsmcv2  38438  lsatcv0  38440  lcvexchlem4  38446  lcvexchlem5  38447  l1cvpat  38463  lfl0f  38478  lfladdcl  38480  lflnegcl  38484  lkrlss  38504  eqlkr  38508  lkrlsp  38511  lkrlsp2  38512  lshpkrcl  38525  lkrin  38573  1cvrjat  38885  llni  38918  llnle  38928  lplni  38942  lplnle  38950  llncvrlpln2  38967  2atmat  38971  lvoli  38985  lplncvrlvol2  39025  elpaddri  39212  paddclN  39252  pclclN  39301  pclfinN  39310  0psubclN  39353  1psubclN  39354  atpsubclN  39355  pmapsubclN  39356  osumclN  39377  pexmidN  39379  pexmidlem6N  39385  lhp2lt  39411  lautcnv  39500  idlaut  39506  lautco  39507  idldil  39524  ldilcnv  39525  ldilco  39526  ltrncnv  39556  idltrn  39560  cdleme16d  39691  cdleme50laut  39957  cdleme50ldil  39958  cdleme50ltrn  39967  ltrnco  40129  dian0  40449  dia0eldmN  40450  dia1eldmN  40451  dialss  40456  diaintclN  40468  docaclN  40534  doca2N  40536  djajN  40547  dibintclN  40577  diblss  40580  dicvaddcl  40600  dicvscacl  40601  dicn0  40602  cdlemn11a  40617  dihord2cN  40631  dihord11b  40632  dihord6apre  40666  dihmeetlem1N  40700  dihglblem5apreN  40701  dihpN  40746  dihjatcclem4  40831  dochkr1  40888  islpoldN  40894  lcfrlem31  40983  mapdpglem18  41099  mapdheq2  41139  mapdheq4  41142  mapdh6aN  41145  hdmap1l6a  41219  hdmap14lem4a  41281  lcmineqlem4  41440  frlmfzoccat  41665  drnginvmuld  41685  psrbagres  41698  evlselvlem  41741  evlselv  41742  fsuppind  41745  fsuppssind  41748  prjspvs  41956  irrapxlem4  42167  pell1234qrdich  42203  pell1qr1  42213  pell14qrgap  42217  pellqrexplicit  42219  rmspecfund  42251  fzmaxdif  42324  acongeq  42326  jm2.23  42339  jm3.1  42363  lmhmlnmsplit  42433  hbt  42476  dgrsub2  42481  proot1ex  42546  cantnfub  42673  cantnfresb  42676  cantnf2  42677  tfsconcatfv2  42692  tfsconcatrn  42694  tfsconcatb0  42696  naddcnff  42714  naddcnffo  42716  naddcnfid1  42719  naddcnfid2  42720  clublem  42963  dftrcl3  43073  mnugrud  43644  hashnzfz2  43681  dvconstbi  43694  ubelsupr  44305  restopn3  44445  wessf1ornlem  44481  lefldiveq  44597  iccintsng  44831  climsuse  44919  mullimc  44927  limcdm0  44929  limccog  44931  mullimcf  44934  constlimc  44935  idlimc  44937  limcperiod  44939  limsupre  44952  limcleqr  44955  neglimc  44958  addlimc  44959  0ellimcdiv  44960  xlimliminflimsup  45173  cncfshift  45185  cncfperiod  45190  cncfuni  45197  icccncfext  45198  cncfiooicclem1  45204  fperdvper  45230  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  mbfres2cn  45269  iblsplit  45277  stoweidlem7  45318  stoweidlem13  45324  stoweidlem26  45337  wallispilem3  45378  stirlinglem6  45390  stirlinglem10  45394  dirkercncf  45418  fourierdlem6  45424  fourierdlem11  45429  fourierdlem12  45430  fourierdlem15  45433  fourierdlem26  45444  fourierdlem42  45460  fourierdlem50  45467  fourierdlem51  45468  fourierdlem52  45469  fourierdlem54  45471  fourierdlem62  45479  fourierdlem79  45496  fourierdlem102  45519  fourierdlem114  45531  etransclem23  45568  zgeltp1eq  46612  setsnidel  46640  preimafvsnel  46642  iccpartres  46681  prpair  46764  fpprel2  47004  isuspgrim  47096  grimidvtxedg  47097  grimcnv  47100  isassintop  47195  rhmsubcALTV  47270  srhmsubcALTV  47310  fldhmsubcALTV  47318  rmfsupp  47361  mndpfsupp  47363  scmfsupp  47365  mptcfsupp  47367  lcoel0  47419  lincsumcl  47422  lincscmcl  47423  lcoss  47427  lindsrng01  47459  lincreslvec3  47473  lindssnlvec  47477  zgtp1leeq  47512  lubsscl  47902  glbsscl  47903  idmon  47945  idepi  47946  thinciso  47989