Theorem mul12d 11193

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-mulcom 10944  ax-mulass 10946

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  divrec  11658  remullem  14848  sqreulem  15080  cvgrat  15604  binomrisefac  15761  tanval3  15852  sinadd  15882  dvdsmulgcd  16274  lcmgcdlem  16320  cncongr1  16381  prmdiv  16495  vdwlem6  16696  itgmulc2  25007  dvexp3  25151  aaliou3lem8  25514  dvradcnv  25589  pserdvlem2  25596  abelthlem6  25604  abelthlem7  25606  tangtx  25671  tanarg  25783  dvcxp1  25902  dvcncxp1  25905  heron  25997  dcubic1  26004  mcubic  26006  dquart  26012  quart1  26015  quartlem1  26016  asinsin  26051  lgamgulmlem2  26188  basellem3  26241  bcp1ctr  26436  gausslemma2dlem6  26529  lgseisenlem2  26533  lgseisenlem4  26535  lgsquadlem1  26537  2sqlem4  26578  chebbnd1lem3  26628  rpvmasum2  26669  mulog2sumlem3  26693  selberglem1  26702  selberg4lem1  26717  selberg3r  26726  selberg34r  26728  pntrlog2bndlem4  26737  pntrlog2bndlem6  26740  pntlemr  26759  pntlemk  26763  ostth2lem3  26792  colinearalglem4  27286  branmfn  30476  vtsprod  32628  hgt750leme  32647  faclimlem1  33718  itgmulc2nc  35854  areacirclem1  35874  3factsumint2  40037  lcmineqlem10  40053  lcmineqlem11  40054  pellexlem6  40663  pell1234qrmulcl  40684  rmxyadd  40750  jm2.18  40817  jm2.19lem1  40818  jm2.22  40824  jm2.20nn  40826  proot1ex  41033  sqrtcval  41256  ofmul12  41950  binomcxplemnotnn0  41981  sineq0ALT  42564  mul13d  42825  stoweidlem11  43559  wallispi2lem1  43619  stirlinglem1  43622  stirlinglem3  43624  stirlinglem7  43628  stirlinglem15  43636  dirkertrigeqlem3  43648  dirkercncflem2  43652  fourierdlem66  43720  fourierdlem83  43737  etransclem23  43805  mod42tp1mod8  45065  fppr2odd  45194  2zlidl  45503  itcovalt2lem2lem2  46031  itsclc0yqsollem1  46119  itscnhlc0xyqsol  46122  itscnhlinecirc02plem1  46139