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

Theorem syl13anc 1484
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl13anc.5 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
Assertion
Ref Expression
syl13anc (𝜑𝜂)

Proof of Theorem syl13anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1151 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 575 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  syl23anc  1489  syl33anc  1497  disjxiun  4839  wereu2  5306  ordelord  5956  caovassd  7061  caovcand  7064  caovordid  7068  caovordd  7070  caovdid  7077  caovdird  7080  swoer  8007  swoord1  8008  swoord2  8009  frfi  8442  indexfi  8511  ssfii  8562  elfiun  8573  suplub2  8604  supgtoreq  8613  infltoreq  8645  wemaplem2  8689  htalem  9004  cofsmo  9374  alephsing  9381  sornom  9382  axdc3lem4  9558  zorn2lem1  9601  ttukeylem6  9619  ttukeylem7  9620  prlem934  10138  supfirege  11292  suprfinzcl  11756  ssfzunsn  12608  fzosubel3  12751  fsuppmapnn0fiublem  13011  seqsplit  13055  seqcaopr  13059  ccatass  13583  wrdcctswrd  13687  wrdeqs1cat  13696  splid  13726  spllen  13727  splfv1  13728  splfv2a  13729  splval2  13730  swrds2  13907  isercolllem2  14617  fsumiun  14773  zprod  14886  lcmftp  15566  pcgcd1  15796  cshwsidrepswmod0  16011  cshwshashlem2  16013  cshwsdisj  16015  firest  16296  iscatd2  16544  posasymb  17155  joinle  17217  meetle  17231  lattrd  17261  latleeqj1  17266  latjlej1  17268  latjlej12  17270  latnlej2  17274  latjidm  17277  latleeqm1  17282  latmlem1  17284  latmlem12  17286  latmidm  17289  latledi  17292  latjass  17298  latj12  17299  latj13  17301  latj31  17302  latjrot  17303  latj4  17304  mod1ile  17308  lubun  17326  clatleglb  17329  latdisdlem  17392  mnd32g  17508  mnd12g  17509  mnd4g  17510  ismndd  17516  prdsmndd  17526  imasmnd  17531  mrcmndind  17569  gsumspl  17584  grpasscan2  17682  grpidrcan  17683  grpidlcan  17684  grpinvinv  17685  grplmulf1o  17692  grpinvssd  17695  grpinvadd  17696  grpsubrcan  17699  grpsubadd  17706  grpaddsubass  17708  grppncan  17709  grpsubsub4  17711  grppnpcan2  17712  grpnpncan  17713  grpnpncan0  17714  grpnnncan2  17715  dfgrp3lem  17716  dfgrp3  17717  grplactcnv  17721  imasgrp  17734  mhmmnd  17740  mulgaddcomlem  17765  mulgaddcom  17766  mulgnn0dir  17772  mulgdirlem  17773  mulgneg2  17776  mulgnnass  17777  mulgnn0ass  17778  mulgass  17779  mulgmodid  17781  nsgconj  17827  isnsg3  17828  nmzsubg  17835  ssnmz  17836  eqger  17844  eqgcpbl  17848  conjghm  17891  conjnmz  17894  conjnmzb  17895  subgga  17932  gass  17933  gasubg  17934  galcan  17936  gacan  17937  gapm  17938  gaorber  17940  gastacl  17941  gastacos  17942  cntzsubm  17967  cntzsubg  17968  oppgmnd  17983  symggen  18089  odmodnn0  18158  mndodconglem  18159  odmod  18164  odcong  18167  odmulgid  18170  odbezout  18174  gexdvdsi  18197  gexdvds  18198  sylow1lem2  18213  sylow1lem4  18215  sylow2blem1  18234  sylow2blem2  18235  sylow2blem3  18236  sylow3lem1  18241  sylow3lem2  18242  lsmass  18282  lsmmod  18287  lsmdisj2  18294  subgdisj1  18303  efgredleme  18355  efgredlemc  18357  efgcpbllemb  18367  frgp0  18372  frgpuplem  18384  abl32  18413  abladdsub4  18418  abladdsub  18419  ablpncan2  18420  ablsubsub  18422  mulgdi  18431  mulgsubdi  18434  odadd1  18450  odadd2  18451  gex2abl  18453  oddvdssubg  18457  cygabl  18491  telgsumfzslem  18585  ablfacrp  18665  pgpfac1lem2  18674  pgpfac1lem3a  18675  pgpfac1lem3  18676  pgpfac1lem4  18677  srgmulgass  18731  srgpcomp  18732  srgpcompp  18733  srgpcomppsc  18734  srgbinomlem3  18742  srgbinomlem4  18743  srgbinomlem  18744  csrgbinom  18746  ringadd2  18775  rngo2times  18776  ringcom  18779  ringlz  18787  ringrz  18788  ringnegl  18794  rngnegr  18795  ringmneg1  18796  ringmneg2  18797  ringsubdi  18799  rngsubdir  18800  mulgass2  18801  prdsringd  18812  imasring  18819  opprring  18831  mulgass3  18837  dvdsrtr  18852  dvdsrmul1  18853  unitgrp  18867  dvrass  18890  dvrcan1  18891  dvrcan3  18892  irredrmul  18907  drngmul0or  18970  subrginv  18998  cntzsubr  19014  lmod0vs  19098  lmodvs0  19099  lmodvsmmulgdi  19100  lmodfopne  19103  lmodvneg1  19108  lmodvsneg  19109  lmodcom  19111  lmodsubvs  19121  lmodsubdi  19122  lmodsubdir  19123  lssvsubcl  19146  lssvacl  19159  lssvscl  19160  islss3  19164  lss1d  19168  lssintcl  19169  prdslmodd  19174  lmodvsinv  19241  lmodvsinv2  19242  lmhmplusg  19249  lmhmvsca  19250  lsmcl  19288  pj1lmhm  19305  lvecvs0or  19313  lssvs0or  19315  lvecinv  19318  lspsnvs  19319  lspfixed  19333  lspfixedOLD  19334  lspexch  19335  lspsolvlem  19348  lspsolv  19349  lssacsex  19350  lspsnat  19351  lsppratlem1  19354  lsppratlem3  19356  lsppratlem4  19357  lbsextlem2  19366  lbsextlem4  19368  sralmod  19394  2idlcpbl  19441  unitrrg  19500  assa2ass  19529  issubassa  19531  sraassa  19532  asclghm  19545  asclmul1  19546  asclmul2  19547  asclrhm  19549  assamulgscmlem2  19556  psrbagcon  19578  psrbagconcl  19580  psrbagconf1o  19581  gsumbagdiaglem  19582  psrmulcllem  19594  psrlidm  19610  psrridm  19611  psrass1  19612  psrdi  19613  psrdir  19614  psrass23l  19615  psrcom  19616  mplmon2mul  19707  evlslem1  19721  coe1subfv  19842  lply1binomsc  19883  mulgrhm  20052  cygznlem3  20123  evpmodpmf1o  20148  ipdi  20193  ip2di  20194  ipsubdir  20195  ipsubdi  20196  ip2subdi  20197  ipassr  20199  ipassr2  20200  ip2eq  20206  ocvlss  20224  lsmcss  20244  frlmphl  20328  frlmup1  20345  mamuass  20416  mamudi  20417  mamudir  20418  mamuvs1  20419  mamuvs2  20420  dmatmul  20512  dmatsubcl  20513  scmataddcl  20531  smatvscl  20539  scmatghm  20548  mavmulass  20564  mdetrlin  20617  mdetrsca  20618  mdetralt  20623  mdetunilem7  20633  mdetuni0  20636  matinv  20693  pm2mpghm  20832  chpscmatgsummon  20861  chfacfscmulgsum  20876  chfacfpmmulgsum  20880  chfacfpmmulgsum2  20881  cpmadugsumlemB  20890  cpmadugsumlemC  20891  cpmadugsumlemF  20892  iinopn  20918  subbascn  21270  cnhaus  21370  nrmsep2  21372  nrmsep  21373  regsep2  21392  isreg2  21393  hauscmplem  21421  1stcfb  21460  2ndcctbss  21470  ptbasfi  21596  pthaus  21653  txtube  21655  txhaus  21662  xkohaus  21668  kqnrmlem1  21758  kqnrmlem2  21759  nrmr0reg  21764  nrmhmph  21809  fbssint  21853  infil  21878  fgabs  21894  filconn  21898  filuni  21900  trfil2  21902  trfg  21906  ufprim  21924  elfm3  21965  rnelfm  21968  fmfnfmlem2  21970  fmfnfmlem4  21972  hausflimi  21995  hauspwpwf1  22002  fclsneii  22032  supnfcls  22035  flimfnfcls  22043  fclscmpi  22044  alexsublem  22059  ghmcnp  22129  qustgpopn  22134  psmetsym  22326  psmettri  22327  psmetge0  22328  psmetres2  22330  xmetge0  22360  xmetsym  22363  xmettri  22367  xmetres2  22377  prdsxmetlem  22384  prdsmet  22386  imasdsf1olem  22389  imasf1oxmet  22391  bldisj  22414  xblss2ps  22417  xblss2  22418  xmeter  22449  prdsbl  22507  metustexhalf  22572  metust  22574  nrmmetd  22590  ngpsubcan  22629  nmmtri  22637  nmrtri  22639  ngptgp  22651  nlmvscnlem2  22700  nrginvrcnlem  22706  metdcnlem  22850  clmvs2  23104  clmmulg  23111  clmnegneg  23114  clmnegsubdi2  23115  clmsub4  23116  cvsmuleqdivd  23144  cvsdiveqd  23145  ncvspi  23166  cphabscl  23195  cphsqrtcl2  23196  cphsqrtcl3  23197  cphnmf  23205  cph2ass  23223  cphassi  23224  cphassir  23225  ipcau2  23243  tchcphlem2  23245  ipcnlem2  23253  cfilfcls  23282  iscau3  23286  iscmet3lem2  23300  iscmet3  23301  relcmpcmet  23325  minveclem2  23407  minveclem4  23413  pjthlem1  23418  pjthlem2  23419  uniioombllem4  23565  dyadmax  23577  itg1addlem4  23678  itg1climres  23693  ply1divex  24108  aalioulem2  24300  amgmlem  24928  dvdsppwf1o  25124  perfect1  25165  perfectlem1  25166  perfectlem2  25167  dchrptlem2  25202  colline  25756  ttgcontlem1  25977  axcontlem9  26064  eengtrkg  26077  eengtrkge  26078  nbfusgrlevtxm2  26494  nbusgrvtxm1  26495  elwwlks2ons3im  27092  elwwlks2ons3OLD  27094  usgr2wspthon  27105  clwwlknclwwlkdifnum  27119  clwwlknclwwlkdifnumOLD  27121  numclwwlk5  27574  grpoidinvlem4  27688  grpoinvop  27714  grponpcan  27724  vcm  27757  nvmul0or  27831  nvpncan2  27834  nvdif  27847  nvabs  27853  smcnlem  27878  lnomul  27941  minvecolem2  28057  superpos  29539  ssnnssfz  29874  omndmul2  30035  omndmul3  30036  ogrpaddltbi  30042  ogrpaddltrbid  30044  ogrpsublt  30045  ogrpinvlt  30047  isarchi3  30064  archirngz  30066  archiabllem1a  30068  archiabllem1  30070  archiabllem2a  30071  archiabllem2c  30072  slmdvs0  30101  gsumvsca1  30105  gsumvsca2  30106  dvrdir  30113  rdivmuldivd  30114  dvrcan5  30116  ornglmullt  30130  isarchiofld  30140  rhmdvd  30144  rhmunitinv  30145  psgnfzto1stlem  30173  pmtridfv1  30180  pmtridfv2  30181  mdetpmtr1  30212  mdetpmtr12  30214  mdetlap  30221  locfinref  30231  metideq  30259  metider  30260  pstmxmet  30263  lmxrge0  30321  qqhghm  30355  qqhrhm  30356  ispisys2  30539  rossros  30566  measdivcst  30611  oddpwdc  30739  ballotlemiex  30886  wrdsplex  30941  cvmopnlem  31581  cvmliftmolem2  31585  cvmliftlem6  31593  cvmliftlem8  31595  cvmliftlem9  31596  cvmlift2lem9  31614  cvmlift3lem2  31623  cvmlift3lem6  31627  cvmlift3lem7  31628  cvmlift3lem9  31630  sotrd  31975  frpomin  32057  nodense  32161  nosupfv  32171  noetalem5  32186  cgrtriv  32428  cgrdegen  32430  cgrextend  32434  segconeq  32436  btwntriv2  32438  btwncomand  32441  btwntriv1  32442  btwnintr  32445  btwnexch3  32446  btwnouttr  32450  btwnexch  32451  trisegint  32454  ifscgr  32470  btwnxfr  32482  colineartriv1  32493  colineartriv2  32494  colinearxfr  32501  fscgr  32506  lineid  32509  idinside  32510  endofsegidand  32512  btwnconn1lem5  32517  btwnconn1lem7  32519  btwnconn1lem11  32523  btwnconn1lem12  32524  btwnconn1lem13  32525  brsegle2  32535  segleantisym  32541  broutsideof2  32548  btwnoutside  32551  outsideoftr  32555  outsideofeq  32556  outsideofeu  32557  outsidele  32558  lineunray  32573  lineelsb2  32574  linecom  32576  linethru  32579  neibastop1  32673  lindsenlbs  33715  matunitlindflem1  33716  poimirlem28  33748  poimirlem32  33752  heicant  33755  mettrifi  33862  isbnd3  33892  heibor1lem  33917  bfplem2  33931  ghomdiv  34000  rngo2  34015  rngolz  34030  rngorz  34031  zerdivemp1x  34055  lfladdcl  34849  lflvscl  34855  eqlkr3  34879  lkrlsp  34880  lshpkrlem4  34891  oldmm1  34995  olj01  35003  latmassOLD  35007  latm32  35009  latmrot  35010  latm4  35011  olm01  35014  cmtcomlemN  35026  cmtbr3N  35032  cmtbr4N  35033  lecmtN  35034  omlfh1N  35036  atlen0  35088  atnle  35095  atlatmstc  35097  atlatle  35098  cvlexchb1  35108  cvlcvr1  35117  ishlat3N  35132  hlatjass  35148  hlatj12  35149  hlatj32  35150  hlsupr2  35165  hlhgt2  35167  hl0lt1N  35168  hlrelat  35180  hlrelat2  35181  exatleN  35182  hlrelat3  35190  cvrval5  35193  cvrexchlem  35197  cvratlem  35199  cvrat  35200  atcvr0eq  35204  lnnat  35205  atlt  35215  atlelt  35216  2atlt  35217  atexchltN  35219  cvrat3  35220  2atjm  35223  atbtwn  35224  4noncolr3  35231  athgt  35234  3dimlem3a  35238  3dimlem3OLDN  35240  3dimlem4a  35241  3dimlem4OLDN  35243  3dim1  35245  3dim2  35246  1cvratex  35251  ps-1  35255  ps-2  35256  hlatexch3N  35258  hlatexch4  35259  ps-2b  35260  3atlem1  35261  3atlem2  35262  3atlem5  35265  3atlem6  35266  llnnleat  35291  llncmp  35300  2at0mat0  35303  2atmat0  35304  2atm  35305  lplni2  35315  lvolex3N  35316  lplnnle2at  35319  lplnnleat  35320  lplnnlelln  35321  2atnelpln  35322  llncvrlpln  35336  2atmat  35339  lplncmp  35340  lplnexllnN  35342  2llnjaN  35344  2llnm4  35348  2llnmeqat  35349  lvolnle3at  35360  lvolnleat  35361  2atnelvolN  35365  islvol2aN  35370  4atlem3  35374  4atlem3a  35375  4atlem3b  35376  4atlem4a  35377  4atlem4b  35378  4atlem4c  35379  4atlem4d  35380  4atlem10  35384  4atlem11b  35386  4atlem11  35387  4atlem12b  35389  4atlem12  35390  4at2  35392  lplncvrlvol  35394  lvolcmp  35395  2lplnja  35397  dalemqrprot  35426  dalemply  35432  dalemsly  35433  dalemrot  35435  dalemrotyz  35436  dalem1  35437  dalemcea  35438  dalem3  35442  dalem5  35445  dalem8  35448  dalem-cly  35449  dalem11  35452  dalem12  35453  dalem16  35457  dalem17  35458  dalem18  35459  dalem21  35472  dalem24  35475  dalem25  35476  dalem38  35488  dalem39  35489  dalem44  35494  dalem54  35504  dalem55  35505  dalem57  35507  dalem58  35508  dalem59  35509  dalem60  35510  dath2  35515  2atm2atN  35563  2llnma1b  35564  2llnma3r  35566  cdlema1N  35569  cdlemblem  35571  paddasslem5  35602  paddasslem10  35607  paddasslem12  35609  paddasslem13  35610  paddass  35616  padd12N  35617  padd4N  35618  paddss  35623  pmodlem1  35624  pmodl42N  35629  pmapjoin  35630  pmapjlln1  35633  atmod1i2  35637  llnmod1i2  35638  llnexchb2  35647  dalawlem2  35650  dalawlem3  35651  dalawlem5  35653  dalawlem6  35654  dalawlem7  35655  dalawlem8  35656  dalawlem11  35659  dalawlem12  35660  dalawlem13  35661  pclunN  35676  osumcllem1N  35734  pexmidlem3N  35750  lhp2lt  35779  lhp0lt  35781  lhpexle2lem  35787  lhpexle3lem  35789  lhpocnle  35794  lhpj1  35800  lhpmcvr4N  35804  lhp2at0  35810  lhpat3  35824  4atexlemtlw  35845  4atexlemc  35847  4atexlemnclw  35848  4atexlemcnd  35850  lautcvr  35870  lautj  35871  lautm  35872  ltrnm  35909  ltrnj  35910  ltrncvr  35911  trlval3  35966  cdlemc5  35974  cdlemd2  35978  cdlemd3  35979  cdleme0e  35996  cdleme1  36006  cdleme3c  36009  cdleme3g  36013  cdleme3h  36014  cdleme3  36016  cdleme5  36019  cdleme7c  36024  cdleme7d  36025  cdleme7e  36026  cdleme7ga  36027  cdleme7  36028  cdleme9  36032  cdleme11c  36040  cdleme11g  36044  cdleme11k  36047  cdleme11  36049  cdleme12  36050  cdleme15b  36054  cdleme15d  36056  cdleme16d  36060  cdleme16e  36061  cdleme16f  36062  cdleme17b  36066  cdleme18b  36071  cdleme22gb  36073  cdlemednpq  36078  cdleme19a  36082  cdleme20aN  36088  cdleme20bN  36089  cdleme20c  36090  cdleme20d  36091  cdleme20j  36097  cdleme21c  36106  cdleme22aa  36118  cdleme22b  36120  cdleme22cN  36121  cdleme22d  36122  cdleme22e  36123  cdleme22eALTN  36124  cdleme23b  36129  cdleme23c  36130  cdleme28a  36149  cdleme30a  36157  cdlemefs29bpre0N  36195  cdlemefs29bpre1N  36196  cdlemefs29cpre1N  36197  cdlemefs29clN  36198  cdlemefs32fvaN  36201  cdlemefs32fva1  36202  cdleme32b  36221  cdleme32c  36222  cdleme32e  36224  cdleme35a  36227  cdleme35fnpq  36228  cdleme35b  36229  cdleme35f  36233  cdleme36a  36239  cdleme36m  36240  cdleme37m  36241  cdleme39a  36244  cdleme42c  36251  cdleme42i  36262  cdleme42keg  36265  cdleme42mgN  36267  cdleme48bw  36281  cdlemeg46fjgN  36300  cdlemeg46fjv  36302  cdlemeg46req  36308  cdleme50trn1  36328  cdlemf1  36340  cdlemf2  36341  cdlemg1cex  36367  cdlemg2fv2  36379  cdlemg7fvbwN  36386  cdlemg4c  36391  cdlemg4  36396  cdlemg6c  36399  cdlemg8b  36407  cdlemg10c  36418  cdlemg10  36420  cdlemg11b  36421  cdlemg12f  36427  cdlemg13a  36430  cdlemg17a  36440  cdlemg17dALTN  36443  cdlemg18b  36458  cdlemg19a  36462  cdlemg27a  36471  cdlemg27b  36475  cdlemg33b0  36480  cdlemg33a  36485  cdlemg35  36492  trlcolem  36505  cdlemg42  36508  cdlemg46  36514  trljco  36519  tendopltp  36559  cdlemh1  36594  cdlemh2  36595  cdlemi1  36597  cdlemi  36599  cdlemk3  36612  cdlemk10  36622  cdlemk11  36628  cdlemk15  36634  cdlemk1u  36638  cdlemk5u  36640  cdlemk11u  36650  cdlemk39  36695  cdlemkid1  36701  cdlemk50  36731  cdlemk51  36732  erngdvlem3-rN  36777  tendocnv  36800  tendospcanN  36802  dialss  36825  dia2dimlem1  36843  dia2dimlem2  36844  dia2dimlem3  36845  dia2dimlem10  36852  dia2dimlem12  36854  dvhvaddass  36876  dvhlveclem  36887  cdlemm10N  36897  doca2N  36905  djajN  36916  dib1dim2  36947  diblss  36949  diclspsn  36973  cdlemn2  36974  cdlemn10  36985  dihjustlem  36995  dihord1  36997  dihord2a  36998  dihord2pre2  37005  dib2dim  37022  dih2dimb  37023  dih2dimbALTN  37024  dihopelvalcpre  37027  dihord5b  37038  dihord6b  37039  dihord5apre  37041  dihmeetlem1N  37069  dihglblem5apreN  37070  dihglblem2N  37073  dihglbcpreN  37079  dihmeetbclemN  37083  dihmeetlem3N  37084  dihmeetlem6  37088  dih1dimatlem  37108  djhcvat42  37194  dihjatcclem1  37197  dihjatcclem4  37200  dvh4dimat  37217  lcfl7lem  37278  lclkrlem2m  37298  lcfrlem1  37321  lcdvsass  37386  baerlem3lem1  37486  baerlem5alem1  37487  baerlem5blem1  37488  mapdh6gN  37521  mapdh6hN  37522  hdmap1l6g  37595  hdmap1l6h  37596  hdmapneg  37625  hdmap14lem8  37654  hgmapadd  37673  hgmapmul  37674  hgmapvvlem1  37702  irrapxlem5  37890  aomclem2  38124  isnumbasgrplem2  38173  mpaaeu  38219  mendring  38261  mendlmod  38262  relexpnul  38468  caofcan  39020  disjiun2  39717  wessf1ornlem  39858  fisupclrnmpt  40099  limsupequzlem  40432  cnrefiisplem  40533  stoweidlem18  40712  stoweidlem41  40735  stoweidlem45  40739  stoweidlem55  40749  fourierdlem25  40826  fourierdlem31  40832  fourierdlem37  40838  fourierdlem42  40843  etransclem48  40976  ioorrnopnlem  41001  issalgend  41033  sge0iunmptlemfi  41107  hoicvr  41242  hoidmvlelem2  41290  iunhoiioolem  41369  vonioolem1  41374  prmdvdsfmtnof1lem1  42069  prmdvdsfmtnof  42071  sgprmdvdsmersenne  42094  perfectALTVlem1  42203  perfectALTVlem2  42204  rnglz  42450  ssnn0ssfz  42693  zlmodzxzsub  42704  invginvrid  42714  lmodvsmdi  42729  ply1sclrmsm  42737  lincsum  42784  lincscm  42785  lindslinindimp2lem4  42816  lindslinindsimp2lem5  42817  ldepsprlem  42827  lincresunit3lem1  42834  lincresunit3lem2  42835  isldepslvec2  42840  relogbmulbexp  42921
  Copyright terms: Public domain W3C validator