Theorem mul12d 11423

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 11379	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1372	1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-mulcom 11174  ax-mulass 11176

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  divrec  11888  remullem  15075  sqreulem  15306  cvgrat  15829  binomrisefac  15986  tanval3  16077  sinadd  16107  dvdsmulgcd  16497  lcmgcdlem  16543  cncongr1  16604  prmdiv  16718  vdwlem6  16919  itgmulc2  25351  dvexp3  25495  aaliou3lem8  25858  dvradcnv  25933  pserdvlem2  25940  abelthlem6  25948  abelthlem7  25950  tangtx  26015  tanarg  26127  dvcxp1  26248  dvcncxp1  26251  heron  26343  dcubic1  26350  mcubic  26352  dquart  26358  quart1  26361  quartlem1  26362  asinsin  26397  lgamgulmlem2  26534  basellem3  26587  bcp1ctr  26782  gausslemma2dlem6  26875  lgseisenlem2  26879  lgseisenlem4  26881  lgsquadlem1  26883  2sqlem4  26924  chebbnd1lem3  26974  rpvmasum2  27015  mulog2sumlem3  27039  selberglem1  27048  selberg4lem1  27063  selberg3r  27072  selberg34r  27074  pntrlog2bndlem4  27083  pntrlog2bndlem6  27086  pntlemr  27105  pntlemk  27109  ostth2lem3  27138  colinearalglem4  28167  branmfn  31358  vtsprod  33651  hgt750leme  33670  faclimlem1  34713  itgmulc2nc  36556  areacirclem1  36576  3factsumint2  40887  lcmineqlem10  40903  lcmineqlem11  40904  pellexlem6  41572  pell1234qrmulcl  41593  rmxyadd  41660  jm2.18  41727  jm2.19lem1  41728  jm2.22  41734  jm2.20nn  41736  proot1ex  41943  sqrtcval  42392  ofmul12  43084  binomcxplemnotnn0  43115  sineq0ALT  43698  mul13d  43989  stoweidlem11  44727  wallispi2lem1  44787  stirlinglem1  44790  stirlinglem3  44792  stirlinglem7  44796  stirlinglem15  44804  dirkertrigeqlem3  44816  dirkercncflem2  44820  fourierdlem66  44888  fourierdlem83  44905  etransclem23  44973  mod42tp1mod8  46270  fppr2odd  46399  2zlidl  46832  itcovalt2lem2lem2  47360  itsclc0yqsollem1  47448  itscnhlc0xyqsol  47451  itscnhlinecirc02plem1  47468