Theorem mul12d 11491

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11170   · cmul 11177

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-mulcom 11236  ax-mulass 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411

This theorem is used by:  divrec  11960  remullem  15263  sqreulem  15495  cvgrat  16020  binomrisefac  16176  tanval3  16270  sinadd  16300  dvdsmulgcd  16694  lcmgcdlem  16744  cncongr1  16805  prmdiv  16924  vdwlem6  17126  itgmulc2  26116  dvexp3  26260  aaliou3lem8  26636  dvradcnv  26712  pserdvlem2  26719  abelthlem6  26727  abelthlem7  26729  tangtx  26798  tanarg  26911  dvcxp1  27032  dvcncxp1  27035  heron  27130  dcubic1  27137  mcubic  27139  dquart  27145  quart1  27148  quartlem1  27149  asinsin  27184  lgamgulmlem2  27321  basellem3  27374  bcp1ctr  27570  gausslemma2dlem6  27663  lgseisenlem2  27667  lgseisenlem4  27669  lgsquadlem1  27671  2sqlem4  27712  chebbnd1lem3  27762  rpvmasum2  27803  mulog2sumlem3  27827  selberglem1  27836  selberg4lem1  27851  selberg3r  27860  selberg34r  27862  pntrlog2bndlem4  27871  pntrlog2bndlem6  27874  pntlemr  27893  pntlemk  27897  ostth2lem3  27926  colinearalglem4  29421  branmfn  32641  constrrtlc1  34298  constrrtcclem  34300  constrmulcl  34337  cos9thpiminplylem2  34349  vtsprod  35203  hgt750leme  35222  faclimlem1  36429  itgmulc2nc  38526  areacirclem1  38546  3factsumint2  42992  lcmineqlem10  43008  lcmineqlem11  43009  posbezout  43070  readvrec2  43340  pellexlem6  43779  pell1234qrmulcl  43800  rmxyadd  43866  jm2.18  43933  jm2.19lem1  43934  jm2.22  43940  jm2.20nn  43942  proot1ex  44141  sqrtcval  44585  ofmul12  45253  binomcxplemnotnn0  45284  sineq0ALT  45863  mul13d  46217  stoweidlem11  46943  wallispi2lem1  47003  stirlinglem1  47006  stirlinglem3  47008  stirlinglem7  47012  stirlinglem15  47020  dirkertrigeqlem3  47032  dirkercncflem2  47036  fourierdlem66  47104  fourierdlem83  47121  etransclem23  47189  cos3t  47840  sin5tlem3  47843  mod42tp1mod8  48609  nprmdvdsfacm1lem1  48627  fppr2odd  48751  2zlidl  49259  itcovalt2lem2lem2  49708  itsclc0yqsollem1  49796  itscnhlc0xyqsol  49799  itscnhlinecirc02plem1  49816