Theorem mulass 9601

Description: Alias for ax-mulass 9579, for naming consistency with mulassi 9626. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulass

Proof of Theorem mulass

Step	Hyp	Ref	Expression
1		ax-mulass 9579	1

Syntax hints:  ->wi 4  /\w3a 973  =wceq 1395  e.wcel 1818  (class class class)co 6296  cc 9511  cmul 9518

This theorem is referenced by:  mulid1  9614  mulassi  9626  mulassd  9640  mul12  9767  mul32  9768  mul31  9769  mul4  9770  00id  9776  divass  10250  cju  10557  xmulasslem3  11507  faclbnd5  12376  bcval5  12396  remim  12950  imval2  12984  sqrlem7  13082  sqrtneglem  13100  sqreulem  13192  clim2div  13698  prodfmul  13699  prodmolem3  13740  sinhval  13889  coshval  13890  absefib  13933  efieq1re  13934  muldvds1  14008  muldvds2  14009  dvdsmulc  14011  dvdsmulcr  14013  dvdstr  14018  eulerthlem2  14312  ablfacrp  17117  cncrng  18439  nmoleub2lem3  21598  itg2mulc  22154  abssinper  22911  sinasin  23220  dchrabl  23529  bposlem6  23564  bposlem9  23567  lgsdir  23605  lgsdi  23607  2sqlem6  23644  rpvmasum2  23697  ablomul  25357  cnrngo  25405  cncvc  25476  ipasslem5  25750  ipasslem11  25755  dvasin  30103  pellexlem2  30766  jm2.25  30941  expgrowth  31240  2zrngmsgrp  32753

This theorem was proved from axioms:  ax-mulass 9579