Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl13anc Structured version   Visualization version   GIF version

Theorem syl13anc 1368
 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
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1261 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 694 1 (𝜑𝜂)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054 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 385  df-3an 1056 This theorem is referenced by:  syl23anc  1373  syl33anc  1381  disjxiun  4681  disjxiunOLD  4682  wereu2  5140  ordelord  5783  caovassd  6875  caovcand  6878  caovordid  6882  caovordd  6884  caovdid  6891  caovdird  6894  swoer  7817  swoord1  7818  swoord2  7819  frfi  8246  indexfi  8315  ssfii  8366  elfiun  8377  suplub2  8408  supgtoreq  8417  infltoreq  8449  wemaplem2  8493  htalem  8797  cofsmo  9129  alephsing  9136  sornom  9137  axdc3lem4  9313  zorn2lem1  9356  ttukeylem6  9374  ttukeylem7  9375  prlem934  9893  supfirege  11047  suprfinzcl  11530  ssfzunsn  12425  fzosubel3  12568  fsuppmapnn0fiublem  12829  seqsplit  12874  seqcaopr  12878  ccatass  13406  wrdcctswrd  13511  wrdeqs1cat  13520  splid  13550  spllen  13551  splfv1  13552  splfv2a  13553  splval2  13554  swrds2  13731  isercolllem2  14440  fsumiun  14597  zprod  14711  lcmftp  15396  pcgcd1  15628  cshwsidrepswmod0  15848  cshwshashlem2  15850  cshwsdisj  15852  firest  16140  iscatd2  16389  posasymb  16999  joinle  17061  meetle  17075  lattrd  17105  latleeqj1  17110  latjlej1  17112  latjlej12  17114  latnlej2  17118  latjidm  17121  latleeqm1  17126  latmlem1  17128  latmlem12  17130  latmidm  17133  latledi  17136  latjass  17142  latj12  17143  latj13  17145  latj31  17146  latjrot  17147  latj4  17148  mod1ile  17152  lubun  17170  clatleglb  17173  latdisdlem  17236  mnd32g  17352  mnd12g  17353  mnd4g  17354  ismndd  17360  prdsmndd  17370  imasmnd  17375  mrcmndind  17413  gsumspl  17428  grpasscan2  17526  grpidrcan  17527  grpidlcan  17528  grpinvinv  17529  grplmulf1o  17536  grpinvssd  17539  grpinvadd  17540  grpsubrcan  17543  grpsubadd  17550  grpaddsubass  17552  grppncan  17553  grpsubsub4  17555  grppnpcan2  17556  grpnpncan  17557  grpnpncan0  17558  grpnnncan2  17559  dfgrp3lem  17560  dfgrp3  17561  grplactcnv  17565  imasgrp  17578  mhmmnd  17584  mulgaddcomlem  17610  mulgaddcom  17611  mulgnn0dir  17618  mulgdirlem  17619  mulgneg2  17622  mulgnnass  17623  mulgnnassOLD  17624  mulgnn0ass  17625  mulgass  17626  mulgmodid  17628  nsgconj  17674  isnsg3  17675  nmzsubg  17682  ssnmz  17683  eqger  17691  eqgcpbl  17695  conjghm  17738  conjnmz  17741  conjnmzb  17742  subgga  17779  gass  17780  gasubg  17781  galcan  17783  gacan  17784  gapm  17785  gaorber  17787  gastacl  17788  gastacos  17789  cntzsubm  17814  cntzsubg  17815  oppgmnd  17830  symggen  17936  odmodnn0  18005  mndodconglem  18006  odmod  18011  odcong  18014  odmulgid  18017  odbezout  18021  gexdvdsi  18044  gexdvds  18045  sylow1lem2  18060  sylow1lem4  18062  sylow2blem1  18081  sylow2blem2  18082  sylow2blem3  18083  sylow3lem1  18088  sylow3lem2  18089  lsmass  18129  lsmmod  18134  lsmdisj2  18141  subgdisj1  18150  efgredleme  18202  efgredlemc  18204  efgcpbllemb  18214  frgp0  18219  frgpuplem  18231  abl32  18260  abladdsub4  18265  abladdsub  18266  ablpncan2  18267  ablsubsub  18269  mulgdi  18278  mulgsubdi  18281  odadd1  18297  odadd2  18298  gex2abl  18300  oddvdssubg  18304  cygabl  18338  telgsumfzslem  18431  ablfacrp  18511  pgpfac1lem2  18520  pgpfac1lem3a  18521  pgpfac1lem3  18522  pgpfac1lem4  18523  srgmulgass  18577  srgpcomp  18578  srgpcompp  18579  srgpcomppsc  18580  srgbinomlem3  18588  srgbinomlem4  18589  srgbinomlem  18590  csrgbinom  18592  ringadd2  18621  rngo2times  18622  ringcom  18625  ringlz  18633  ringrz  18634  ringnegl  18640  rngnegr  18641  ringmneg1  18642  ringmneg2  18643  ringsubdi  18645  rngsubdir  18646  mulgass2  18647  prdsringd  18658  imasring  18665  opprring  18677  mulgass3  18683  dvdsrtr  18698  dvdsrmul1  18699  unitgrp  18713  dvrass  18736  dvrcan1  18737  dvrcan3  18738  irredrmul  18753  drngmul0or  18816  subrginv  18844  cntzsubr  18860  lmod0vs  18944  lmodvs0  18945  lmodvsmmulgdi  18946  lmodfopne  18949  lmodvneg1  18954  lmodvsneg  18955  lmodcom  18957  lmodsubvs  18967  lmodsubdi  18968  lmodsubdir  18969  lssvsubcl  18992  lssvacl  19002  lssvscl  19003  islss3  19007  lss1d  19011  lssintcl  19012  prdslmodd  19017  lmodvsinv  19084  lmodvsinv2  19085  lmhmplusg  19092  lmhmvsca  19093  lsmcl  19131  pj1lmhm  19148  lvecvs0or  19156  lssvs0or  19158  lvecinv  19161  lspsnvs  19162  lspfixed  19176  lspexch  19177  lspsolvlem  19190  lspsolv  19191  lssacsex  19192  lspsnat  19193  lsppratlem1  19195  lsppratlem3  19197  lsppratlem4  19198  lbsextlem2  19207  lbsextlem4  19209  sralmod  19235  2idlcpbl  19282  unitrrg  19341  assa2ass  19370  issubassa  19372  sraassa  19373  asclghm  19386  asclmul1  19387  asclmul2  19388  asclrhm  19390  assamulgscmlem2  19397  psrbagcon  19419  psrbagconcl  19421  psrbagconf1o  19422  gsumbagdiaglem  19423  psrmulcllem  19435  psrlidm  19451  psrridm  19452  psrass1  19453  psrdi  19454  psrdir  19455  psrass23l  19456  psrcom  19457  mplmon2mul  19549  evlslem1  19563  coe1subfv  19684  lply1binomsc  19725  mulgrhm  19894  cygznlem3  19966  evpmodpmf1o  19990  ipdi  20033  ip2di  20034  ipsubdir  20035  ipsubdi  20036  ip2subdi  20037  ipassr  20039  ipassr2  20040  ip2eq  20046  ocvlss  20064  lsmcss  20084  frlmphl  20168  frlmup1  20185  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  dmatmul  20351  dmatsubcl  20352  scmataddcl  20370  smatvscl  20378  scmatghm  20387  mavmulass  20403  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  mdetunilem7  20472  mdetuni0  20475  matinv  20531  pm2mpghm  20669  chpscmatgsummon  20698  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  iinopn  20755  subbascn  21106  cnhaus  21206  nrmsep2  21208  nrmsep  21209  regsep2  21228  isreg2  21229  hauscmplem  21257  1stcfb  21296  2ndcctbss  21306  ptbasfi  21432  pthaus  21489  txtube  21491  txhaus  21498  xkohaus  21504  kqnrmlem1  21594  kqnrmlem2  21595  nrmr0reg  21600  nrmhmph  21645  fbssint  21689  infil  21714  fgabs  21730  filconn  21734  filuni  21736  trfil2  21738  trfg  21742  ufprim  21760  elfm3  21801  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  hausflimi  21831  hauspwpwf1  21838  fclsneii  21868  supnfcls  21871  flimfnfcls  21879  fclscmpi  21880  alexsublem  21895  ghmcnp  21965  qustgpopn  21970  psmetsym  22162  psmettri  22163  psmetge0  22164  psmetres2  22166  xmetge0  22196  xmetsym  22199  xmettri  22203  xmetres2  22213  prdsxmetlem  22220  prdsmet  22222  imasdsf1olem  22225  imasf1oxmet  22227  bldisj  22250  xblss2ps  22253  xblss2  22254  xmeter  22285  prdsbl  22343  metustexhalf  22408  metust  22410  nrmmetd  22426  ngpsubcan  22465  nmmtri  22473  nmrtri  22475  ngptgp  22487  nlmvscnlem2  22536  nrginvrcnlem  22542  metdcnlem  22686  clmvs2  22940  clmmulg  22947  clmnegneg  22950  clmnegsubdi2  22951  clmsub4  22952  cvsmuleqdivd  22980  cvsdiveqd  22981  ncvspi  23002  cphabscl  23031  cphsqrtcl2  23032  cphsqrtcl3  23033  cphnmf  23041  cph2ass  23059  cphassi  23060  cphassir  23061  ipcau2  23079  tchcphlem2  23081  ipcnlem2  23089  cfilfcls  23118  iscau3  23122  iscmet3lem2  23136  iscmet3  23137  relcmpcmet  23161  minveclem2  23243  minveclem4  23249  pjthlem1  23254  pjthlem2  23255  uniioombllem4  23400  dyadmax  23412  itg1addlem4  23511  itg1climres  23526  ply1divex  23941  aalioulem2  24133  amgmlem  24761  dvdsppwf1o  24957  perfect1  24998  perfectlem1  24999  perfectlem2  25000  dchrptlem2  25035  colline  25589  ttgcontlem1  25810  axcontlem9  25897  eengtrkg  25910  eengtrkge  25911  nbfusgrlevtxm2  26324  nbusgrvtxm1  26325  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  usgr2wspthon  26932  clwwlknclwwlkdifnum  26946  clwwlknclwwlkdifnumOLD  26948  numclwwlk5  27375  grpoidinvlem4  27489  grpoinvop  27515  grponpcan  27525  vcm  27559  nvmul0or  27633  nvpncan2  27636  nvdif  27649  nvabs  27655  smcnlem  27680  lnomul  27743  minvecolem2  27859  superpos  29341  ssnnssfz  29677  omndmul2  29840  omndmul3  29841  ogrpaddltbi  29847  ogrpaddltrbid  29849  ogrpsublt  29850  ogrpinvlt  29852  isarchi3  29869  archirngz  29871  archiabllem1a  29873  archiabllem1  29875  archiabllem2a  29876  archiabllem2c  29877  slmdvs0  29906  gsumvsca1  29910  gsumvsca2  29911  dvrdir  29918  rdivmuldivd  29919  dvrcan5  29921  ornglmullt  29935  isarchiofld  29945  rhmdvd  29949  rhmunitinv  29950  psgnfzto1stlem  29978  pmtridfv1  29985  pmtridfv2  29986  mdetpmtr1  30017  mdetpmtr12  30019  mdetlap  30026  locfinref  30036  metideq  30064  metider  30065  pstmxmet  30068  lmxrge0  30126  qqhghm  30160  qqhrhm  30161  ispisys2  30344  rossros  30371  measdivcst  30416  oddpwdc  30544  ballotlemiex  30691  wrdsplex  30746  cvmopnlem  31386  cvmliftmolem2  31390  cvmliftlem6  31398  cvmliftlem8  31400  cvmliftlem9  31401  cvmlift2lem9  31419  cvmlift3lem2  31428  cvmlift3lem6  31432  cvmlift3lem7  31433  cvmlift3lem9  31435  sotrd  31781  frpomin  31863  nodense  31967  nosupfv  31977  noetalem5  31992  cgrtriv  32234  cgrdegen  32236  cgrextend  32240  segconeq  32242  btwntriv2  32244  btwncomand  32247  btwntriv1  32248  btwnintr  32251  btwnexch3  32252  btwnouttr  32256  btwnexch  32257  trisegint  32260  ifscgr  32276  btwnxfr  32288  colineartriv1  32299  colineartriv2  32300  colinearxfr  32307  fscgr  32312  lineid  32315  idinside  32316  endofsegidand  32318  btwnconn1lem5  32323  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1lem12  32330  btwnconn1lem13  32331  brsegle2  32341  segleantisym  32347  broutsideof2  32354  btwnoutside  32357  outsideoftr  32361  outsideofeq  32362  outsideofeu  32363  outsidele  32364  lineunray  32379  lineelsb2  32380  linecom  32382  linethru  32385  neibastop1  32479  lindsenlbs  33534  matunitlindflem1  33535  poimirlem28  33567  poimirlem32  33571  heicant  33574  mettrifi  33683  isbnd3  33713  heibor1lem  33738  bfplem2  33752  ghomdiv  33821  rngo2  33836  rngolz  33851  rngorz  33852  zerdivemp1x  33876  lfladdcl  34676  lflvscl  34682  eqlkr3  34706  lkrlsp  34707  lshpkrlem4  34718  oldmm1  34822  olj01  34830  latmassOLD  34834  latm32  34836  latmrot  34837  latm4  34838  olm01  34841  cmtcomlemN  34853  cmtbr3N  34859  cmtbr4N  34860  lecmtN  34861  omlfh1N  34863  atlen0  34915  atnle  34922  atlatmstc  34924  atlatle  34925  cvlexchb1  34935  cvlcvr1  34944  ishlat3N  34959  hlatjass  34974  hlatj12  34975  hlatj32  34976  hlsupr2  34991  hlhgt2  34993  hl0lt1N  34994  hlrelat  35006  hlrelat2  35007  exatleN  35008  hlrelat3  35016  cvrval5  35019  cvrexchlem  35023  cvratlem  35025  cvrat  35026  atcvr0eq  35030  lnnat  35031  atlt  35041  atlelt  35042  2atlt  35043  atexchltN  35045  cvrat3  35046  2atjm  35049  atbtwn  35050  4noncolr3  35057  athgt  35060  3dimlem3a  35064  3dimlem3OLDN  35066  3dimlem4a  35067  3dimlem4OLDN  35069  3dim1  35071  3dim2  35072  1cvratex  35077  ps-1  35081  ps-2  35082  hlatexch3N  35084  hlatexch4  35085  ps-2b  35086  3atlem1  35087  3atlem2  35088  3atlem5  35091  3atlem6  35092  llnnleat  35117  llncmp  35126  2at0mat0  35129  2atmat0  35130  2atm  35131  lplni2  35141  lvolex3N  35142  lplnnle2at  35145  lplnnleat  35146  lplnnlelln  35147  2atnelpln  35148  llncvrlpln  35162  2atmat  35165  lplncmp  35166  lplnexllnN  35168  2llnjaN  35170  2llnm4  35174  2llnmeqat  35175  lvolnle3at  35186  lvolnleat  35187  2atnelvolN  35191  islvol2aN  35196  4atlem3  35200  4atlem3a  35201  4atlem3b  35202  4atlem4a  35203  4atlem4b  35204  4atlem4c  35205  4atlem4d  35206  4atlem10  35210  4atlem11b  35212  4atlem11  35213  4atlem12b  35215  4atlem12  35216  4at2  35218  lplncvrlvol  35220  lvolcmp  35221  2lplnja  35223  dalemqrprot  35252  dalemply  35258  dalemsly  35259  dalemrot  35261  dalemrotyz  35262  dalem1  35263  dalemcea  35264  dalem3  35268  dalem5  35271  dalem8  35274  dalem-cly  35275  dalem11  35278  dalem12  35279  dalem16  35283  dalem17  35284  dalem18  35285  dalem21  35298  dalem24  35301  dalem25  35302  dalem38  35314  dalem39  35315  dalem44  35320  dalem54  35330  dalem55  35331  dalem57  35333  dalem58  35334  dalem59  35335  dalem60  35336  dath2  35341  2atm2atN  35389  2llnma1b  35390  2llnma3r  35392  cdlema1N  35395  cdlemblem  35397  paddasslem5  35428  paddasslem10  35433  paddasslem12  35435  paddasslem13  35436  paddass  35442  padd12N  35443  padd4N  35444  paddss  35449  pmodlem1  35450  pmodl42N  35455  pmapjoin  35456  pmapjlln1  35459  atmod1i2  35463  llnmod1i2  35464  llnexchb2  35473  dalawlem2  35476  dalawlem3  35477  dalawlem5  35479  dalawlem6  35480  dalawlem7  35481  dalawlem8  35482  dalawlem11  35485  dalawlem12  35486  dalawlem13  35487  pclunN  35502  osumcllem1N  35560  pexmidlem3N  35576  lhp2lt  35605  lhp0lt  35607  lhpexle2lem  35613  lhpexle3lem  35615  lhpocnle  35620  lhpj1  35626  lhpmcvr4N  35630  lhp2at0  35636  lhpat3  35650  4atexlemtlw  35671  4atexlemc  35673  4atexlemnclw  35674  4atexlemcnd  35676  lautcvr  35696  lautj  35697  lautm  35698  ltrnm  35735  ltrnj  35736  ltrncvr  35737  trlval3  35792  cdlemc5  35800  cdlemd2  35804  cdlemd3  35805  cdleme0e  35822  cdleme1  35832  cdleme3c  35835  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme5  35845  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme9  35858  cdleme11c  35866  cdleme11g  35870  cdleme11k  35873  cdleme11  35875  cdleme12  35876  cdleme15b  35880  cdleme15d  35882  cdleme16d  35886  cdleme16e  35887  cdleme16f  35888  cdleme17b  35892  cdleme18b  35897  cdleme22gb  35899  cdlemednpq  35904  cdleme19a  35908  cdleme20aN  35914  cdleme20bN  35915  cdleme20c  35916  cdleme20d  35917  cdleme20j  35923  cdleme21c  35932  cdleme22aa  35944  cdleme22b  35946  cdleme22cN  35947  cdleme22d  35948  cdleme22e  35949  cdleme22eALTN  35950  cdleme23b  35955  cdleme23c  35956  cdleme28a  35975  cdleme30a  35983  cdlemefs29bpre0N  36021  cdlemefs29bpre1N  36022  cdlemefs29cpre1N  36023  cdlemefs29clN  36024  cdlemefs32fvaN  36027  cdlemefs32fva1  36028  cdleme32b  36047  cdleme32c  36048  cdleme32e  36050  cdleme35a  36053  cdleme35fnpq  36054  cdleme35b  36055  cdleme35f  36059  cdleme36a  36065  cdleme36m  36066  cdleme37m  36067  cdleme39a  36070  cdleme42c  36077  cdleme42i  36088  cdleme42keg  36091  cdleme42mgN  36093  cdleme48bw  36107  cdlemeg46fjgN  36126  cdlemeg46fjv  36128  cdlemeg46req  36134  cdleme50trn1  36154  cdlemf1  36166  cdlemf2  36167  cdlemg1cex  36193  cdlemg2fv2  36205  cdlemg7fvbwN  36212  cdlemg4c  36217  cdlemg4  36222  cdlemg6c  36225  cdlemg8b  36233  cdlemg10c  36244  cdlemg10  36246  cdlemg11b  36247  cdlemg12f  36253  cdlemg13a  36256  cdlemg17a  36266  cdlemg17dALTN  36269  cdlemg18b  36284  cdlemg19a  36288  cdlemg27a  36297  cdlemg27b  36301  cdlemg33b0  36306  cdlemg33a  36311  cdlemg35  36318  trlcolem  36331  cdlemg42  36334  cdlemg46  36340  trljco  36345  tendopltp  36385  cdlemh1  36420  cdlemh2  36421  cdlemi1  36423  cdlemi  36425  cdlemk3  36438  cdlemk10  36448  cdlemk11  36454  cdlemk15  36460  cdlemk1u  36464  cdlemk5u  36466  cdlemk11u  36476  cdlemk39  36521  cdlemkid1  36527  cdlemk50  36557  cdlemk51  36558  erngdvlem3-rN  36603  tendocnv  36627  tendospcanN  36629  dialss  36652  dia2dimlem1  36670  dia2dimlem2  36671  dia2dimlem3  36672  dia2dimlem10  36679  dia2dimlem12  36681  dvhvaddass  36703  dvhlveclem  36714  cdlemm10N  36724  doca2N  36732  djajN  36743  dib1dim2  36774  diblss  36776  diclspsn  36800  cdlemn2  36801  cdlemn10  36812  dihjustlem  36822  dihord1  36824  dihord2a  36825  dihord2pre2  36832  dib2dim  36849  dih2dimb  36850  dih2dimbALTN  36851  dihopelvalcpre  36854  dihord5b  36865  dihord6b  36866  dihord5apre  36868  dihmeetlem1N  36896  dihglblem5apreN  36897  dihglblem2N  36900  dihglbcpreN  36906  dihmeetbclemN  36910  dihmeetlem3N  36911  dihmeetlem6  36915  dih1dimatlem  36935  djhcvat42  37021  dihjatcclem1  37024  dihjatcclem4  37027  dvh4dimat  37044  lcfl7lem  37105  lclkrlem2m  37125  lcfrlem1  37148  lcdvsass  37213  baerlem3lem1  37313  baerlem5alem1  37314  baerlem5blem1  37315  mapdh6gN  37348  mapdh6hN  37349  hdmap1l6g  37423  hdmap1l6h  37424  hdmapneg  37455  hdmap14lem8  37484  hgmapadd  37503  hgmapmul  37504  hgmapvvlem1  37532  irrapxlem5  37707  aomclem2  37942  isnumbasgrplem2  37991  mpaaeu  38037  mendring  38079  mendlmod  38080  relexpnul  38287  caofcan  38839  disjiun2  39540  wessf1ornlem  39685  fisupclrnmpt  39935  limsupequzlem  40272  cnrefiisplem  40373  stoweidlem18  40553  stoweidlem41  40576  stoweidlem45  40580  stoweidlem55  40590  fourierdlem25  40667  fourierdlem31  40673  fourierdlem37  40679  fourierdlem42  40684  etransclem48  40817  ioorrnopnlem  40842  issalgend  40874  sge0iunmptlemfi  40948  hoicvr  41083  hoidmvlelem2  41131  iunhoiioolem  41210  vonioolem1  41215  prmdvdsfmtnof1lem1  41821  prmdvdsfmtnof  41823  sgprmdvdsmersenne  41846  perfectALTVlem1  41955  perfectALTVlem2  41956  rnglz  42209  ssnn0ssfz  42452  zlmodzxzsub  42463  invginvrid  42473  lmodvsmdi  42488  ply1sclrmsm  42496  lincsum  42543  lincscm  42544  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  ldepsprlem  42586  lincresunit3lem1  42593  lincresunit3lem2  42594  isldepslvec2  42599  relogbmulbexp  42680
 Copyright terms: Public domain W3C validator