Theorem mul12d 11452

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135   · cmul 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-mulcom 11201  ax-mulass 11203

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416

This theorem is referenced by:  divrec  11920  remullem  15150  sqreulem  15381  cvgrat  15902  binomrisefac  16061  tanval3  16153  sinadd  16183  dvdsmulgcd  16576  lcmgcdlem  16626  cncongr1  16687  prmdiv  16805  vdwlem6  17007  itgmulc2  25806  dvexp3  25953  aaliou3lem8  26324  dvradcnv  26401  pserdvlem2  26409  abelthlem6  26417  abelthlem7  26419  tangtx  26484  tanarg  26598  dvcxp1  26719  dvcncxp1  26722  heron  26818  dcubic1  26825  mcubic  26827  dquart  26833  quart1  26836  quartlem1  26837  asinsin  26872  lgamgulmlem2  27010  basellem3  27063  bcp1ctr  27260  gausslemma2dlem6  27353  lgseisenlem2  27357  lgseisenlem4  27359  lgsquadlem1  27361  2sqlem4  27402  chebbnd1lem3  27452  rpvmasum2  27493  mulog2sumlem3  27517  selberglem1  27526  selberg4lem1  27541  selberg3r  27550  selberg34r  27552  pntrlog2bndlem4  27561  pntrlog2bndlem6  27564  pntlemr  27583  pntlemk  27587  ostth2lem3  27616  colinearalglem4  28855  branmfn  32053  constrrtlc1  33717  constrrtcclem  33719  constrmulcl  33756  vtsprod  34629  hgt750leme  34648  faclimlem1  35718  itgmulc2nc  37670  areacirclem1  37690  3factsumint2  41998  lcmineqlem10  42014  lcmineqlem11  42015  posbezout  42076  readvrec2  42370  pellexlem6  42823  pell1234qrmulcl  42844  rmxyadd  42911  jm2.18  42978  jm2.19lem1  42979  jm2.22  42985  jm2.20nn  42987  proot1ex  43186  sqrtcval  43631  ofmul12  44316  binomcxplemnotnn0  44347  sineq0ALT  44929  mul13d  45263  stoweidlem11  45998  wallispi2lem1  46058  stirlinglem1  46061  stirlinglem3  46063  stirlinglem7  46067  stirlinglem15  46075  dirkertrigeqlem3  46087  dirkercncflem2  46091  fourierdlem66  46159  fourierdlem83  46176  etransclem23  46244  mod42tp1mod8  47562  fppr2odd  47691  2zlidl  48129  itcovalt2lem2lem2  48568  itsclc0yqsollem1  48656  itscnhlc0xyqsol  48659  itscnhlinecirc02plem1  48676