Theorem mul12d 11353

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-mulcom 11100  ax-mulass 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  divrec  11823  remullem  15088  sqreulem  15320  cvgrat  15846  binomrisefac  16005  tanval3  16099  sinadd  16129  dvdsmulgcd  16523  lcmgcdlem  16573  cncongr1  16634  prmdiv  16753  vdwlem6  16955  itgmulc2  25826  dvexp3  25970  aaliou3lem8  26336  dvradcnv  26411  pserdvlem2  26418  abelthlem6  26426  abelthlem7  26428  tangtx  26494  tanarg  26608  dvcxp1  26729  dvcncxp1  26732  heron  26827  dcubic1  26834  mcubic  26836  dquart  26842  quart1  26845  quartlem1  26846  asinsin  26881  lgamgulmlem2  27018  basellem3  27071  bcp1ctr  27267  gausslemma2dlem6  27360  lgseisenlem2  27364  lgseisenlem4  27366  lgsquadlem1  27368  2sqlem4  27409  chebbnd1lem3  27459  rpvmasum2  27500  mulog2sumlem3  27524  selberglem1  27533  selberg4lem1  27548  selberg3r  27557  selberg34r  27559  pntrlog2bndlem4  27568  pntrlog2bndlem6  27571  pntlemr  27590  pntlemk  27594  ostth2lem3  27623  colinearalglem4  29003  branmfn  32201  constrrtlc1  33923  constrrtcclem  33925  constrmulcl  33962  cos9thpiminplylem2  33974  vtsprod  34830  hgt750leme  34849  faclimlem1  35972  itgmulc2nc  38056  areacirclem1  38076  3factsumint2  42508  lcmineqlem10  42524  lcmineqlem11  42525  posbezout  42586  readvrec2  42839  pellexlem6  43280  pell1234qrmulcl  43301  rmxyadd  43367  jm2.18  43434  jm2.19lem1  43435  jm2.22  43441  jm2.20nn  43443  proot1ex  43642  sqrtcval  44086  ofmul12  44770  binomcxplemnotnn0  44801  sineq0ALT  45381  mul13d  45729  stoweidlem11  46455  wallispi2lem1  46515  stirlinglem1  46518  stirlinglem3  46520  stirlinglem7  46524  stirlinglem15  46532  dirkertrigeqlem3  46544  dirkercncflem2  46548  fourierdlem66  46616  fourierdlem83  46633  etransclem23  46701  cos3t  47336  sin5tlem3  47339  mod42tp1mod8  48081  nprmdvdsfacm1lem1  48099  fppr2odd  48223  2zlidl  48732  itcovalt2lem2lem2  49166  itsclc0yqsollem1  49254  itscnhlc0xyqsol  49257  itscnhlinecirc02plem1  49274