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

Theorem mulassd 7808
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 7770 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1216 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480  (class class class)co 5777   CCcc 7637    x. cmul 7644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-mulass 7742
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  ltmul1  8373  recexap  8433  mulap0  8434  mulcanapd  8441  receuap  8449  divmulasscomap  8475  divdivdivap  8492  divmuleqap  8496  conjmulap  8508  apmul1  8567  qapne  9453  modqmul1  10174  modqdi  10189  expadd  10359  mulbinom2  10432  binom3  10433  faclbnd  10511  faclbnd6  10514  bcm1k  10530  bcp1nk  10532  bcval5  10533  crre  10653  remullem  10667  resqrexlemcalc1  10810  resqrexlemnm  10814  amgm2  10914  binomlem  11276  geo2sum  11307  mertenslemi1  11328  clim2prod  11332  sinadd  11466  tanaddap  11469  dvdsmulcr  11546  dvdsmulgcd  11736  qredeq  11800  2sqpwodd  11877  dvexp  12870  tangtx  12953  cxpmul  13027
  Copyright terms: Public domain W3C validator