Theorem mul12d 11314

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996   · cmul 11003

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 2112  ax-9 2120  ax-ext 2702  ax-mulcom 11062  ax-mulass 11064

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344

This theorem is referenced by:  divrec  11784  remullem  15027  sqreulem  15259  cvgrat  15782  binomrisefac  15941  tanval3  16035  sinadd  16065  dvdsmulgcd  16459  lcmgcdlem  16509  cncongr1  16570  prmdiv  16688  vdwlem6  16890  itgmulc2  25755  dvexp3  25902  aaliou3lem8  26273  dvradcnv  26350  pserdvlem2  26358  abelthlem6  26366  abelthlem7  26368  tangtx  26434  tanarg  26548  dvcxp1  26669  dvcncxp1  26672  heron  26768  dcubic1  26775  mcubic  26777  dquart  26783  quart1  26786  quartlem1  26787  asinsin  26822  lgamgulmlem2  26960  basellem3  27013  bcp1ctr  27210  gausslemma2dlem6  27303  lgseisenlem2  27307  lgseisenlem4  27309  lgsquadlem1  27311  2sqlem4  27352  chebbnd1lem3  27402  rpvmasum2  27443  mulog2sumlem3  27467  selberglem1  27476  selberg4lem1  27491  selberg3r  27500  selberg34r  27502  pntrlog2bndlem4  27511  pntrlog2bndlem6  27514  pntlemr  27533  pntlemk  27537  ostth2lem3  27566  colinearalglem4  28880  branmfn  32075  constrrtlc1  33735  constrrtcclem  33737  constrmulcl  33774  cos9thpiminplylem2  33786  vtsprod  34642  hgt750leme  34661  faclimlem1  35755  itgmulc2nc  37707  areacirclem1  37727  3factsumint2  42034  lcmineqlem10  42050  lcmineqlem11  42051  posbezout  42112  readvrec2  42373  pellexlem6  42846  pell1234qrmulcl  42867  rmxyadd  42933  jm2.18  43000  jm2.19lem1  43001  jm2.22  43007  jm2.20nn  43009  proot1ex  43208  sqrtcval  43653  ofmul12  44337  binomcxplemnotnn0  44368  sineq0ALT  44948  mul13d  45300  stoweidlem11  46028  wallispi2lem1  46088  stirlinglem1  46091  stirlinglem3  46093  stirlinglem7  46097  stirlinglem15  46105  dirkertrigeqlem3  46117  dirkercncflem2  46121  fourierdlem66  46189  fourierdlem83  46206  etransclem23  46274  mod42tp1mod8  47612  fppr2odd  47741  2zlidl  48250  itcovalt2lem2lem2  48685  itsclc0yqsollem1  48773  itscnhlc0xyqsol  48776  itscnhlinecirc02plem1  48793