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  4579  disjxiunOLD  4580  wereu2  5035  ordelord  5662  caovassd  6731  caovcand  6734  caovordid  6738  caovordd  6740  caovdid  6747  caovdird  6750  swoer  7659  swoord1  7660  swoord2  7661  frfi  8090  indexfi  8157  ssfii  8208  elfiun  8219  suplub2  8250  supgtoreq  8259  infltoreq  8291  wemaplem2  8335  htalem  8642  cofsmo  8974  alephsing  8981  sornom  8982  axdc3lem4  9158  zorn2lem1  9201  ttukeylem6  9219  ttukeylem7  9220  prlem934  9734  supfirege  10886  suprfinzcl  11368  fzosubel3  12396  fsuppmapnn0fiublem  12651  seqsplit  12696  seqcaopr  12700  ccatass  13224  wrdcctswrd  13317  wrdeqs1cat  13326  splid  13355  spllen  13356  splfv1  13357  splfv2a  13358  splval2  13359  swrds2  13533  isercolllem2  14244  fsumiun  14394  zprod  14506  lcmftp  15187  pcgcd1  15419  cshwsidrepswmod0  15639  cshwshashlem2  15641  cshwsdisj  15643  firest  15916  iscatd2  16165  posasymb  16775  joinle  16837  meetle  16851  lattrd  16881  latleeqj1  16886  latjlej1  16888  latjlej12  16890  latnlej2  16894  latjidm  16897  latleeqm1  16902  latmlem1  16904  latmlem12  16906  latmidm  16909  latledi  16912  latjass  16918  latj12  16919  latj13  16921  latj31  16922  latjrot  16923  latj4  16924  mod1ile  16928  lubun  16946  clatleglb  16949  latdisdlem  17012  mnd32g  17128  mnd12g  17129  mnd4g  17130  ismndd  17136  prdsmndd  17146  imasmnd  17151  mrcmndind  17189  gsumspl  17204  grpasscan2  17302  grpidrcan  17303  grpidlcan  17304  grpinvinv  17305  grplmulf1o  17312  grpinvssd  17315  grpinvadd  17316  grpsubrcan  17319  grpsubadd  17326  grpaddsubass  17328  grppncan  17329  grpsubsub4  17331  grppnpcan2  17332  grpnpncan  17333  grpnpncan0  17334  grpnnncan2  17335  dfgrp3lem  17336  dfgrp3  17337  grplactcnv  17341  imasgrp  17354  mhmmnd  17360  mulgaddcomlem  17386  mulgaddcom  17387  mulgnn0dir  17394  mulgdirlem  17395  mulgneg2  17398  mulgnnass  17399  mulgnnassOLD  17400  mulgnn0ass  17401  mulgass  17402  mulgmodid  17404  nsgconj  17450  isnsg3  17451  nmzsubg  17458  ssnmz  17459  eqger  17467  eqgcpbl  17471  conjghm  17514  conjnmz  17517  conjnmzb  17518  subgga  17556  gass  17557  gasubg  17558  galcan  17560  gacan  17561  gapm  17562  gaorber  17564  gastacl  17565  gastacos  17566  cntzsubm  17591  cntzsubg  17592  oppgmnd  17607  symggen  17713  odmodnn0  17782  mndodconglem  17783  odmod  17788  odcong  17791  odmulgid  17794  odbezout  17798  gexdvdsi  17821  gexdvds  17822  sylow1lem2  17837  sylow1lem4  17839  sylow2blem1  17858  sylow2blem2  17859  sylow2blem3  17860  sylow3lem1  17865  sylow3lem2  17866  lsmass  17906  lsmmod  17911  lsmdisj2  17918  subgdisj1  17927  efgredleme  17979  efgredlemc  17981  efgcpbllemb  17991  frgp0  17996  frgpuplem  18008  abl32  18037  abladdsub4  18042  abladdsub  18043  ablpncan2  18044  ablsubsub  18046  mulgdi  18055  mulgsubdi  18058  odadd1  18074  odadd2  18075  gex2abl  18077  oddvdssubg  18081  cygabl  18115  telgsumfzslem  18208  ablfacrp  18288  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem4  18300  srgmulgass  18354  srgpcomp  18355  srgpcompp  18356  srgpcomppsc  18357  srgbinomlem3  18365  srgbinomlem4  18366  srgbinomlem  18367  csrgbinom  18369  ringadd2  18398  rngo2times  18399  ringcom  18402  ringlz  18410  ringrz  18411  ringnegl  18417  rngnegr  18418  ringmneg1  18419  ringmneg2  18420  ringsubdi  18422  rngsubdir  18423  mulgass2  18424  prdsringd  18435  imasring  18442  opprring  18454  mulgass3  18460  dvdsrtr  18475  dvdsrmul1  18476  unitgrp  18490  dvrass  18513  dvrcan1  18514  dvrcan3  18515  irredrmul  18530  drngmul0or  18591  subrginv  18619  cntzsubr  18635  lmod0vs  18719  lmodvs0  18720  lmodvsmmulgdi  18721  lmodfopne  18724  lmodvneg1  18729  lmodvsneg  18730  lmodcom  18732  lmodsubvs  18742  lmodsubdi  18743  lmodsubdir  18744  lssvsubcl  18765  lssvacl  18775  lssvscl  18776  islss3  18780  lss1d  18784  lssintcl  18785  prdslmodd  18790  lmodvsinv  18857  lmodvsinv2  18858  lmhmplusg  18865  lmhmvsca  18866  lsmcl  18904  pj1lmhm  18921  lvecvs0or  18929  lssvs0or  18931  lvecinv  18934  lspsnvs  18935  lspfixed  18949  lspexch  18950  lspsolvlem  18963  lspsolv  18964  lssacsex  18965  lspsnat  18966  lsppratlem1  18968  lsppratlem3  18970  lsppratlem4  18971  lbsextlem2  18980  lbsextlem4  18982  sralmod  19008  2idlcpbl  19055  unitrrg  19114  assa2ass  19143  issubassa  19145  sraassa  19146  asclghm  19159  asclmul1  19160  asclmul2  19161  asclrhm  19163  assamulgscmlem2  19170  psrbagcon  19192  psrbagconcl  19194  psrbagconf1o  19195  gsumbagdiaglem  19196  psrmulcllem  19208  psrlidm  19224  psrridm  19225  psrass1  19226  psrdi  19227  psrdir  19228  psrass23l  19229  psrcom  19230  mplmon2mul  19322  evlslem1  19336  coe1subfv  19457  lply1binomsc  19498  mulgrhm  19665  cygznlem3  19737  evpmodpmf1o  19761  ipdi  19804  ip2di  19805  ipsubdir  19806  ipsubdi  19807  ip2subdi  19808  ipassr  19810  ipassr2  19811  ip2eq  19817  ocvlss  19835  lsmcss  19855  frlmphl  19939  frlmup1  19956  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  dmatmul  20122  dmatsubcl  20123  scmataddcl  20141  smatvscl  20149  scmatghm  20158  mavmulass  20174  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  mdetunilem7  20243  mdetuni0  20246  matinv  20302  pm2mpghm  20440  chpscmatgsummon  20469  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  iinopn  20532  subbascn  20868  cnhaus  20968  nrmsep2  20970  nrmsep  20971  regsep2  20990  isreg2  20991  hauscmplem  21019  1stcfb  21058  2ndcctbss  21068  ptbasfi  21194  pthaus  21251  txtube  21253  txhaus  21260  xkohaus  21266  kqnrmlem1  21356  kqnrmlem2  21357  nrmr0reg  21362  nrmhmph  21407  fbssint  21452  infil  21477  fgabs  21493  filcon  21497  filuni  21499  trfil2  21501  trfg  21505  ufprim  21523  elfm3  21564  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  hausflimi  21594  hauspwpwf1  21601  fclsneii  21631  supnfcls  21634  flimfnfcls  21642  fclscmpi  21643  alexsublem  21658  ghmcnp  21728  qustgpopn  21733  psmetsym  21925  psmettri  21926  psmetge0  21927  psmetres2  21929  xmetge0  21959  xmetsym  21962  xmettri  21966  xmetres2  21976  prdsxmetlem  21983  prdsmet  21985  imasdsf1olem  21988  imasf1oxmet  21990  bldisj  22013  xblss2ps  22016  xblss2  22017  xmeter  22048  prdsbl  22106  metustexhalf  22171  metust  22173  nrmmetd  22189  ngpsubcan  22228  nmmtri  22236  nmrtri  22238  ngptgp  22250  nlmvscnlem2  22299  nrginvrcnlem  22305  metdcnlem  22447  clmvs2  22702  clmmulg  22709  clmnegneg  22712  clmnegsubdi2  22713  clmsub4  22714  cvsmuleqdivd  22742  cvsdiveqd  22743  ncvspi  22764  cphabscl  22793  cphsqrtcl2  22794  cphsqrtcl3  22795  cphnmf  22803  cph2ass  22821  cphassi  22822  cphassir  22823  ipcau2  22841  tchcphlem2  22843  ipcnlem2  22851  cfilfcls  22880  iscau3  22884  iscmet3lem2  22898  iscmet3  22899  relcmpcmet  22923  minveclem2  23005  minveclem4  23011  pjthlem1  23016  pjthlem2  23017  uniioombllem4  23160  dyadmax  23172  itg1addlem4  23272  itg1climres  23287  ply1divex  23700  aalioulem2  23892  amgmlem  24516  dvdsppwf1o  24712  perfect1  24753  perfectlem1  24754  perfectlem2  24755  dchrptlem2  24790  colline  25344  ttgcontlem1  25565  axcontlem9  25652  eengtrkg  25665  eengtrkge  25666  4cycl4dv4e  26196  el2spthonot0  26398  usg2spthonot1  26417  clwlknclwlkdifnum  26488  eupa0  26501  eupares  26502  eupap1  26503  frg2woteu  26582  numclwwlk5  26639  numclwwlk6  26640  grpoidinvlem4  26745  grpoinvop  26771  grponpcan  26781  vcm  26815  nvmul0or  26889  nvpncan2  26892  nvdif  26905  nvabs  26911  smcnlem  26936  lnomul  26999  minvecolem2  27115  superpos  28597  ssnnssfz  28937  omndmul2  29043  omndmul3  29044  ogrpaddltbi  29050  ogrpaddltrbid  29052  ogrpsublt  29053  ogrpinvlt  29055  isarchi3  29072  archirngz  29074  archiabllem1a  29076  archiabllem1  29078  archiabllem2a  29079  archiabllem2c  29080  slmdvs0  29109  gsumvsca1  29113  gsumvsca2  29114  dvrdir  29121  rdivmuldivd  29122  dvrcan5  29124  ornglmullt  29138  isarchiofld  29148  rhmdvd  29152  rhmunitinv  29153  psgnfzto1stlem  29181  mdetpmtr1  29217  mdetpmtr12  29219  mdetlap  29226  locfinref  29236  metideq  29264  metider  29265  pstmxmet  29268  lmxrge0  29326  qqhghm  29360  qqhrhm  29361  ispisys2  29543  rossros  29570  measdivcst  29615  oddpwdc  29743  ballotlemiex  29890  wrdsplex  29944  cvmopnlem  30514  cvmliftmolem2  30518  cvmliftlem6  30526  cvmliftlem8  30528  cvmliftlem9  30529  cvmlift2lem9  30547  cvmlift3lem2  30556  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  nodense  31088  cgrtriv  31279  cgrdegen  31281  cgrextend  31285  segconeq  31287  btwntriv2  31289  btwncomand  31292  btwntriv1  31293  btwnintr  31296  btwnexch3  31297  btwnouttr  31301  btwnexch  31302  trisegint  31305  ifscgr  31321  btwnxfr  31333  colineartriv1  31344  colineartriv2  31345  colinearxfr  31352  fscgr  31357  lineid  31360  idinside  31361  endofsegidand  31363  btwnconn1lem5  31368  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn1lem13  31376  brsegle2  31386  segleantisym  31392  broutsideof2  31399  btwnoutside  31402  outsideoftr  31406  outsideofeq  31407  outsideofeu  31408  outsidele  31409  lineunray  31424  lineelsb2  31425  linecom  31427  linethru  31430  neibastop1  31524  lindsenlbs  32574  matunitlindflem1  32575  poimirlem28  32607  poimirlem32  32611  heicant  32614  mettrifi  32723  isbnd3  32753  heibor1lem  32778  bfplem2  32792  ghomdiv  32861  rngo2  32876  rngolz  32891  rngorz  32892  zerdivemp1x  32916  lfladdcl  33376  lflvscl  33382  eqlkr3  33406  lkrlsp  33407  lshpkrlem4  33418  oldmm1  33522  olj01  33530  latmassOLD  33534  latm32  33536  latmrot  33537  latm4  33538  olm01  33541  cmtcomlemN  33553  cmtbr3N  33559  cmtbr4N  33560  lecmtN  33561  omlfh1N  33563  atlen0  33615  atnle  33622  atlatmstc  33624  atlatle  33625  cvlexchb1  33635  cvlcvr1  33644  ishlat3N  33659  hlatjass  33674  hlatj12  33675  hlatj32  33676  hlsupr2  33691  hlhgt2  33693  hl0lt1N  33694  hlrelat  33706  hlrelat2  33707  exatleN  33708  hlrelat3  33716  cvrval5  33719  cvrexchlem  33723  cvratlem  33725  cvrat  33726  atcvr0eq  33730  lnnat  33731  atlt  33741  atlelt  33742  2atlt  33743  atexchltN  33745  cvrat3  33746  2atjm  33749  atbtwn  33750  4noncolr3  33757  athgt  33760  3dimlem3a  33764  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4OLDN  33769  3dim1  33771  3dim2  33772  1cvratex  33777  ps-1  33781  ps-2  33782  hlatexch3N  33784  hlatexch4  33785  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem5  33791  3atlem6  33792  llnnleat  33817  llncmp  33826  2at0mat0  33829  2atmat0  33830  2atm  33831  lplni2  33841  lvolex3N  33842  lplnnle2at  33845  lplnnleat  33846  lplnnlelln  33847  2atnelpln  33848  llncvrlpln  33862  2atmat  33865  lplncmp  33866  lplnexllnN  33868  2llnjaN  33870  2llnm4  33874  2llnmeqat  33875  lvolnle3at  33886  lvolnleat  33887  2atnelvolN  33891  islvol2aN  33896  4atlem3  33900  4atlem3a  33901  4atlem3b  33902  4atlem4a  33903  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  4atlem10  33910  4atlem11b  33912  4atlem11  33913  4atlem12b  33915  4atlem12  33916  4at2  33918  lplncvrlvol  33920  lvolcmp  33921  2lplnja  33923  dalemqrprot  33952  dalemply  33958  dalemsly  33959  dalemrot  33961  dalemrotyz  33962  dalem1  33963  dalemcea  33964  dalem3  33968  dalem5  33971  dalem8  33974  dalem-cly  33975  dalem11  33978  dalem12  33979  dalem16  33983  dalem17  33984  dalem18  33985  dalem21  33998  dalem24  34001  dalem25  34002  dalem38  34014  dalem39  34015  dalem44  34020  dalem54  34030  dalem55  34031  dalem57  34033  dalem58  34034  dalem59  34035  dalem60  34036  dath2  34041  2atm2atN  34089  2llnma1b  34090  2llnma3r  34092  cdlema1N  34095  cdlemblem  34097  paddasslem5  34128  paddasslem10  34133  paddasslem12  34135  paddasslem13  34136  paddass  34142  padd12N  34143  padd4N  34144  paddss  34149  pmodlem1  34150  pmodl42N  34155  pmapjoin  34156  pmapjlln1  34159  atmod1i2  34163  llnmod1i2  34164  llnexchb2  34173  dalawlem2  34176  dalawlem3  34177  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem11  34185  dalawlem12  34186  dalawlem13  34187  pclunN  34202  osumcllem1N  34260  pexmidlem3N  34276  lhp2lt  34305  lhp0lt  34307  lhpexle2lem  34313  lhpexle3lem  34315  lhpocnle  34320  lhpj1  34326  lhpmcvr4N  34330  lhp2at0  34336  lhpat3  34350  4atexlemtlw  34371  4atexlemc  34373  4atexlemnclw  34374  4atexlemcnd  34376  lautcvr  34396  lautj  34397  lautm  34398  ltrnm  34435  ltrnj  34436  ltrncvr  34437  trlval3  34492  cdlemc5  34500  cdlemd2  34504  cdlemd3  34505  cdleme0e  34522  cdleme1  34532  cdleme3c  34535  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme5  34545  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme9  34558  cdleme11c  34566  cdleme11g  34570  cdleme11k  34573  cdleme11  34575  cdleme12  34576  cdleme15b  34580  cdleme15d  34582  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme17b  34592  cdleme18b  34597  cdleme22gb  34599  cdlemednpq  34604  cdleme19a  34609  cdleme20aN  34615  cdleme20bN  34616  cdleme20c  34617  cdleme20d  34618  cdleme20j  34624  cdleme21c  34633  cdleme22aa  34645  cdleme22b  34647  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme23b  34656  cdleme23c  34657  cdleme28a  34676  cdleme30a  34684  cdlemefs29bpre0N  34722  cdlemefs29bpre1N  34723  cdlemefs29cpre1N  34724  cdlemefs29clN  34725  cdlemefs32fvaN  34728  cdlemefs32fva1  34729  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35f  34760  cdleme36a  34766  cdleme36m  34767  cdleme37m  34768  cdleme39a  34771  cdleme42c  34778  cdleme42i  34789  cdleme42keg  34792  cdleme42mgN  34794  cdleme48bw  34808  cdlemeg46fjgN  34827  cdlemeg46fjv  34829  cdlemeg46req  34835  cdleme50trn1  34855  cdlemf1  34867  cdlemf2  34868  cdlemg1cex  34894  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg4c  34918  cdlemg4  34923  cdlemg6c  34926  cdlemg8b  34934  cdlemg10c  34945  cdlemg10  34947  cdlemg11b  34948  cdlemg12f  34954  cdlemg13a  34957  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg18b  34985  cdlemg19a  34989  cdlemg27a  34998  cdlemg27b  35002  cdlemg33b0  35007  cdlemg33a  35012  cdlemg35  35019  trlcolem  35032  cdlemg42  35035  cdlemg46  35041  trljco  35046  tendopltp  35086  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  cdlemi  35126  cdlemk3  35139  cdlemk10  35149  cdlemk11  35155  cdlemk15  35161  cdlemk1u  35165  cdlemk5u  35167  cdlemk11u  35177  cdlemk39  35222  cdlemkid1  35228  cdlemk50  35258  cdlemk51  35259  erngdvlem3-rN  35304  tendocnv  35328  tendospcanN  35330  dialss  35353  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dia2dimlem10  35380  dia2dimlem12  35382  dvhvaddass  35404  dvhlveclem  35415  cdlemm10N  35425  doca2N  35433  djajN  35444  dib1dim2  35475  diblss  35477  diclspsn  35501  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2pre2  35533  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihopelvalcpre  35555  dihord5b  35566  dihord6b  35567  dihord5apre  35569  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem2N  35601  dihglbcpreN  35607  dihmeetbclemN  35611  dihmeetlem3N  35612  dihmeetlem6  35616  dih1dimatlem  35636  djhcvat42  35722  dihjatcclem1  35725  dihjatcclem4  35728  dvh4dimat  35745  lcfl7lem  35806  lclkrlem2m  35826  lcfrlem1  35849  lcdvsass  35914  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  mapdh6gN  36049  mapdh6hN  36050  hdmap1l6g  36124  hdmap1l6h  36125  hdmapneg  36156  hdmap14lem8  36185  hgmapadd  36204  hgmapmul  36205  hgmapvvlem1  36233  irrapxlem5  36408  aomclem2  36643  isnumbasgrplem2  36693  mpaaeu  36739  mendring  36781  mendlmod  36782  relexpnul  36989  caofcan  37544  disjiun2  38251  wessf1ornlem  38366  stoweidlem18  38911  stoweidlem41  38934  stoweidlem45  38938  stoweidlem55  38948  fourierdlem25  39025  fourierdlem31  39031  fourierdlem37  39037  fourierdlem42  39042  etransclem48  39175  ioorrnopnlem  39200  issalgend  39232  sge0iunmptlemfi  39306  hoicvr  39438  hoidmvlelem2  39486  iunhoiioolem  39566  vonioolem1  39571  prmdvdsfmtnof1lem1  40034  prmdvdsfmtnof  40036  sgprmdvdsmersenne  40059  perfectALTVlem1  40164  perfectALTVlem2  40165  nbfusgrlevtxm2  40606  nbusgrvtxm1  40607  elwwlks2ons3  41159  usgr2wspthon  41168  clwwlknclwwlkdifnum  41182  frgr2wwlkeu  41492  av-numclwwlk5  41542  rnglz  41674  ssnn0ssfz  41920  zlmodzxzsub  41931  invginvrid  41942  lmodvsmdi  41957  ply1sclrmsm  41965  lincsum  42012  lincscm  42013  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  ldepsprlem  42055  lincresunit3lem1  42062  lincresunit3lem2  42063  isldepslvec2  42068  relogbmulbexp  42153
  Copyright terms: Public domain W3C validator