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

Theorem mulass 7070
Description: Alias for ax-mulass 7045, for naming consistency with mulassi 7094. (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 7045 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 896    = wceq 1259    e. wcel 1409  (class class class)co 5540   CCcc 6945    x. cmul 6952
This theorem was proved from axioms:  ax-mulass 7045
This theorem is referenced by:  mulid1  7082  mulassi  7094  mulassd  7108  mul12  7203  mul32  7204  mul31  7205  mul4  7206  rimul  7650  divassap  7743  cju  7989  div4p1lem1div2  8235  mulbinom2  9533  sqoddm1div8  9569  remim  9688  imval2  9722  muldvds1  10132  muldvds2  10133  dvdsmulc  10135  dvdstr  10144
  Copyright terms: Public domain W3C validator