Theorem syl13anc 1328

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl13anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl13anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1242	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 693	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl23anc  1333  syl33anc  1341  disjxiun  4649  disjxiunOLD  4650  wereu2  5111  ordelord  5745  caovassd  6833  caovcand  6836  caovordid  6840  caovordd  6842  caovdid  6849  caovdird  6852  swoer  7772  swoord1  7773  swoord2  7774  frfi  8205  indexfi  8274  ssfii  8325  elfiun  8336  suplub2  8367  supgtoreq  8376  infltoreq  8408  wemaplem2  8452  htalem  8759  cofsmo  9091  alephsing  9098  sornom  9099  axdc3lem4  9275  zorn2lem1  9318  ttukeylem6  9336  ttukeylem7  9337  prlem934  9855  supfirege  11009  suprfinzcl  11492  ssfzunsn  12387  fzosubel3  12528  fsuppmapnn0fiublem  12789  seqsplit  12834  seqcaopr  12838  ccatass  13371  wrdcctswrd  13465  wrdeqs1cat  13474  splid  13504  spllen  13505  splfv1  13506  splfv2a  13507  splval2  13508  swrds2  13685  isercolllem2  14396  fsumiun  14553  zprod  14667  lcmftp  15349  pcgcd1  15581  cshwsidrepswmod0  15801  cshwshashlem2  15803  cshwsdisj  15805  firest  16093  iscatd2  16342  posasymb  16952  joinle  17014  meetle  17028  lattrd  17058  latleeqj1  17063  latjlej1  17065  latjlej12  17067  latnlej2  17071  latjidm  17074  latleeqm1  17079  latmlem1  17081  latmlem12  17083  latmidm  17086  latledi  17089  latjass  17095  latj12  17096  latj13  17098  latj31  17099  latjrot  17100  latj4  17101  mod1ile  17105  lubun  17123  clatleglb  17126  latdisdlem  17189  mnd32g  17305  mnd12g  17306  mnd4g  17307  ismndd  17313  prdsmndd  17323  imasmnd  17328  mrcmndind  17366  gsumspl  17381  grpasscan2  17479  grpidrcan  17480  grpidlcan  17481  grpinvinv  17482  grplmulf1o  17489  grpinvssd  17492  grpinvadd  17493  grpsubrcan  17496  grpsubadd  17503  grpaddsubass  17505  grppncan  17506  grpsubsub4  17508  grppnpcan2  17509  grpnpncan  17510  grpnpncan0  17511  grpnnncan2  17512  dfgrp3lem  17513  dfgrp3  17514  grplactcnv  17518  imasgrp  17531  mhmmnd  17537  mulgaddcomlem  17563  mulgaddcom  17564  mulgnn0dir  17571  mulgdirlem  17572  mulgneg2  17575  mulgnnass  17576  mulgnnassOLD  17577  mulgnn0ass  17578  mulgass  17579  mulgmodid  17581  nsgconj  17627  isnsg3  17628  nmzsubg  17635  ssnmz  17636  eqger  17644  eqgcpbl  17648  conjghm  17691  conjnmz  17694  conjnmzb  17695  subgga  17733  gass  17734  gasubg  17735  galcan  17737  gacan  17738  gapm  17739  gaorber  17741  gastacl  17742  gastacos  17743  cntzsubm  17768  cntzsubg  17769  oppgmnd  17784  symggen  17890  odmodnn0  17959  mndodconglem  17960  odmod  17965  odcong  17968  odmulgid  17971  odbezout  17975  gexdvdsi  17998  gexdvds  17999  sylow1lem2  18014  sylow1lem4  18016  sylow2blem1  18035  sylow2blem2  18036  sylow2blem3  18037  sylow3lem1  18042  sylow3lem2  18043  lsmass  18083  lsmmod  18088  lsmdisj2  18095  subgdisj1  18104  efgredleme  18156  efgredlemc  18158  efgcpbllemb  18168  frgp0  18173  frgpuplem  18185  abl32  18214  abladdsub4  18219  abladdsub  18220  ablpncan2  18221  ablsubsub  18223  mulgdi  18232  mulgsubdi  18235  odadd1  18251  odadd2  18252  gex2abl  18254  oddvdssubg  18258  cygabl  18292  telgsumfzslem  18385  ablfacrp  18465  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem4  18477  srgmulgass  18531  srgpcomp  18532  srgpcompp  18533  srgpcomppsc  18534  srgbinomlem3  18542  srgbinomlem4  18543  srgbinomlem  18544  csrgbinom  18546  ringadd2  18575  rngo2times  18576  ringcom  18579  ringlz  18587  ringrz  18588  ringnegl  18594  rngnegr  18595  ringmneg1  18596  ringmneg2  18597  ringsubdi  18599  rngsubdir  18600  mulgass2  18601  prdsringd  18612  imasring  18619  opprring  18631  mulgass3  18637  dvdsrtr  18652  dvdsrmul1  18653  unitgrp  18667  dvrass  18690  dvrcan1  18691  dvrcan3  18692  irredrmul  18707  drngmul0or  18768  subrginv  18796  cntzsubr  18812  lmod0vs  18896  lmodvs0  18897  lmodvsmmulgdi  18898  lmodfopne  18901  lmodvneg1  18906  lmodvsneg  18907  lmodcom  18909  lmodsubvs  18919  lmodsubdi  18920  lmodsubdir  18921  lssvsubcl  18944  lssvacl  18954  lssvscl  18955  islss3  18959  lss1d  18963  lssintcl  18964  prdslmodd  18969  lmodvsinv  19036  lmodvsinv2  19037  lmhmplusg  19044  lmhmvsca  19045  lsmcl  19083  pj1lmhm  19100  lvecvs0or  19108  lssvs0or  19110  lvecinv  19113  lspsnvs  19114  lspfixed  19128  lspexch  19129  lspsolvlem  19142  lspsolv  19143  lssacsex  19144  lspsnat  19145  lsppratlem1  19147  lsppratlem3  19149  lsppratlem4  19150  lbsextlem2  19159  lbsextlem4  19161  sralmod  19187  2idlcpbl  19234  unitrrg  19293  assa2ass  19322  issubassa  19324  sraassa  19325  asclghm  19338  asclmul1  19339  asclmul2  19340  asclrhm  19342  assamulgscmlem2  19349  psrbagcon  19371  psrbagconcl  19373  psrbagconf1o  19374  gsumbagdiaglem  19375  psrmulcllem  19387  psrlidm  19403  psrridm  19404  psrass1  19405  psrdi  19406  psrdir  19407  psrass23l  19408  psrcom  19409  mplmon2mul  19501  evlslem1  19515  coe1subfv  19636  lply1binomsc  19677  mulgrhm  19846  cygznlem3  19918  evpmodpmf1o  19942  ipdi  19985  ip2di  19986  ipsubdir  19987  ipsubdi  19988  ip2subdi  19989  ipassr  19991  ipassr2  19992  ip2eq  19998  ocvlss  20016  lsmcss  20036  frlmphl  20120  frlmup1  20137  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  dmatmul  20303  dmatsubcl  20304  scmataddcl  20322  smatvscl  20330  scmatghm  20339  mavmulass  20355  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  mdetunilem7  20424  mdetuni0  20427  matinv  20483  pm2mpghm  20621  chpscmatgsummon  20650  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  iinopn  20707  subbascn  21058  cnhaus  21158  nrmsep2  21160  nrmsep  21161  regsep2  21180  isreg2  21181  hauscmplem  21209  1stcfb  21248  2ndcctbss  21258  ptbasfi  21384  pthaus  21441  txtube  21443  txhaus  21450  xkohaus  21456  kqnrmlem1  21546  kqnrmlem2  21547  nrmr0reg  21552  nrmhmph  21597  fbssint  21642  infil  21667  fgabs  21683  filconn  21687  filuni  21689  trfil2  21691  trfg  21695  ufprim  21713  elfm3  21754  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  hausflimi  21784  hauspwpwf1  21791  fclsneii  21821  supnfcls  21824  flimfnfcls  21832  fclscmpi  21833  alexsublem  21848  ghmcnp  21918  qustgpopn  21923  psmetsym  22115  psmettri  22116  psmetge0  22117  psmetres2  22119  xmetge0  22149  xmetsym  22152  xmettri  22156  xmetres2  22166  prdsxmetlem  22173  prdsmet  22175  imasdsf1olem  22178  imasf1oxmet  22180  bldisj  22203  xblss2ps  22206  xblss2  22207  xmeter  22238  prdsbl  22296  metustexhalf  22361  metust  22363  nrmmetd  22379  ngpsubcan  22418  nmmtri  22426  nmrtri  22428  ngptgp  22440  nlmvscnlem2  22489  nrginvrcnlem  22495  metdcnlem  22639  clmvs2  22894  clmmulg  22901  clmnegneg  22904  clmnegsubdi2  22905  clmsub4  22906  cvsmuleqdivd  22934  cvsdiveqd  22935  ncvspi  22956  cphabscl  22985  cphsqrtcl2  22986  cphsqrtcl3  22987  cphnmf  22995  cph2ass  23013  cphassi  23014  cphassir  23015  ipcau2  23033  tchcphlem2  23035  ipcnlem2  23043  cfilfcls  23072  iscau3  23076  iscmet3lem2  23090  iscmet3  23091  relcmpcmet  23115  minveclem2  23197  minveclem4  23203  pjthlem1  23208  pjthlem2  23209  uniioombllem4  23354  dyadmax  23366  itg1addlem4  23466  itg1climres  23481  ply1divex  23896  aalioulem2  24088  amgmlem  24716  dvdsppwf1o  24912  perfect1  24953  perfectlem1  24954  perfectlem2  24955  dchrptlem2  24990  colline  25544  ttgcontlem1  25765  axcontlem9  25852  eengtrkg  25865  eengtrkge  25866  nbfusgrlevtxm2  26280  nbusgrvtxm1  26281  elwwlks2ons3  26848  usgr2wspthon  26858  clwwlknclwwlkdifnum  26874  numclwwlk5  27246  grpoidinvlem4  27361  grpoinvop  27387  grponpcan  27397  vcm  27431  nvmul0or  27505  nvpncan2  27508  nvdif  27521  nvabs  27527  smcnlem  27552  lnomul  27615  minvecolem2  27731  superpos  29213  ssnnssfz  29549  omndmul2  29712  omndmul3  29713  ogrpaddltbi  29719  ogrpaddltrbid  29721  ogrpsublt  29722  ogrpinvlt  29724  isarchi3  29741  archirngz  29743  archiabllem1a  29745  archiabllem1  29747  archiabllem2a  29748  archiabllem2c  29749  slmdvs0  29778  gsumvsca1  29782  gsumvsca2  29783  dvrdir  29790  rdivmuldivd  29791  dvrcan5  29793  ornglmullt  29807  isarchiofld  29817  rhmdvd  29821  rhmunitinv  29822  psgnfzto1stlem  29850  pmtridfv1  29857  pmtridfv2  29858  mdetpmtr1  29889  mdetpmtr12  29891  mdetlap  29898  locfinref  29908  metideq  29936  metider  29937  pstmxmet  29940  lmxrge0  29998  qqhghm  30032  qqhrhm  30033  ispisys2  30216  rossros  30243  measdivcst  30288  oddpwdc  30416  ballotlemiex  30563  wrdsplex  30618  cvmopnlem  31260  cvmliftmolem2  31264  cvmliftlem6  31272  cvmliftlem8  31274  cvmliftlem9  31275  cvmlift2lem9  31293  cvmlift3lem2  31302  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  sotrd  31655  nodense  31842  nosupfv  31852  noetalem5  31867  cgrtriv  32109  cgrdegen  32111  cgrextend  32115  segconeq  32117  btwntriv2  32119  btwncomand  32122  btwntriv1  32123  btwnintr  32126  btwnexch3  32127  btwnouttr  32131  btwnexch  32132  trisegint  32135  ifscgr  32151  btwnxfr  32163  colineartriv1  32174  colineartriv2  32175  colinearxfr  32182  fscgr  32187  lineid  32190  idinside  32191  endofsegidand  32193  btwnconn1lem5  32198  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn1lem13  32206  brsegle2  32216  segleantisym  32222  broutsideof2  32229  btwnoutside  32232  outsideoftr  32236  outsideofeq  32237  outsideofeu  32238  outsidele  32239  lineunray  32254  lineelsb2  32255  linecom  32257  linethru  32260  neibastop1  32354  lindsenlbs  33404  matunitlindflem1  33405  poimirlem28  33437  poimirlem32  33441  heicant  33444  mettrifi  33553  isbnd3  33583  heibor1lem  33608  bfplem2  33622  ghomdiv  33691  rngo2  33706  rngolz  33721  rngorz  33722  zerdivemp1x  33746  lfladdcl  34358  lflvscl  34364  eqlkr3  34388  lkrlsp  34389  lshpkrlem4  34400  oldmm1  34504  olj01  34512  latmassOLD  34516  latm32  34518  latmrot  34519  latm4  34520  olm01  34523  cmtcomlemN  34535  cmtbr3N  34541  cmtbr4N  34542  lecmtN  34543  omlfh1N  34545  atlen0  34597  atnle  34604  atlatmstc  34606  atlatle  34607  cvlexchb1  34617  cvlcvr1  34626  ishlat3N  34641  hlatjass  34656  hlatj12  34657  hlatj32  34658  hlsupr2  34673  hlhgt2  34675  hl0lt1N  34676  hlrelat  34688  hlrelat2  34689  exatleN  34690  hlrelat3  34698  cvrval5  34701  cvrexchlem  34705  cvratlem  34707  cvrat  34708  atcvr0eq  34712  lnnat  34713  atlt  34723  atlelt  34724  2atlt  34725  atexchltN  34727  cvrat3  34728  2atjm  34731  atbtwn  34732  4noncolr3  34739  athgt  34742  3dimlem3a  34746  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4OLDN  34751  3dim1  34753  3dim2  34754  1cvratex  34759  ps-1  34763  ps-2  34764  hlatexch3N  34766  hlatexch4  34767  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem5  34773  3atlem6  34774  llnnleat  34799  llncmp  34808  2at0mat0  34811  2atmat0  34812  2atm  34813  lplni2  34823  lvolex3N  34824  lplnnle2at  34827  lplnnleat  34828  lplnnlelln  34829  2atnelpln  34830  llncvrlpln  34844  2atmat  34847  lplncmp  34848  lplnexllnN  34850  2llnjaN  34852  2llnm4  34856  2llnmeqat  34857  lvolnle3at  34868  lvolnleat  34869  2atnelvolN  34873  islvol2aN  34878  4atlem3  34882  4atlem3a  34883  4atlem3b  34884  4atlem4a  34885  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  4atlem10  34892  4atlem11b  34894  4atlem11  34895  4atlem12b  34897  4atlem12  34898  4at2  34900  lplncvrlvol  34902  lvolcmp  34903  2lplnja  34905  dalemqrprot  34934  dalemply  34940  dalemsly  34941  dalemrot  34943  dalemrotyz  34944  dalem1  34945  dalemcea  34946  dalem3  34950  dalem5  34953  dalem8  34956  dalem-cly  34957  dalem11  34960  dalem12  34961  dalem16  34965  dalem17  34966  dalem18  34967  dalem21  34980  dalem24  34983  dalem25  34984  dalem38  34996  dalem39  34997  dalem44  35002  dalem54  35012  dalem55  35013  dalem57  35015  dalem58  35016  dalem59  35017  dalem60  35018  dath2  35023  2atm2atN  35071  2llnma1b  35072  2llnma3r  35074  cdlema1N  35077  cdlemblem  35079  paddasslem5  35110  paddasslem10  35115  paddasslem12  35117  paddasslem13  35118  paddass  35124  padd12N  35125  padd4N  35126  paddss  35131  pmodlem1  35132  pmodl42N  35137  pmapjoin  35138  pmapjlln1  35141  atmod1i2  35145  llnmod1i2  35146  llnexchb2  35155  dalawlem2  35158  dalawlem3  35159  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  pclunN  35184  osumcllem1N  35242  pexmidlem3N  35258  lhp2lt  35287  lhp0lt  35289  lhpexle2lem  35295  lhpexle3lem  35297  lhpocnle  35302  lhpj1  35308  lhpmcvr4N  35312  lhp2at0  35318  lhpat3  35332  4atexlemtlw  35353  4atexlemc  35355  4atexlemnclw  35356  4atexlemcnd  35358  lautcvr  35378  lautj  35379  lautm  35380  ltrnm  35417  ltrnj  35418  ltrncvr  35419  trlval3  35474  cdlemc5  35482  cdlemd2  35486  cdlemd3  35487  cdleme0e  35504  cdleme1  35514  cdleme3c  35517  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme5  35527  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme9  35540  cdleme11c  35548  cdleme11g  35552  cdleme11k  35555  cdleme11  35557  cdleme12  35558  cdleme15b  35562  cdleme15d  35564  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17b  35574  cdleme18b  35579  cdleme22gb  35581  cdlemednpq  35586  cdleme19a  35591  cdleme20aN  35597  cdleme20bN  35598  cdleme20c  35599  cdleme20d  35600  cdleme20j  35606  cdleme21c  35615  cdleme22aa  35627  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme23b  35638  cdleme23c  35639  cdleme28a  35658  cdleme30a  35666  cdlemefs29bpre0N  35704  cdlemefs29bpre1N  35705  cdlemefs29cpre1N  35706  cdlemefs29clN  35707  cdlemefs32fvaN  35710  cdlemefs32fva1  35711  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35f  35742  cdleme36a  35748  cdleme36m  35749  cdleme37m  35750  cdleme39a  35753  cdleme42c  35760  cdleme42i  35771  cdleme42keg  35774  cdleme42mgN  35776  cdleme48bw  35790  cdlemeg46fjgN  35809  cdlemeg46fjv  35811  cdlemeg46req  35817  cdleme50trn1  35837  cdlemf1  35849  cdlemf2  35850  cdlemg1cex  35876  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg4c  35900  cdlemg4  35905  cdlemg6c  35908  cdlemg8b  35916  cdlemg10c  35927  cdlemg10  35929  cdlemg11b  35930  cdlemg12f  35936  cdlemg13a  35939  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg18b  35967  cdlemg19a  35971  cdlemg27a  35980  cdlemg27b  35984  cdlemg33b0  35989  cdlemg33a  35994  cdlemg35  36001  trlcolem  36014  cdlemg42  36017  cdlemg46  36023  trljco  36028  tendopltp  36068  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  cdlemi  36108  cdlemk3  36121  cdlemk10  36131  cdlemk11  36137  cdlemk15  36143  cdlemk1u  36147  cdlemk5u  36149  cdlemk11u  36159  cdlemk39  36204  cdlemkid1  36210  cdlemk50  36240  cdlemk51  36241  erngdvlem3-rN  36286  tendocnv  36310  tendospcanN  36312  dialss  36335  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  dia2dimlem10  36362  dia2dimlem12  36364  dvhvaddass  36386  dvhlveclem  36397  cdlemm10N  36407  doca2N  36415  djajN  36426  dib1dim2  36457  diblss  36459  diclspsn  36483  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505  dihord1  36507  dihord2a  36508  dihord2pre2  36515  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihopelvalcpre  36537  dihord5b  36548  dihord6b  36549  dihord5apre  36551  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem2N  36583  dihglbcpreN  36589  dihmeetbclemN  36593  dihmeetlem3N  36594  dihmeetlem6  36598  dih1dimatlem  36618  djhcvat42  36704  dihjatcclem1  36707  dihjatcclem4  36710  dvh4dimat  36727  lcfl7lem  36788  lclkrlem2m  36808  lcfrlem1  36831  lcdvsass  36896  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  mapdh6gN  37031  mapdh6hN  37032  hdmap1l6g  37106  hdmap1l6h  37107  hdmapneg  37138  hdmap14lem8  37167  hgmapadd  37186  hgmapmul  37187  hgmapvvlem1  37215  irrapxlem5  37390  aomclem2  37625  isnumbasgrplem2  37674  mpaaeu  37720  mendring  37762  mendlmod  37763  relexpnul  37970  caofcan  38522  disjiun2  39226  wessf1ornlem  39371  fisupclrnmpt  39622  limsupequzlem  39954  cnrefiisplem  40055  stoweidlem18  40235  stoweidlem41  40258  stoweidlem45  40262  stoweidlem55  40272  fourierdlem25  40349  fourierdlem31  40355  fourierdlem37  40361  fourierdlem42  40366  etransclem48  40499  ioorrnopnlem  40524  issalgend  40556  sge0iunmptlemfi  40630  hoicvr  40762  hoidmvlelem2  40810  iunhoiioolem  40889  vonioolem1  40894  prmdvdsfmtnof1lem1  41496  prmdvdsfmtnof  41498  sgprmdvdsmersenne  41521  perfectALTVlem1  41630  perfectALTVlem2  41631  rnglz  41884  ssnn0ssfz  42127  zlmodzxzsub  42138  invginvrid  42148  lmodvsmdi  42163  ply1sclrmsm  42171  lincsum  42218  lincscm  42219  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  ldepsprlem  42261  lincresunit3lem1  42268  lincresunit3lem2  42269  isldepslvec2  42274  relogbmulbexp  42355