Theorem mul12d 10838

Description: Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addcand.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mul12d	⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Proof of Theorem mul12d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcand.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mul12 10794	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1368	1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-mulcom 10590  ax-mulass 10592

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  divrec  11303  remullem  14479  sqreulem  14711  cvgrat  15231  binomrisefac  15388  tanval3  15479  sinadd  15509  dvdsmulgcd  15895  lcmgcdlem  15940  cncongr1  16001  prmdiv  16112  vdwlem6  16312  itgmulc2  24437  dvexp3  24581  aaliou3lem8  24941  dvradcnv  25016  pserdvlem2  25023  abelthlem6  25031  abelthlem7  25033  tangtx  25098  tanarg  25210  dvcxp1  25329  dvcncxp1  25332  heron  25424  dcubic1  25431  mcubic  25433  dquart  25439  quart1  25442  quartlem1  25443  asinsin  25478  lgamgulmlem2  25615  basellem3  25668  bcp1ctr  25863  gausslemma2dlem6  25956  lgseisenlem2  25960  lgseisenlem4  25962  lgsquadlem1  25964  2sqlem4  26005  chebbnd1lem3  26055  rpvmasum2  26096  mulog2sumlem3  26120  selberglem1  26129  selberg4lem1  26144  selberg3r  26153  selberg34r  26155  pntrlog2bndlem4  26164  pntrlog2bndlem6  26167  pntlemr  26186  pntlemk  26190  ostth2lem3  26219  colinearalglem4  26703  branmfn  29888  vtsprod  32020  hgt750leme  32039  faclimlem1  33088  itgmulc2nc  35125  areacirclem1  35145  3factsumint2  39310  lcmineqlem10  39326  lcmineqlem11  39327  pellexlem6  39775  pell1234qrmulcl  39796  rmxyadd  39862  jm2.18  39929  jm2.19lem1  39930  jm2.22  39936  jm2.20nn  39938  proot1ex  40145  sqrtcval  40341  ofmul12  41029  binomcxplemnotnn0  41060  sineq0ALT  41643  mul13d  41910  stoweidlem11  42653  wallispi2lem1  42713  stirlinglem1  42716  stirlinglem3  42718  stirlinglem7  42722  stirlinglem15  42730  dirkertrigeqlem3  42742  dirkercncflem2  42746  fourierdlem66  42814  fourierdlem83  42831  etransclem23  42899  mod42tp1mod8  44120  fppr2odd  44249  2zlidl  44558  itcovalt2lem2lem2  45088  itsclc0yqsollem1  45176  itscnhlc0xyqsol  45179  itscnhlinecirc02plem1  45196