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

Theorem mulass 7623
Description: Alias for ax-mulass 7598, for naming consistency with mulassi 7647. (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 7598 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 930    = wceq 1299    e. wcel 1448  (class class class)co 5706   CCcc 7498    x. cmul 7505
This theorem was proved from axioms:  ax-mulass 7598
This theorem is referenced by:  mulid1  7635  mulassi  7647  mulassd  7661  mul12  7762  mul32  7763  mul31  7764  mul4  7765  rimul  8213  divassap  8311  cju  8577  div4p1lem1div2  8825  mulbinom2  10249  sqoddm1div8  10285  remim  10473  imval2  10507  absefib  11274  efieq1re  11275  muldvds1  11313  muldvds2  11314  dvdsmulc  11316  dvdstr  11325
  Copyright terms: Public domain W3C validator