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

Theorem mulassd 7936
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 7898 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1233 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348    e. wcel 2141  (class class class)co 5851   CCcc 7765    x. cmul 7772
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 7870
This theorem depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  ltmul1  8504  recexap  8564  mulap0  8565  mulcanapd  8572  receuap  8580  divmulasscomap  8606  divdivdivap  8623  divmuleqap  8627  conjmulap  8639  apmul1  8698  qapne  9591  modqmul1  10326  modqdi  10341  expadd  10511  mulbinom2  10585  binom3  10586  faclbnd  10668  faclbnd6  10671  bcm1k  10687  bcp1nk  10689  bcval5  10690  crre  10814  remullem  10828  resqrexlemcalc1  10971  resqrexlemnm  10975  amgm2  11075  binomlem  11439  geo2sum  11470  mertenslemi1  11491  clim2prod  11495  sinadd  11692  tanaddap  11695  dvdsmulcr  11776  dvdsmulgcd  11973  qredeq  12043  2sqpwodd  12123  pcaddlem  12285  prmpwdvds  12300  dvexp  13434  tangtx  13518  cxpmul  13592  binom4  13656  lgsneg  13684  2sqlem3  13712
  Copyright terms: Public domain W3C validator