Theorem mul12d 11343

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-mulcom 11092  ax-mulass 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  divrec  11813  remullem  15053  sqreulem  15285  cvgrat  15808  binomrisefac  15967  tanval3  16061  sinadd  16091  dvdsmulgcd  16485  lcmgcdlem  16535  cncongr1  16596  prmdiv  16714  vdwlem6  16916  itgmulc2  25751  dvexp3  25898  aaliou3lem8  26269  dvradcnv  26346  pserdvlem2  26354  abelthlem6  26362  abelthlem7  26364  tangtx  26430  tanarg  26544  dvcxp1  26665  dvcncxp1  26668  heron  26764  dcubic1  26771  mcubic  26773  dquart  26779  quart1  26782  quartlem1  26783  asinsin  26818  lgamgulmlem2  26956  basellem3  27009  bcp1ctr  27206  gausslemma2dlem6  27299  lgseisenlem2  27303  lgseisenlem4  27305  lgsquadlem1  27307  2sqlem4  27348  chebbnd1lem3  27398  rpvmasum2  27439  mulog2sumlem3  27463  selberglem1  27472  selberg4lem1  27487  selberg3r  27496  selberg34r  27498  pntrlog2bndlem4  27507  pntrlog2bndlem6  27510  pntlemr  27529  pntlemk  27533  ostth2lem3  27562  colinearalglem4  28872  branmfn  32067  constrrtlc1  33698  constrrtcclem  33700  constrmulcl  33737  cos9thpiminplylem2  33749  vtsprod  34606  hgt750leme  34625  faclimlem1  35715  itgmulc2nc  37667  areacirclem1  37687  3factsumint2  41995  lcmineqlem10  42011  lcmineqlem11  42012  posbezout  42073  readvrec2  42334  pellexlem6  42807  pell1234qrmulcl  42828  rmxyadd  42894  jm2.18  42961  jm2.19lem1  42962  jm2.22  42968  jm2.20nn  42970  proot1ex  43169  sqrtcval  43614  ofmul12  44298  binomcxplemnotnn0  44329  sineq0ALT  44910  mul13d  45262  stoweidlem11  45993  wallispi2lem1  46053  stirlinglem1  46056  stirlinglem3  46058  stirlinglem7  46062  stirlinglem15  46070  dirkertrigeqlem3  46082  dirkercncflem2  46086  fourierdlem66  46154  fourierdlem83  46171  etransclem23  46239  mod42tp1mod8  47587  fppr2odd  47716  2zlidl  48212  itcovalt2lem2lem2  48647  itsclc0yqsollem1  48735  itscnhlc0xyqsol  48738  itscnhlinecirc02plem1  48755