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

Theorem mulassd 7983
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
addcld.2 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
addassd.3 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
Assertion
Ref Expression
mulassd (๐œ‘ โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))

Proof of Theorem mulassd
StepHypRef Expression
1 addcld.1 . 2 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 addcld.2 . 2 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
3 addassd.3 . 2 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
4 mulass 7944 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))
51, 2, 3, 4syl3anc 1238 1 (๐œ‘ โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   = wceq 1353   โˆˆ wcel 2148  (class class class)co 5877  โ„‚cc 7811   ยท cmul 7818
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 7916
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  ltmul1  8551  recexap  8612  mulap0  8613  mulcanapd  8620  receuap  8628  divmulasscomap  8655  divdivdivap  8672  divmuleqap  8676  conjmulap  8688  apmul1  8747  qapne  9641  modqmul1  10379  modqdi  10394  expadd  10564  mulbinom2  10639  binom3  10640  faclbnd  10723  faclbnd6  10726  bcm1k  10742  bcp1nk  10744  bcval5  10745  crre  10868  remullem  10882  resqrexlemcalc1  11025  resqrexlemnm  11029  amgm2  11129  binomlem  11493  geo2sum  11524  mertenslemi1  11545  clim2prod  11549  sinadd  11746  tanaddap  11749  dvdsmulcr  11830  dvdsmulgcd  12028  qredeq  12098  2sqpwodd  12178  pcaddlem  12340  prmpwdvds  12355  dvexp  14260  tangtx  14344  cxpmul  14418  binom4  14482  lgsneg  14510  lgseisenlem1  14535  lgseisenlem2  14536  2lgsoddprmlem2  14539  2sqlem3  14549
  Copyright terms: Public domain W3C validator