Theorem mul12d 11354

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-mulcom 11102  ax-mulass 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  divrec  11824  remullem  15063  sqreulem  15295  cvgrat  15818  binomrisefac  15977  tanval3  16071  sinadd  16101  dvdsmulgcd  16495  lcmgcdlem  16545  cncongr1  16606  prmdiv  16724  vdwlem6  16926  itgmulc2  25803  dvexp3  25950  aaliou3lem8  26321  dvradcnv  26398  pserdvlem2  26406  abelthlem6  26414  abelthlem7  26416  tangtx  26482  tanarg  26596  dvcxp1  26717  dvcncxp1  26720  heron  26816  dcubic1  26823  mcubic  26825  dquart  26831  quart1  26834  quartlem1  26835  asinsin  26870  lgamgulmlem2  27008  basellem3  27061  bcp1ctr  27258  gausslemma2dlem6  27351  lgseisenlem2  27355  lgseisenlem4  27357  lgsquadlem1  27359  2sqlem4  27400  chebbnd1lem3  27450  rpvmasum2  27491  mulog2sumlem3  27515  selberglem1  27524  selberg4lem1  27539  selberg3r  27548  selberg34r  27550  pntrlog2bndlem4  27559  pntrlog2bndlem6  27562  pntlemr  27581  pntlemk  27585  ostth2lem3  27614  colinearalglem4  28994  branmfn  32192  constrrtlc1  33909  constrrtcclem  33911  constrmulcl  33948  cos9thpiminplylem2  33960  vtsprod  34816  hgt750leme  34835  faclimlem1  35956  itgmulc2nc  37928  areacirclem1  37948  3factsumint2  42381  lcmineqlem10  42397  lcmineqlem11  42398  posbezout  42459  readvrec2  42720  pellexlem6  43180  pell1234qrmulcl  43201  rmxyadd  43267  jm2.18  43334  jm2.19lem1  43335  jm2.22  43341  jm2.20nn  43343  proot1ex  43542  sqrtcval  43986  ofmul12  44670  binomcxplemnotnn0  44701  sineq0ALT  45281  mul13d  45631  stoweidlem11  46358  wallispi2lem1  46418  stirlinglem1  46421  stirlinglem3  46423  stirlinglem7  46427  stirlinglem15  46435  dirkertrigeqlem3  46447  dirkercncflem2  46451  fourierdlem66  46519  fourierdlem83  46536  etransclem23  46604  mod42tp1mod8  47951  fppr2odd  48080  2zlidl  48589  itcovalt2lem2lem2  49023  itsclc0yqsollem1  49111  itscnhlc0xyqsol  49114  itscnhlinecirc02plem1  49131