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

Theorem mulassd 7661
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 7623 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1299    e. wcel 1448  (class class class)co 5706   CCcc 7498    x. cmul 7505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-mulass 7598
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  ltmul1  8220  recexap  8275  mulap0  8276  mulcanapd  8283  receuap  8291  divmulasscomap  8317  divdivdivap  8334  divmuleqap  8338  conjmulap  8350  apmul1  8409  qapne  9281  modqmul1  9991  modqdi  10006  expadd  10176  mulbinom2  10249  binom3  10250  faclbnd  10328  faclbnd6  10331  bcm1k  10347  bcp1nk  10349  bcval5  10350  crre  10470  remullem  10484  resqrexlemcalc1  10626  resqrexlemnm  10630  amgm2  10730  binomlem  11091  geo2sum  11122  mertenslemi1  11143  sinadd  11241  tanaddap  11244  dvdsmulcr  11318  dvdsmulgcd  11506  qredeq  11570  2sqpwodd  11646
  Copyright terms: Public domain W3C validator