Theorem mul12d 11346

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028   · cmul 11035

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 11094  ax-mulass 11096

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  divrec  11816  remullem  15055  sqreulem  15287  cvgrat  15810  binomrisefac  15969  tanval3  16063  sinadd  16093  dvdsmulgcd  16487  lcmgcdlem  16537  cncongr1  16598  prmdiv  16716  vdwlem6  16918  itgmulc2  25795  dvexp3  25942  aaliou3lem8  26313  dvradcnv  26390  pserdvlem2  26398  abelthlem6  26406  abelthlem7  26408  tangtx  26474  tanarg  26588  dvcxp1  26709  dvcncxp1  26712  heron  26808  dcubic1  26815  mcubic  26817  dquart  26823  quart1  26826  quartlem1  26827  asinsin  26862  lgamgulmlem2  27000  basellem3  27053  bcp1ctr  27250  gausslemma2dlem6  27343  lgseisenlem2  27347  lgseisenlem4  27349  lgsquadlem1  27351  2sqlem4  27392  chebbnd1lem3  27442  rpvmasum2  27483  mulog2sumlem3  27507  selberglem1  27516  selberg4lem1  27531  selberg3r  27540  selberg34r  27542  pntrlog2bndlem4  27551  pntrlog2bndlem6  27554  pntlemr  27573  pntlemk  27577  ostth2lem3  27606  colinearalglem4  28965  branmfn  32163  constrrtlc1  33870  constrrtcclem  33872  constrmulcl  33909  cos9thpiminplylem2  33921  vtsprod  34777  hgt750leme  34796  faclimlem1  35918  itgmulc2nc  37860  areacirclem1  37880  3factsumint2  42313  lcmineqlem10  42329  lcmineqlem11  42330  posbezout  42391  readvrec2  42652  pellexlem6  43112  pell1234qrmulcl  43133  rmxyadd  43199  jm2.18  43266  jm2.19lem1  43267  jm2.22  43273  jm2.20nn  43275  proot1ex  43474  sqrtcval  43918  ofmul12  44602  binomcxplemnotnn0  44633  sineq0ALT  45213  mul13d  45564  stoweidlem11  46291  wallispi2lem1  46351  stirlinglem1  46354  stirlinglem3  46356  stirlinglem7  46360  stirlinglem15  46368  dirkertrigeqlem3  46380  dirkercncflem2  46384  fourierdlem66  46452  fourierdlem83  46469  etransclem23  46537  mod42tp1mod8  47884  fppr2odd  48013  2zlidl  48522  itcovalt2lem2lem2  48956  itsclc0yqsollem1  49044  itscnhlc0xyqsol  49047  itscnhlinecirc02plem1  49064