Theorem mul12d 11332

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   · cmul 11021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-mulcom 11080  ax-mulass 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  divrec  11802  remullem  15045  sqreulem  15277  cvgrat  15800  binomrisefac  15959  tanval3  16053  sinadd  16083  dvdsmulgcd  16477  lcmgcdlem  16527  cncongr1  16588  prmdiv  16706  vdwlem6  16908  itgmulc2  25772  dvexp3  25919  aaliou3lem8  26290  dvradcnv  26367  pserdvlem2  26375  abelthlem6  26383  abelthlem7  26385  tangtx  26451  tanarg  26565  dvcxp1  26686  dvcncxp1  26689  heron  26785  dcubic1  26792  mcubic  26794  dquart  26800  quart1  26803  quartlem1  26804  asinsin  26839  lgamgulmlem2  26977  basellem3  27030  bcp1ctr  27227  gausslemma2dlem6  27320  lgseisenlem2  27324  lgseisenlem4  27326  lgsquadlem1  27328  2sqlem4  27369  chebbnd1lem3  27419  rpvmasum2  27460  mulog2sumlem3  27484  selberglem1  27493  selberg4lem1  27508  selberg3r  27517  selberg34r  27519  pntrlog2bndlem4  27528  pntrlog2bndlem6  27531  pntlemr  27550  pntlemk  27554  ostth2lem3  27583  colinearalglem4  28898  branmfn  32096  constrrtlc1  33756  constrrtcclem  33758  constrmulcl  33795  cos9thpiminplylem2  33807  vtsprod  34663  hgt750leme  34682  faclimlem1  35798  itgmulc2nc  37738  areacirclem1  37758  3factsumint2  42125  lcmineqlem10  42141  lcmineqlem11  42142  posbezout  42203  readvrec2  42469  pellexlem6  42941  pell1234qrmulcl  42962  rmxyadd  43028  jm2.18  43095  jm2.19lem1  43096  jm2.22  43102  jm2.20nn  43104  proot1ex  43303  sqrtcval  43748  ofmul12  44432  binomcxplemnotnn0  44463  sineq0ALT  45043  mul13d  45395  stoweidlem11  46123  wallispi2lem1  46183  stirlinglem1  46186  stirlinglem3  46188  stirlinglem7  46192  stirlinglem15  46200  dirkertrigeqlem3  46212  dirkercncflem2  46216  fourierdlem66  46284  fourierdlem83  46301  etransclem23  46369  mod42tp1mod8  47716  fppr2odd  47845  2zlidl  48354  itcovalt2lem2lem2  48789  itsclc0yqsollem1  48877  itscnhlc0xyqsol  48880  itscnhlinecirc02plem1  48897