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

Theorem mulassd 7193
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
mulassd  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )

Proof of Theorem mulassd
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 mulass 7155 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1170 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285    e. wcel 1434  (class class class)co 5537   CCcc 7030    x. cmul 7037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-mulass 7130
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  ltmul1  7748  recexap  7799  mulap0  7800  mulcanapd  7807  receuap  7815  divmulasscomap  7840  divdivdivap  7857  divmuleqap  7861  conjmulap  7873  apmul1  7932  qapne  8794  modqmul1  9448  modqdi  9463  expadd  9604  mulbinom2  9675  binom3  9676  faclbnd  9754  faclbnd6  9757  bcm1k  9773  bcp1nk  9775  ibcval5  9776  crre  9871  remullem  9885  resqrexlemcalc1  10027  resqrexlemnm  10031  amgm2  10131  dvdsmulcr  10359  dvdsmulgcd  10547  qredeq  10611  2sqpwodd  10687
  Copyright terms: Public domain W3C validator