ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulass Unicode version

Theorem mulass 7972
Description: Alias for ax-mulass 7944, for naming consistency with mulassi 7996. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7944 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 980    = wceq 1364    e. wcel 2160  (class class class)co 5896   CCcc 7839    x. cmul 7846
This theorem was proved from axioms:  ax-mulass 7944
This theorem is referenced by:  mulrid  7984  mulassi  7996  mulassd  8011  mul12  8116  mul32  8117  mul31  8118  mul4  8119  rimul  8572  divassap  8677  cju  8948  div4p1lem1div2  9202  mulbinom2  10668  sqoddm1div8  10705  remim  10901  imval2  10935  clim2divap  11580  prod3fmul  11581  prodmodclem3  11615  absefib  11810  efieq1re  11811  muldvds1  11855  muldvds2  11856  dvdsmulc  11858  dvdstr  11867  oddprmdvds  12386  cncrng  13872  abssinper  14724  2sqlem6  14925
  Copyright terms: Public domain W3C validator