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

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

Proof of Theorem mul12
StepHypRef Expression
1 mulcom 11224 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))
21oveq1d 7435 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ))
323adant3 1130 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ))
4 mulass 11226 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))
5 mulass 11226 . . 3 ((๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ)))
653com12 1121 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ)))
73, 4, 63eqtr3d 2776 1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099  (class class class)co 7420  โ„‚cc 11136   ยท cmul 11143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-mulcom 11202  ax-mulass 11204
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423
This theorem is referenced by:  mul02  11422  mul12i  11439  mul12d  11453  mulre  15100  sqreulem  15338  fsumcube  16036  demoivre  16176  demoivreALT  16177  dvdscmul  16259  dvdscmulr  16261  dvdstr  16270  ablfacrp  20022  nmoleub2lem3  25041  sinperlem  26414  coskpi  26456  sineq0  26457  efif1olem4  26478  rpvmasum2  27444  expgrowthi  43770
  Copyright terms: Public domain W3C validator