MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul12 Structured version   Visualization version   GIF version

Theorem mul12 11378
Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
Assertion
Ref Expression
mul12 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ)))

Proof of Theorem mul12
StepHypRef Expression
1 mulcom 11193 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))
21oveq1d 7417 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ))
323adant3 1129 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ))
4 mulass 11195 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))
5 mulass 11195 . . 3 ((๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ)))
653com12 1120 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ)))
73, 4, 63eqtr3d 2772 1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  (class class class)co 7402  โ„‚cc 11105   ยท cmul 11112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-mulcom 11171  ax-mulass 11173
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405
This theorem is referenced by:  mul02  11391  mul12i  11408  mul12d  11422  mulre  15070  sqreulem  15308  fsumcube  16006  demoivre  16146  demoivreALT  16147  dvdscmul  16229  dvdscmulr  16231  dvdstr  16240  ablfacrp  19984  nmoleub2lem3  24986  sinperlem  26355  coskpi  26397  sineq0  26398  efif1olem4  26419  rpvmasum2  27385  expgrowthi  43641
  Copyright terms: Public domain W3C validator