Theorem mul12d 11344

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   · cmul 11032

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 11091  ax-mulass 11093

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  divrec  11814  remullem  15079  sqreulem  15311  cvgrat  15837  binomrisefac  15996  tanval3  16090  sinadd  16120  dvdsmulgcd  16514  lcmgcdlem  16564  cncongr1  16625  prmdiv  16744  vdwlem6  16946  itgmulc2  25810  dvexp3  25954  aaliou3lem8  26324  dvradcnv  26401  pserdvlem2  26409  abelthlem6  26417  abelthlem7  26419  tangtx  26485  tanarg  26599  dvcxp1  26720  dvcncxp1  26723  heron  26819  dcubic1  26826  mcubic  26828  dquart  26834  quart1  26837  quartlem1  26838  asinsin  26873  lgamgulmlem2  27011  basellem3  27064  bcp1ctr  27261  gausslemma2dlem6  27354  lgseisenlem2  27358  lgseisenlem4  27360  lgsquadlem1  27362  2sqlem4  27403  chebbnd1lem3  27453  rpvmasum2  27494  mulog2sumlem3  27518  selberglem1  27527  selberg4lem1  27542  selberg3r  27551  selberg34r  27553  pntrlog2bndlem4  27562  pntrlog2bndlem6  27565  pntlemr  27584  pntlemk  27588  ostth2lem3  27617  colinearalglem4  28997  branmfn  32196  constrrtlc1  33897  constrrtcclem  33899  constrmulcl  33936  cos9thpiminplylem2  33948  vtsprod  34804  hgt750leme  34823  faclimlem1  35946  itgmulc2nc  38020  areacirclem1  38040  3factsumint2  42472  lcmineqlem10  42488  lcmineqlem11  42489  posbezout  42550  readvrec2  42804  pellexlem6  43277  pell1234qrmulcl  43298  rmxyadd  43364  jm2.18  43431  jm2.19lem1  43432  jm2.22  43438  jm2.20nn  43440  proot1ex  43639  sqrtcval  44083  ofmul12  44767  binomcxplemnotnn0  44798  sineq0ALT  45378  mul13d  45728  stoweidlem11  46454  wallispi2lem1  46514  stirlinglem1  46517  stirlinglem3  46519  stirlinglem7  46523  stirlinglem15  46531  dirkertrigeqlem3  46543  dirkercncflem2  46547  fourierdlem66  46615  fourierdlem83  46632  etransclem23  46700  mod42tp1mod8  48062  nprmdvdsfacm1lem1  48080  fppr2odd  48204  2zlidl  48713  itcovalt2lem2lem2  49147  itsclc0yqsollem1  49235  itscnhlc0xyqsol  49238  itscnhlinecirc02plem1  49255