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

Theorem mulass 7452
Description: Alias for ax-mulass 7427, for naming consistency with mulassi 7476. (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 7427 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 924    = wceq 1289    e. wcel 1438  (class class class)co 5634   CCcc 7327    x. cmul 7334
This theorem was proved from axioms:  ax-mulass 7427
This theorem is referenced by:  mulid1  7464  mulassi  7476  mulassd  7490  mul12  7590  mul32  7591  mul31  7592  mul4  7593  rimul  8038  divassap  8131  cju  8393  div4p1lem1div2  8639  mulbinom2  10035  sqoddm1div8  10071  remim  10259  imval2  10293  muldvds1  10914  muldvds2  10915  dvdsmulc  10917  dvdstr  10926
  Copyright terms: Public domain W3C validator