Theorem syl13anc 1363

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

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1119	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 584	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  syl23anc  1368  syl33anc  1376  disjxiun  4953  wereu2  5432  ordelord  6080  caovassd  7194  caovcand  7197  caovordid  7201  caovordd  7203  caovdid  7210  caovdird  7213  swoer  8160  swoord1  8161  swoord2  8162  frfi  8599  indexfi  8668  ssfii  8719  elfiun  8730  suplub2  8761  supgtoreq  8770  infltoreq  8802  wemaplem2  8847  htalem  9160  cofsmo  9526  alephsing  9533  sornom  9534  axdc3lem4  9710  zorn2lem1  9753  ttukeylem6  9771  ttukeylem7  9772  prlem934  10290  supfirege  11464  suprfinzcl  11935  ssfzunsn  12792  fzosubel3  12936  fsuppmapnn0fiublem  13196  seqsplit  13241  seqcaopr  13245  ccatass  13774  spllen  13940  splfv1  13941  splfv2a  13942  splval2  13943  swrds2  14126  isercolllem2  14844  fsumiun  14997  zprod  15112  lcmftp  15797  pcgcd1  16030  cshwsidrepswmod0  16245  cshwshashlem2  16247  cshwsdisj  16249  firest  16523  iscatd2  16769  posasymb  17379  joinle  17441  meetle  17455  lattrd  17485  latleeqj1  17490  latjlej1  17492  latjlej12  17494  latnlej2  17498  latjidm  17501  latleeqm1  17506  latmlem1  17508  latmlem12  17510  latmidm  17513  latledi  17516  latjass  17522  latj12  17523  latj13  17525  latj31  17526  latjrot  17527  latj4  17528  mod1ile  17532  lubun  17550  clatleglb  17553  latdisdlem  17616  mnd32g  17732  mnd12g  17733  mnd4g  17734  ismndd  17740  prdsmndd  17750  imasmnd  17755  mndind  17793  gsumspl  17808  grpasscan2  17908  grpidrcan  17909  grpidlcan  17910  grpinvinv  17911  grplmulf1o  17918  grpinvssd  17921  grpinvadd  17922  grpsubrcan  17925  grpsubadd  17932  grpaddsubass  17934  grppncan  17935  grpsubsub4  17937  grppnpcan2  17938  grpnpncan  17939  grpnpncan0  17940  grpnnncan2  17941  dfgrp3lem  17942  dfgrp3  17943  grplactcnv  17947  imasgrp  17960  mhmmnd  17966  mulgaddcomlem  17992  mulgaddcom  17993  mulgnn0dir  17999  mulgdirlem  18000  mulgneg2  18003  mulgnnass  18004  mulgnn0ass  18005  mulgass  18006  mulgmodid  18008  nsgconj  18054  isnsg3  18055  nmzsubg  18062  ssnmz  18063  eqger  18071  eqgcpbl  18075  conjghm  18118  conjnmz  18121  conjnmzb  18122  subgga  18159  gass  18160  gasubg  18161  galcan  18163  gacan  18164  gapm  18165  gaorber  18167  gastacl  18168  gastacos  18169  cntzsubm  18195  cntzsubg  18196  oppgmnd  18211  symggen  18317  odmodnn0  18387  mndodconglem  18388  odmod  18393  odcong  18396  odmulgid  18399  odbezout  18403  gexdvdsi  18426  gexdvds  18427  sylow1lem2  18442  sylow1lem4  18444  sylow2blem1  18463  sylow2blem2  18464  sylow2blem3  18465  sylow3lem1  18470  sylow3lem2  18471  lsmass  18511  lsmmod  18516  lsmdisj2  18523  subgdisj1  18532  efgredleme  18584  efgredlemc  18586  efgcpbllemb  18596  frgp0  18601  frgpuplem  18613  abl32  18642  abladdsub4  18647  abladdsub  18648  ablpncan2  18649  ablsubsub  18651  mulgdi  18660  mulgsubdi  18663  odadd1  18679  odadd2  18680  gex2abl  18682  oddvdssubg  18686  cygabl  18720  telgsumfzslem  18813  ablfacrp  18893  pgpfac1lem2  18902  pgpfac1lem3a  18903  pgpfac1lem3  18904  pgpfac1lem4  18905  srgmulgass  18959  srgpcomp  18960  srgpcompp  18961  srgpcomppsc  18962  srgbinomlem3  18970  srgbinomlem4  18971  srgbinomlem  18972  csrgbinom  18974  ringadd2  19003  rngo2times  19004  ringcom  19007  ringlz  19015  ringrz  19016  ringnegl  19022  rngnegr  19023  ringmneg1  19024  ringmneg2  19025  ringsubdi  19027  rngsubdir  19028  mulgass2  19029  prdsringd  19040  imasring  19047  opprring  19059  mulgass3  19065  dvdsrtr  19080  dvdsrmul1  19081  unitgrp  19095  dvrass  19118  dvrcan1  19119  dvrcan3  19120  irredrmul  19135  drngmul0or  19201  subrginv  19229  cntzsubr  19246  lmod0vs  19345  lmodvs0  19346  lmodvsmmulgdi  19347  lmodfopne  19350  lmodvneg1  19355  lmodvsneg  19356  lmodcom  19358  lmodsubvs  19368  lmodsubdi  19369  lmodsubdir  19370  lssvsubcl  19393  lssvacl  19404  lssvscl  19405  islss3  19409  lss1d  19413  lssintcl  19414  prdslmodd  19419  lmodvsinv  19486  lmodvsinv2  19487  lmhmplusg  19494  lmhmvsca  19495  lsmcl  19533  pj1lmhm  19550  lvecvs0or  19558  lssvs0or  19560  lvecinv  19563  lspsnvs  19564  lspfixed  19578  lspexch  19579  lspsolvlem  19592  lspsolv  19593  lssacsex  19594  lspsnat  19595  lsppratlem1  19597  lsppratlem3  19599  lsppratlem4  19600  lbsextlem2  19609  lbsextlem4  19611  sralmod  19637  2idlcpbl  19684  unitrrg  19743  assa2ass  19772  issubassa  19774  sraassa  19775  asclghm  19788  asclmul1  19790  asclmul2  19791  ascldimul  19792  ascldimulOLD  19793  assamulgscmlem2  19805  psrbagcon  19827  psrbagconcl  19829  psrbagconf1o  19830  gsumbagdiaglem  19831  psrmulcllem  19843  psrlidm  19859  psrridm  19860  psrass1  19861  psrdi  19862  psrdir  19863  psrass23l  19864  psrcom  19865  mplmon2mul  19956  evlslem1  19970  coe1subfv  20105  lply1binomsc  20146  mulgrhm  20315  cygznlem3  20386  evpmodpmf1o  20410  ipdi  20454  ip2di  20455  ipsubdir  20456  ipsubdi  20457  ip2subdi  20458  ipassr  20460  ipassr2  20461  ip2eq  20467  phlssphl  20473  ocvlss  20486  lsmcss  20506  frlmphl  20595  frlmup1  20612  mamuass  20683  mamudi  20684  mamudir  20685  mamuvs1  20686  mamuvs2  20687  dmatmul  20778  dmatsubcl  20779  scmataddcl  20797  smatvscl  20805  scmatghm  20814  mavmulass  20830  mdetrlin  20883  mdetrsca  20884  mdetralt  20889  mdetunilem7  20899  mdetuni0  20902  matinv  20958  pm2mpghm  21096  chpscmatgsummon  21125  chfacfscmulgsum  21140  chfacfpmmulgsum  21144  chfacfpmmulgsum2  21145  cpmadugsumlemB  21154  cpmadugsumlemC  21155  cpmadugsumlemF  21156  iinopn  21182  subbascn  21534  cnhaus  21634  nrmsep2  21636  nrmsep  21637  regsep2  21656  isreg2  21657  hauscmplem  21686  1stcfb  21725  2ndcctbss  21735  ptbasfi  21861  pthaus  21918  txtube  21920  txhaus  21927  xkohaus  21933  kqnrmlem1  22023  kqnrmlem2  22024  nrmr0reg  22029  nrmhmph  22074  fbssint  22118  infil  22143  fgabs  22159  filconn  22163  filuni  22165  trfil2  22167  trfg  22171  ufprim  22189  elfm3  22230  rnelfm  22233  fmfnfmlem2  22235  fmfnfmlem4  22237  hausflimi  22260  hauspwpwf1  22267  fclsneii  22297  supnfcls  22300  flimfnfcls  22308  fclscmpi  22309  alexsublem  22324  ghmcnp  22394  qustgpopn  22399  psmetsym  22591  psmettri  22592  psmetge0  22593  psmetres2  22595  xmetge0  22625  xmetsym  22628  xmettri  22632  xmetres2  22642  prdsxmetlem  22649  prdsmet  22651  imasdsf1olem  22654  imasf1oxmet  22656  bldisj  22679  xblss2ps  22682  xblss2  22683  xmeter  22714  prdsbl  22772  metustexhalf  22837  metust  22839  nrmmetd  22855  ngpsubcan  22894  nmmtri  22902  nmrtri  22904  ngptgp  22916  nlmvscnlem2  22965  nrginvrcnlem  22971  metdcnlem  23115  clmvs2  23369  clmmulg  23376  clmnegneg  23379  clmnegsubdi2  23380  clmsub4  23381  cvsi  23405  cvsmuleqdivd  23409  cvsdiveqd  23410  ncvspi  23431  cphabscl  23460  cphsqrtcl2  23461  cphsqrtcl3  23462  cphnmf  23470  cph2ass  23488  cphassi  23489  cphassir  23490  ipcau2  23508  tcphcphlem2  23510  ipcnlem2  23518  cfilfcls  23548  iscau3  23552  iscmet3lem2  23566  iscmet3  23567  relcmpcmet  23592  minveclem2  23700  minveclem4  23706  pjthlem1  23711  pjthlem2  23712  uniioombllem4  23858  dyadmax  23870  itg1addlem4  23971  itg1climres  23986  ply1divex  24401  aalioulem2  24593  amgmlem  25237  dvdsppwf1o  25433  perfect1  25474  perfectlem1  25475  perfectlem2  25476  dchrptlem2  25511  colline  26105  ttgcontlem1  26342  axcontlem9  26429  eengtrkg  26443  eengtrkge  26444  nbfusgrlevtxm2  26831  nbusgrvtxm1  26832  elwwlks2ons3im  27408  usgr2wspthon  27419  clwwlknclwwlkdifnum  27433  numclwwlk5  27847  grpoidinvlem4  27963  grpoinvop  27989  grponpcan  27999  vcm  28032  nvmul0or  28106  nvpncan2  28109  nvdif  28122  nvabs  28128  smcnlem  28153  lnomul  28216  minvecolem2  28331  superpos  29810  ssnnssfz  30170  omndmul2  30343  omndmul3  30344  ogrpaddltbi  30349  ogrpaddltrbid  30351  ogrpsublt  30352  ogrpinvlt  30354  cyc3genpmlem  30389  isarchi3  30412  archirngz  30414  archiabllem1a  30416  archiabllem1  30418  archiabllem2a  30419  archiabllem2c  30420  slmdvs0  30449  gsumvsca1  30455  gsumvsca2  30456  lmodvslmhm  30457  dvdschrmulg  30467  dvrdir  30470  rdivmuldivd  30471  dvrcan5  30473  ornglmullt  30489  isarchiofld  30499  rhmdvd  30503  rhmunitinv  30504  eqgvscpbl  30528  imaslmod  30531  lbslsat  30573  fedgmullem1  30584  fedgmullem2  30585  psgnfzto1stlem  30620  pmtridfv1  30627  pmtridfv2  30628  mdetpmtr1  30659  mdetpmtr12  30661  mdetlap  30668  locfinref  30678  metideq  30706  metider  30707  pstmxmet  30710  lmxrge0  30768  qqhghm  30802  qqhrhm  30803  ispisys2  30985  rossros  31012  measdivcst  31056  oddpwdc  31185  ballotlemiex  31332  cvmopnlem  32089  cvmliftmolem2  32093  cvmliftlem6  32101  cvmliftlem8  32103  cvmliftlem9  32104  cvmlift2lem9  32122  cvmlift3lem2  32131  cvmlift3lem6  32135  cvmlift3lem7  32136  cvmlift3lem9  32138  sotrd  32554  frpomin  32632  frrlem13  32689  nodense  32750  nosupfv  32760  noetalem5  32775  cgrtriv  33017  cgrdegen  33019  cgrextend  33023  segconeq  33025  btwntriv2  33027  btwncomand  33030  btwntriv1  33031  btwnintr  33034  btwnexch3  33035  btwnouttr  33039  btwnexch  33040  trisegint  33043  ifscgr  33059  btwnxfr  33071  colineartriv1  33082  colineartriv2  33083  colinearxfr  33090  fscgr  33095  lineid  33098  idinside  33099  endofsegidand  33101  btwnconn1lem5  33106  btwnconn1lem7  33108  btwnconn1lem11  33112  btwnconn1lem12  33113  btwnconn1lem13  33114  brsegle2  33124  segleantisym  33130  broutsideof2  33137  btwnoutside  33140  outsideoftr  33144  outsideofeq  33145  outsideofeu  33146  outsidele  33147  lineunray  33162  lineelsb2  33163  linecom  33165  linethru  33168  neibastop1  33261  lindsadd  34362  lindsenlbs  34364  matunitlindflem1  34365  poimirlem28  34397  poimirlem32  34401  heicant  34404  mettrifi  34510  isbnd3  34540  heibor1lem  34565  bfplem2  34579  ghomdiv  34648  rngo2  34663  rngolz  34678  rngorz  34679  zerdivemp1x  34703  lfladdcl  35688  lflvscl  35694  eqlkr3  35718  lkrlsp  35719  lshpkrlem4  35730  oldmm1  35834  olj01  35842  latmassOLD  35846  latm32  35848  latmrot  35849  latm4  35850  olm01  35853  cmtcomlemN  35865  cmtbr3N  35871  cmtbr4N  35872  lecmtN  35873  omlfh1N  35875  atlen0  35927  atnle  35934  atlatmstc  35936  atlatle  35937  cvlexchb1  35947  cvlcvr1  35956  ishlat3N  35971  hlatjass  35987  hlatj12  35988  hlatj32  35989  hlsupr2  36004  hlhgt2  36006  hl0lt1N  36007  hlrelat  36019  hlrelat2  36020  exatleN  36021  hlrelat3  36029  cvrval5  36032  cvrexchlem  36036  cvratlem  36038  cvrat  36039  atcvr0eq  36043  lnnat  36044  atlt  36054  atlelt  36055  2atlt  36056  atexchltN  36058  cvrat3  36059  2atjm  36062  atbtwn  36063  4noncolr3  36070  athgt  36073  3dimlem3a  36077  3dimlem3OLDN  36079  3dimlem4a  36080  3dimlem4OLDN  36082  3dim1  36084  3dim2  36085  1cvratex  36090  ps-1  36094  ps-2  36095  hlatexch3N  36097  hlatexch4  36098  ps-2b  36099  3atlem1  36100  3atlem2  36101  3atlem5  36104  3atlem6  36105  llnnleat  36130  llncmp  36139  2at0mat0  36142  2atmat0  36143  2atm  36144  lplni2  36154  lvolex3N  36155  lplnnle2at  36158  lplnnleat  36159  lplnnlelln  36160  2atnelpln  36161  llncvrlpln  36175  2atmat  36178  lplncmp  36179  lplnexllnN  36181  2llnjaN  36183  2llnm4  36187  2llnmeqat  36188  lvolnle3at  36199  lvolnleat  36200  2atnelvolN  36204  islvol2aN  36209  4atlem3  36213  4atlem3a  36214  4atlem3b  36215  4atlem4a  36216  4atlem4b  36217  4atlem4c  36218  4atlem4d  36219  4atlem10  36223  4atlem11b  36225  4atlem11  36226  4atlem12b  36228  4atlem12  36229  4at2  36231  lplncvrlvol  36233  lvolcmp  36234  2lplnja  36236  dalemqrprot  36265  dalemply  36271  dalemsly  36272  dalemrot  36274  dalemrotyz  36275  dalem1  36276  dalemcea  36277  dalem3  36281  dalem5  36284  dalem8  36287  dalem-cly  36288  dalem11  36291  dalem12  36292  dalem16  36296  dalem17  36297  dalem18  36298  dalem21  36311  dalem24  36314  dalem25  36315  dalem38  36327  dalem39  36328  dalem44  36333  dalem54  36343  dalem55  36344  dalem57  36346  dalem58  36347  dalem59  36348  dalem60  36349  dath2  36354  2atm2atN  36402  2llnma1b  36403  2llnma3r  36405  cdlema1N  36408  cdlemblem  36410  paddasslem5  36441  paddasslem10  36446  paddasslem12  36448  paddasslem13  36449  paddass  36455  padd12N  36456  padd4N  36457  paddss  36462  pmodlem1  36463  pmodl42N  36468  pmapjoin  36469  pmapjlln1  36472  atmod1i2  36476  llnmod1i2  36477  llnexchb2  36486  dalawlem2  36489  dalawlem3  36490  dalawlem5  36492  dalawlem6  36493  dalawlem7  36494  dalawlem8  36495  dalawlem11  36498  dalawlem12  36499  dalawlem13  36500  pclunN  36515  osumcllem1N  36573  pexmidlem3N  36589  lhp2lt  36618  lhp0lt  36620  lhpexle2lem  36626  lhpexle3lem  36628  lhpocnle  36633  lhpj1  36639  lhpmcvr4N  36643  lhp2at0  36649  lhpat3  36663  4atexlemtlw  36684  4atexlemc  36686  4atexlemnclw  36687  4atexlemcnd  36689  lautcvr  36709  lautj  36710  lautm  36711  ltrnm  36748  ltrnj  36749  ltrncvr  36750  trlval3  36804  cdlemc5  36812  cdlemd2  36816  cdlemd3  36817  cdleme0e  36834  cdleme1  36844  cdleme3c  36847  cdleme3g  36851  cdleme3h  36852  cdleme3  36854  cdleme5  36857  cdleme7c  36862  cdleme7d  36863  cdleme7e  36864  cdleme7ga  36865  cdleme7  36866  cdleme9  36870  cdleme11c  36878  cdleme11g  36882  cdleme11k  36885  cdleme11  36887  cdleme12  36888  cdleme15b  36892  cdleme15d  36894  cdleme16d  36898  cdleme16e  36899  cdleme16f  36900  cdleme17b  36904  cdleme18b  36909  cdleme22gb  36911  cdlemednpq  36916  cdleme19a  36920  cdleme20aN  36926  cdleme20bN  36927  cdleme20c  36928  cdleme20d  36929  cdleme20j  36935  cdleme21c  36944  cdleme22aa  36956  cdleme22b  36958  cdleme22cN  36959  cdleme22d  36960  cdleme22e  36961  cdleme22eALTN  36962  cdleme23b  36967  cdleme23c  36968  cdleme28a  36987  cdleme30a  36995  cdlemefs29bpre0N  37033  cdlemefs29bpre1N  37034  cdlemefs29cpre1N  37035  cdlemefs29clN  37036  cdlemefs32fvaN  37039  cdlemefs32fva1  37040  cdleme32b  37059  cdleme32c  37060  cdleme32e  37062  cdleme35a  37065  cdleme35fnpq  37066  cdleme35b  37067  cdleme35f  37071  cdleme36a  37077  cdleme36m  37078  cdleme37m  37079  cdleme39a  37082  cdleme42c  37089  cdleme42i  37100  cdleme42keg  37103  cdleme42mgN  37105  cdleme48bw  37119  cdlemeg46fjgN  37138  cdlemeg46fjv  37140  cdlemeg46req  37146  cdleme50trn1  37166  cdlemf1  37178  cdlemf2  37179  cdlemg1cex  37205  cdlemg2fv2  37217  cdlemg7fvbwN  37224  cdlemg4c  37229  cdlemg4  37234  cdlemg6c  37237  cdlemg8b  37245  cdlemg10c  37256  cdlemg10  37258  cdlemg11b  37259  cdlemg12f  37265  cdlemg13a  37268  cdlemg17a  37278  cdlemg17dALTN  37281  cdlemg18b  37296  cdlemg19a  37300  cdlemg27a  37309  cdlemg27b  37313  cdlemg33b0  37318  cdlemg33a  37323  cdlemg35  37330  trlcolem  37343  cdlemg42  37346  cdlemg46  37352  trljco  37357  tendopltp  37397  cdlemh1  37432  cdlemh2  37433  cdlemi1  37435  cdlemi  37437  cdlemk3  37450  cdlemk10  37460  cdlemk11  37466  cdlemk15  37472  cdlemk1u  37476  cdlemk5u  37478  cdlemk11u  37488  cdlemk39  37533  cdlemkid1  37539  cdlemk50  37569  cdlemk51  37570  erngdvlem3-rN  37615  tendocnv  37638  tendospcanN  37640  dialss  37663  dia2dimlem1  37681  dia2dimlem2  37682  dia2dimlem3  37683  dia2dimlem10  37690  dia2dimlem12  37692  dvhvaddass  37714  dvhlveclem  37725  cdlemm10N  37735  doca2N  37743  djajN  37754  dib1dim2  37785  diblss  37787  diclspsn  37811  cdlemn2  37812  cdlemn10  37823  dihjustlem  37833  dihord1  37835  dihord2a  37836  dihord2pre2  37843  dib2dim  37860  dih2dimb  37861  dih2dimbALTN  37862  dihopelvalcpre  37865  dihord5b  37876  dihord6b  37877  dihord5apre  37879  dihmeetlem1N  37907  dihglblem5apreN  37908  dihglblem2N  37911  dihglbcpreN  37917  dihmeetbclemN  37921  dihmeetlem3N  37922  dihmeetlem6  37926  dih1dimatlem  37946  djhcvat42  38032  dihjatcclem1  38035  dihjatcclem4  38038  dvh4dimat  38055  lcfl7lem  38116  lclkrlem2m  38136  lcfrlem1  38159  lcdvsass  38224  baerlem3lem1  38324  baerlem5alem1  38325  baerlem5blem1  38326  mapdh6gN  38359  mapdh6hN  38360  hdmap1l6g  38433  hdmap1l6h  38434  hdmapneg  38463  hdmap14lem8  38492  hgmapadd  38511  hgmapmul  38512  hgmapvvlem1  38540  prjspertr  38702  irrapxlem5  38859  aomclem2  39091  isnumbasgrplem2  39140  mpaaeu  39186  mendring  39228  mendlmod  39229  relexpnul  39459  ablsimpgfindlem1  40117  caofcan  40145  disjiun2  40811  wessf1ornlem  40938  fisupclrnmpt  41166  limsupequzlem  41499  cnrefiisplem  41606  stoweidlem18  41799  stoweidlem41  41822  stoweidlem45  41826  stoweidlem55  41836  fourierdlem25  41913  fourierdlem31  41919  fourierdlem37  41925  fourierdlem42  41930  etransclem48  42063  ioorrnopnlem  42085  issalgend  42117  sge0iunmptlemfi  42191  hoicvr  42326  hoidmvlelem2  42374  iunhoiioolem  42453  vonioolem1  42458  prproropf1olem2  43102  prmdvdsfmtnof1lem1  43182  prmdvdsfmtnof  43184  sgprmdvdsmersenne  43205  perfectALTVlem1  43322  perfectALTVlem2  43323  rnglz  43587  ssnn0ssfz  43829  zlmodzxzsub  43840  invginvrid  43849  lmodvsmdi  43864  ply1sclrmsm  43871  lincsum  43918  lincscm  43919  lindslinindimp2lem4  43950  lindslinindsimp2lem5  43951  ldepsprlem  43961  lincresunit3lem1  43968  lincresunit3lem2  43969  isldepslvec2  43974  relogbmulbexp  44056