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

Theorem mul12 11376
Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
Assertion
Ref Expression
mul12 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Proof of Theorem mul12
StepHypRef Expression
1 mulcom 11192 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
21oveq1d 7416 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐵 · 𝐴) · 𝐶))
323adant3 1129 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐵 · 𝐴) · 𝐶))
4 mulass 11194 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5 mulass 11194 . . 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 7401  cc 11104   · cmul 11111
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 11170  ax-mulass 11172
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 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404
This theorem is referenced by:  mul02  11389  mul12i  11406  mul12d  11420  mulre  15065  sqreulem  15303  fsumcube  16001  demoivre  16140  demoivreALT  16141  dvdscmul  16223  dvdscmulr  16225  dvdstr  16234  ablfacrp  19978  nmoleub2lem3  24964  sinperlem  26332  coskpi  26374  sineq0  26375  efif1olem4  26396  rpvmasum2  27361  expgrowthi  43581
  Copyright terms: Public domain W3C validator