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

Theorem syl13anc 1320
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 1235 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 691 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  syl23anc  1325  syl33anc  1333  disjxiun  4574  disjxiunOLD  4575  wereu2  5025  ordelord  5648  caovassd  6709  caovcand  6712  caovordid  6716  caovordd  6718  caovdid  6725  caovdird  6728  swoer  7637  swoord1  7638  swoord2  7639  frfi  8068  indexfi  8135  ssfii  8186  elfiun  8197  suplub2  8228  supgtoreq  8237  infltoreq  8269  wemaplem2  8313  htalem  8620  cofsmo  8952  alephsing  8959  sornom  8960  axdc3lem4  9136  zorn2lem1  9179  ttukeylem6  9197  ttukeylem7  9198  prlem934  9712  supfirege  10859  suprfinzcl  11327  fzosubel3  12354  fsuppmapnn0fiublem  12609  seqsplit  12654  seqcaopr  12658  ccatass  13173  wrdcctswrd  13266  wrdeqs1cat  13275  splid  13304  spllen  13305  splfv1  13306  splfv2a  13307  splval2  13308  swrds2  13482  isercolllem2  14193  fsumiun  14343  zprod  14455  lcmftp  15136  pcgcd1  15368  cshwsidrepswmod0  15588  cshwshashlem2  15590  cshwsdisj  15592  firest  15865  iscatd2  16114  posasymb  16724  joinle  16786  meetle  16800  lattrd  16830  latleeqj1  16835  latjlej1  16837  latjlej12  16839  latnlej2  16843  latjidm  16846  latleeqm1  16851  latmlem1  16853  latmlem12  16855  latmidm  16858  latledi  16861  latjass  16867  latj12  16868  latj13  16870  latj31  16871  latjrot  16872  latj4  16873  mod1ile  16877  lubun  16895  clatleglb  16898  latdisdlem  16961  mnd32g  17077  mnd12g  17078  mnd4g  17079  ismndd  17085  prdsmndd  17095  imasmnd  17100  mrcmndind  17138  gsumspl  17153  grpasscan2  17251  grpidrcan  17252  grpidlcan  17253  grpinvinv  17254  grplmulf1o  17261  grpinvssd  17264  grpinvadd  17265  grpsubrcan  17268  grpsubadd  17275  grpaddsubass  17277  grppncan  17278  grpsubsub4  17280  grppnpcan2  17281  grpnpncan  17282  grpnpncan0  17283  grpnnncan2  17284  dfgrp3lem  17285  dfgrp3  17286  grplactcnv  17290  imasgrp  17303  mhmmnd  17309  mulgaddcomlem  17335  mulgaddcom  17336  mulgnn0dir  17343  mulgdirlem  17344  mulgneg2  17347  mulgnnass  17348  mulgnnassOLD  17349  mulgnn0ass  17350  mulgass  17351  mulgmodid  17353  nsgconj  17399  isnsg3  17400  nmzsubg  17407  ssnmz  17408  eqger  17416  eqgcpbl  17420  conjghm  17463  conjnmz  17466  conjnmzb  17467  subgga  17505  gass  17506  gasubg  17507  galcan  17509  gacan  17510  gapm  17511  gaorber  17513  gastacl  17514  gastacos  17515  cntzsubm  17540  cntzsubg  17541  oppgmnd  17556  symggen  17662  odmodnn0  17731  mndodconglem  17732  odmod  17737  odcong  17740  odmulgid  17743  odbezout  17747  gexdvdsi  17770  gexdvds  17771  sylow1lem2  17786  sylow1lem4  17788  sylow2blem1  17807  sylow2blem2  17808  sylow2blem3  17809  sylow3lem1  17814  sylow3lem2  17815  lsmass  17855  lsmmod  17860  lsmdisj2  17867  subgdisj1  17876  efgredleme  17928  efgredlemc  17930  efgcpbllemb  17940  frgp0  17945  frgpuplem  17957  abl32  17986  abladdsub4  17991  abladdsub  17992  ablpncan2  17993  ablsubsub  17995  mulgdi  18004  mulgsubdi  18007  odadd1  18023  odadd2  18024  gex2abl  18026  oddvdssubg  18030  cygabl  18064  telgsumfzslem  18157  ablfacrp  18237  pgpfac1lem2  18246  pgpfac1lem3a  18247  pgpfac1lem3  18248  pgpfac1lem4  18249  srgmulgass  18303  srgpcomp  18304  srgpcompp  18305  srgpcomppsc  18306  srgbinomlem3  18314  srgbinomlem4  18315  srgbinomlem  18316  csrgbinom  18318  ringadd2  18347  rngo2times  18348  ringcom  18351  ringlz  18359  ringrz  18360  ringnegl  18366  rngnegr  18367  ringmneg1  18368  ringmneg2  18369  ringsubdi  18371  rngsubdir  18372  mulgass2  18373  prdsringd  18384  imasring  18391  opprring  18403  mulgass3  18409  dvdsrtr  18424  dvdsrmul1  18425  unitgrp  18439  dvrass  18462  dvrcan1  18463  dvrcan3  18464  irredrmul  18479  drngmul0or  18540  subrginv  18568  cntzsubr  18584  lmod0vs  18668  lmodvs0  18669  lmodvsmmulgdi  18670  lmodfopne  18673  lmodvneg1  18678  lmodvsneg  18679  lmodcom  18681  lmodsubvs  18691  lmodsubdi  18692  lmodsubdir  18693  lssvsubcl  18714  lssvacl  18724  lssvscl  18725  islss3  18729  lss1d  18733  lssintcl  18734  prdslmodd  18739  lmodvsinv  18806  lmodvsinv2  18807  lmhmplusg  18814  lmhmvsca  18815  lsmcl  18853  pj1lmhm  18870  lvecvs0or  18878  lssvs0or  18880  lvecinv  18883  lspsnvs  18884  lspfixed  18898  lspexch  18899  lspsolvlem  18912  lspsolv  18913  lssacsex  18914  lspsnat  18915  lsppratlem1  18917  lsppratlem3  18919  lsppratlem4  18920  lbsextlem2  18929  lbsextlem4  18931  sralmod  18957  2idlcpbl  19004  unitrrg  19063  assa2ass  19092  issubassa  19094  sraassa  19095  asclghm  19108  asclmul1  19109  asclmul2  19110  asclrhm  19112  assamulgscmlem2  19119  psrbagcon  19141  psrbagconcl  19143  psrbagconf1o  19144  gsumbagdiaglem  19145  psrmulcllem  19157  psrlidm  19173  psrridm  19174  psrass1  19175  psrdi  19176  psrdir  19177  psrass23l  19178  psrcom  19179  mplmon2mul  19271  evlslem1  19285  coe1subfv  19406  lply1binomsc  19447  mulgrhm  19613  cygznlem3  19685  evpmodpmf1o  19709  ipdi  19752  ip2di  19753  ipsubdir  19754  ipsubdi  19755  ip2subdi  19756  ipassr  19758  ipassr2  19759  ip2eq  19765  ocvlss  19783  lsmcss  19803  frlmphl  19887  frlmup1  19904  mamuass  19975  mamudi  19976  mamudir  19977  mamuvs1  19978  mamuvs2  19979  dmatmul  20070  dmatsubcl  20071  scmataddcl  20089  smatvscl  20097  scmatghm  20106  mavmulass  20122  mdetrlin  20175  mdetrsca  20176  mdetralt  20181  mdetunilem7  20191  mdetuni0  20194  matinv  20250  pm2mpghm  20388  chpscmatgsummon  20417  chfacfscmulgsum  20432  chfacfpmmulgsum  20436  chfacfpmmulgsum2  20437  cpmadugsumlemB  20446  cpmadugsumlemC  20447  cpmadugsumlemF  20448  iinopn  20480  subbascn  20816  cnhaus  20916  nrmsep2  20918  nrmsep  20919  regsep2  20938  isreg2  20939  hauscmplem  20967  1stcfb  21006  2ndcctbss  21016  ptbasfi  21142  pthaus  21199  txtube  21201  txhaus  21208  xkohaus  21214  kqnrmlem1  21304  kqnrmlem2  21305  nrmr0reg  21310  nrmhmph  21355  fbssint  21400  infil  21425  fgabs  21441  filcon  21445  filuni  21447  trfil2  21449  trfg  21453  ufprim  21471  elfm3  21512  rnelfm  21515  fmfnfmlem2  21517  fmfnfmlem4  21519  hausflimi  21542  hauspwpwf1  21549  fclsneii  21579  supnfcls  21582  flimfnfcls  21590  fclscmpi  21591  alexsublem  21606  ghmcnp  21676  qustgpopn  21681  psmetsym  21873  psmettri  21874  psmetge0  21875  psmetres2  21877  xmetge0  21907  xmetsym  21910  xmettri  21914  xmetres2  21924  prdsxmetlem  21931  prdsmet  21933  imasdsf1olem  21936  imasf1oxmet  21938  bldisj  21961  xblss2ps  21964  xblss2  21965  xmeter  21996  prdsbl  22054  metustexhalf  22119  metust  22121  nrmmetd  22137  ngpsubcan  22176  nmmtri  22184  nmrtri  22186  ngptgp  22198  nlmvscnlem2  22247  nrginvrcnlem  22253  metdcnlem  22395  clmvs2  22650  clmmulg  22657  clmnegneg  22660  clmnegsubdi2  22661  clmsub4  22662  cvsmuleqdivd  22690  cvsdiveqd  22691  ncvspi  22709  cphabscl  22738  cphsqrtcl2  22739  cphsqrtcl3  22740  cphnmf  22748  cph2ass  22766  cphassi  22767  cphassir  22768  ipcau2  22786  tchcphlem2  22788  ipcnlem2  22796  cfilfcls  22825  iscau3  22829  iscmet3lem2  22843  iscmet3  22844  relcmpcmet  22868  minveclem2  22950  minveclem4  22956  pjthlem1  22961  pjthlem2  22962  uniioombllem4  23105  dyadmax  23117  itg1addlem4  23217  itg1climres  23232  ply1divex  23645  aalioulem2  23837  amgmlem  24461  dvdsppwf1o  24657  perfect1  24698  perfectlem1  24699  perfectlem2  24700  dchrptlem2  24735  colline  25290  ttgcontlem1  25511  axcontlem9  25598  eengtrkg  25611  eengtrkge  25612  4cycl4dv4e  25990  el2spthonot0  26192  usg2spthonot1  26211  clwlknclwlkdifnum  26282  eupa0  26295  eupares  26296  eupap1  26297  frg2woteu  26376  numclwwlk5  26433  numclwwlk6  26434  grpoidinvlem4  26539  grpoinvop  26565  grponpcan  26575  vcm  26609  nvmul0or  26683  nvpncan2  26686  nvdif  26699  nvabs  26705  smcnlem  26730  lnomul  26793  minvecolem2  26909  superpos  28391  ssnnssfz  28731  omndmul2  28837  omndmul3  28838  ogrpaddltbi  28844  ogrpaddltrbid  28846  ogrpsublt  28847  ogrpinvlt  28849  isarchi3  28866  archirngz  28868  archiabllem1a  28870  archiabllem1  28872  archiabllem2a  28873  archiabllem2c  28874  slmdvs0  28903  gsumvsca1  28907  gsumvsca2  28908  dvrdir  28915  rdivmuldivd  28916  dvrcan5  28918  ornglmullt  28932  isarchiofld  28942  rhmdvd  28946  rhmunitinv  28947  psgnfzto1stlem  28975  mdetpmtr1  29011  mdetpmtr12  29013  mdetlap  29020  locfinref  29030  metideq  29058  metider  29059  pstmxmet  29062  lmxrge0  29120  qqhghm  29154  qqhrhm  29155  ispisys2  29337  rossros  29364  measdivcst  29409  oddpwdc  29537  ballotlemiex  29684  wrdsplex  29738  cvmopnlem  30308  cvmliftmolem2  30312  cvmliftlem6  30320  cvmliftlem8  30322  cvmliftlem9  30323  cvmlift2lem9  30341  cvmlift3lem2  30350  cvmlift3lem6  30354  cvmlift3lem7  30355  cvmlift3lem9  30357  nodense  30882  cgrtriv  31073  cgrdegen  31075  cgrextend  31079  segconeq  31081  btwntriv2  31083  btwncomand  31086  btwntriv1  31087  btwnintr  31090  btwnexch3  31091  btwnouttr  31095  btwnexch  31096  trisegint  31099  ifscgr  31115  btwnxfr  31127  colineartriv1  31138  colineartriv2  31139  colinearxfr  31146  fscgr  31151  lineid  31154  idinside  31155  endofsegidand  31157  btwnconn1lem5  31162  btwnconn1lem7  31164  btwnconn1lem11  31168  btwnconn1lem12  31169  btwnconn1lem13  31170  brsegle2  31180  segleantisym  31186  broutsideof2  31193  btwnoutside  31196  outsideoftr  31200  outsideofeq  31201  outsideofeu  31202  outsidele  31203  lineunray  31218  lineelsb2  31219  linecom  31221  linethru  31224  neibastop1  31318  lindsenlbs  32368  matunitlindflem1  32369  poimirlem28  32401  poimirlem32  32405  heicant  32408  mettrifi  32517  isbnd3  32547  heibor1lem  32572  bfplem2  32586  ghomdiv  32655  rngo2  32670  rngolz  32685  rngorz  32686  zerdivemp1x  32710  lfladdcl  33170  lflvscl  33176  eqlkr3  33200  lkrlsp  33201  lshpkrlem4  33212  oldmm1  33316  olj01  33324  latmassOLD  33328  latm32  33330  latmrot  33331  latm4  33332  olm01  33335  cmtcomlemN  33347  cmtbr3N  33353  cmtbr4N  33354  lecmtN  33355  omlfh1N  33357  atlen0  33409  atnle  33416  atlatmstc  33418  atlatle  33419  cvlexchb1  33429  cvlcvr1  33438  ishlat3N  33453  hlatjass  33468  hlatj12  33469  hlatj32  33470  hlsupr2  33485  hlhgt2  33487  hl0lt1N  33488  hlrelat  33500  hlrelat2  33501  exatleN  33502  hlrelat3  33510  cvrval5  33513  cvrexchlem  33517  cvratlem  33519  cvrat  33520  atcvr0eq  33524  lnnat  33525  atlt  33535  atlelt  33536  2atlt  33537  atexchltN  33539  cvrat3  33540  2atjm  33543  atbtwn  33544  4noncolr3  33551  athgt  33554  3dimlem3a  33558  3dimlem3OLDN  33560  3dimlem4a  33561  3dimlem4OLDN  33563  3dim1  33565  3dim2  33566  1cvratex  33571  ps-1  33575  ps-2  33576  hlatexch3N  33578  hlatexch4  33579  ps-2b  33580  3atlem1  33581  3atlem2  33582  3atlem5  33585  3atlem6  33586  llnnleat  33611  llncmp  33620  2at0mat0  33623  2atmat0  33624  2atm  33625  lplni2  33635  lvolex3N  33636  lplnnle2at  33639  lplnnleat  33640  lplnnlelln  33641  2atnelpln  33642  llncvrlpln  33656  2atmat  33659  lplncmp  33660  lplnexllnN  33662  2llnjaN  33664  2llnm4  33668  2llnmeqat  33669  lvolnle3at  33680  lvolnleat  33681  2atnelvolN  33685  islvol2aN  33690  4atlem3  33694  4atlem3a  33695  4atlem3b  33696  4atlem4a  33697  4atlem4b  33698  4atlem4c  33699  4atlem4d  33700  4atlem10  33704  4atlem11b  33706  4atlem11  33707  4atlem12b  33709  4atlem12  33710  4at2  33712  lplncvrlvol  33714  lvolcmp  33715  2lplnja  33717  dalemqrprot  33746  dalemply  33752  dalemsly  33753  dalemrot  33755  dalemrotyz  33756  dalem1  33757  dalemcea  33758  dalem3  33762  dalem5  33765  dalem8  33768  dalem-cly  33769  dalem11  33772  dalem12  33773  dalem16  33777  dalem17  33778  dalem18  33779  dalem21  33792  dalem24  33795  dalem25  33796  dalem38  33808  dalem39  33809  dalem44  33814  dalem54  33824  dalem55  33825  dalem57  33827  dalem58  33828  dalem59  33829  dalem60  33830  dath2  33835  2atm2atN  33883  2llnma1b  33884  2llnma3r  33886  cdlema1N  33889  cdlemblem  33891  paddasslem5  33922  paddasslem10  33927  paddasslem12  33929  paddasslem13  33930  paddass  33936  padd12N  33937  padd4N  33938  paddss  33943  pmodlem1  33944  pmodl42N  33949  pmapjoin  33950  pmapjlln1  33953  atmod1i2  33957  llnmod1i2  33958  llnexchb2  33967  dalawlem2  33970  dalawlem3  33971  dalawlem5  33973  dalawlem6  33974  dalawlem7  33975  dalawlem8  33976  dalawlem11  33979  dalawlem12  33980  dalawlem13  33981  pclunN  33996  osumcllem1N  34054  pexmidlem3N  34070  lhp2lt  34099  lhp0lt  34101  lhpexle2lem  34107  lhpexle3lem  34109  lhpocnle  34114  lhpj1  34120  lhpmcvr4N  34124  lhp2at0  34130  lhpat3  34144  4atexlemtlw  34165  4atexlemc  34167  4atexlemnclw  34168  4atexlemcnd  34170  lautcvr  34190  lautj  34191  lautm  34192  ltrnm  34229  ltrnj  34230  ltrncvr  34231  trlval3  34286  cdlemc5  34294  cdlemd2  34298  cdlemd3  34299  cdleme0e  34316  cdleme1  34326  cdleme3c  34329  cdleme3g  34333  cdleme3h  34334  cdleme3  34336  cdleme5  34339  cdleme7c  34344  cdleme7d  34345  cdleme7e  34346  cdleme7ga  34347  cdleme7  34348  cdleme9  34352  cdleme11c  34360  cdleme11g  34364  cdleme11k  34367  cdleme11  34369  cdleme12  34370  cdleme15b  34374  cdleme15d  34376  cdleme16d  34380  cdleme16e  34381  cdleme16f  34382  cdleme17b  34386  cdleme18b  34391  cdleme22gb  34393  cdlemednpq  34398  cdleme19a  34403  cdleme20aN  34409  cdleme20bN  34410  cdleme20c  34411  cdleme20d  34412  cdleme20j  34418  cdleme21c  34427  cdleme22aa  34439  cdleme22b  34441  cdleme22cN  34442  cdleme22d  34443  cdleme22e  34444  cdleme22eALTN  34445  cdleme23b  34450  cdleme23c  34451  cdleme28a  34470  cdleme30a  34478  cdlemefs29bpre0N  34516  cdlemefs29bpre1N  34517  cdlemefs29cpre1N  34518  cdlemefs29clN  34519  cdlemefs32fvaN  34522  cdlemefs32fva1  34523  cdleme32b  34542  cdleme32c  34543  cdleme32e  34545  cdleme35a  34548  cdleme35fnpq  34549  cdleme35b  34550  cdleme35f  34554  cdleme36a  34560  cdleme36m  34561  cdleme37m  34562  cdleme39a  34565  cdleme42c  34572  cdleme42i  34583  cdleme42keg  34586  cdleme42mgN  34588  cdleme48bw  34602  cdlemeg46fjgN  34621  cdlemeg46fjv  34623  cdlemeg46req  34629  cdleme50trn1  34649  cdlemf1  34661  cdlemf2  34662  cdlemg1cex  34688  cdlemg2fv2  34700  cdlemg7fvbwN  34707  cdlemg4c  34712  cdlemg4  34717  cdlemg6c  34720  cdlemg8b  34728  cdlemg10c  34739  cdlemg10  34741  cdlemg11b  34742  cdlemg12f  34748  cdlemg13a  34751  cdlemg17a  34761  cdlemg17dALTN  34764  cdlemg18b  34779  cdlemg19a  34783  cdlemg27a  34792  cdlemg27b  34796  cdlemg33b0  34801  cdlemg33a  34806  cdlemg35  34813  trlcolem  34826  cdlemg42  34829  cdlemg46  34835  trljco  34840  tendopltp  34880  cdlemh1  34915  cdlemh2  34916  cdlemi1  34918  cdlemi  34920  cdlemk3  34933  cdlemk10  34943  cdlemk11  34949  cdlemk15  34955  cdlemk1u  34959  cdlemk5u  34961  cdlemk11u  34971  cdlemk39  35016  cdlemkid1  35022  cdlemk50  35052  cdlemk51  35053  erngdvlem3-rN  35098  tendocnv  35122  tendospcanN  35124  dialss  35147  dia2dimlem1  35165  dia2dimlem2  35166  dia2dimlem3  35167  dia2dimlem10  35174  dia2dimlem12  35176  dvhvaddass  35198  dvhlveclem  35209  cdlemm10N  35219  doca2N  35227  djajN  35238  dib1dim2  35269  diblss  35271  diclspsn  35295  cdlemn2  35296  cdlemn10  35307  dihjustlem  35317  dihord1  35319  dihord2a  35320  dihord2pre2  35327  dib2dim  35344  dih2dimb  35345  dih2dimbALTN  35346  dihopelvalcpre  35349  dihord5b  35360  dihord6b  35361  dihord5apre  35363  dihmeetlem1N  35391  dihglblem5apreN  35392  dihglblem2N  35395  dihglbcpreN  35401  dihmeetbclemN  35405  dihmeetlem3N  35406  dihmeetlem6  35410  dih1dimatlem  35430  djhcvat42  35516  dihjatcclem1  35519  dihjatcclem4  35522  dvh4dimat  35539  lcfl7lem  35600  lclkrlem2m  35620  lcfrlem1  35643  lcdvsass  35708  baerlem3lem1  35808  baerlem5alem1  35809  baerlem5blem1  35810  mapdh6gN  35843  mapdh6hN  35844  hdmap1l6g  35918  hdmap1l6h  35919  hdmapneg  35950  hdmap14lem8  35979  hgmapadd  35998  hgmapmul  35999  hgmapvvlem1  36027  irrapxlem5  36202  aomclem2  36437  isnumbasgrplem2  36487  mpaaeu  36533  mendring  36575  mendlmod  36576  relexpnul  36783  caofcan  37338  disjiun2  38045  wessf1ornlem  38160  stoweidlem18  38705  stoweidlem41  38728  stoweidlem45  38732  stoweidlem55  38742  fourierdlem25  38819  fourierdlem31  38825  fourierdlem37  38831  fourierdlem42  38836  etransclem48  38969  ioorrnopnlem  38994  issalgend  39026  sge0iunmptlemfi  39100  hoicvr  39232  hoidmvlelem2  39280  iunhoiioolem  39360  vonioolem1  39365  prmdvdsfmtnof1lem1  39829  prmdvdsfmtnof  39831  sgprmdvdsmersenne  39854  perfectALTVlem1  39959  perfectALTVlem2  39960  nbfusgrlevtxm2  40598  nbusgrvtxm1  40599  elwwlks2ons3  41151  usgr2wspthon  41160  clwwlknclwwlkdifnum  41174  frgr2wwlkeu  41484  av-numclwwlk5  41534  rnglz  41666  ssnn0ssfz  41912  zlmodzxzsub  41923  invginvrid  41934  lmodvsmdi  41949  ply1sclrmsm  41957  lincsum  42004  lincscm  42005  lindslinindimp2lem4  42036  lindslinindsimp2lem5  42037  ldepsprlem  42047  lincresunit3lem1  42054  lincresunit3lem2  42055  isldepslvec2  42060  relogbmulbexp  42145
  Copyright terms: Public domain W3C validator