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

Theorem mulassd 8006
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 7967 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1249 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 2160  (class class class)co 5892   CCcc 7834    x. cmul 7841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 7939
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  ltmul1  8574  recexap  8635  mulap0  8636  mulcanapd  8643  receuap  8651  divmulasscomap  8678  divdivdivap  8695  divmuleqap  8699  conjmulap  8711  apmul1  8770  qapne  9664  modqmul1  10403  modqdi  10418  expadd  10588  mulbinom2  10663  binom3  10664  faclbnd  10748  faclbnd6  10751  bcm1k  10767  bcp1nk  10769  bcval5  10770  crre  10893  remullem  10907  resqrexlemcalc1  11050  resqrexlemnm  11054  amgm2  11154  binomlem  11518  geo2sum  11549  mertenslemi1  11570  clim2prod  11574  sinadd  11771  tanaddap  11774  dvdsmulcr  11855  dvdsmulgcd  12053  qredeq  12123  2sqpwodd  12203  pcaddlem  12366  prmpwdvds  12382  dvexp  14612  tangtx  14696  cxpmul  14770  binom4  14834  lgsneg  14863  lgseisenlem1  14888  lgseisenlem2  14889  2lgsoddprmlem2  14892  2sqlem3  14902
  Copyright terms: Public domain W3C validator