Theorem mul12d 11114

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-mulcom 10866  ax-mulass 10868

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  divrec  11579  remullem  14767  sqreulem  14999  cvgrat  15523  binomrisefac  15680  tanval3  15771  sinadd  15801  dvdsmulgcd  16193  lcmgcdlem  16239  cncongr1  16300  prmdiv  16414  vdwlem6  16615  itgmulc2  24903  dvexp3  25047  aaliou3lem8  25410  dvradcnv  25485  pserdvlem2  25492  abelthlem6  25500  abelthlem7  25502  tangtx  25567  tanarg  25679  dvcxp1  25798  dvcncxp1  25801  heron  25893  dcubic1  25900  mcubic  25902  dquart  25908  quart1  25911  quartlem1  25912  asinsin  25947  lgamgulmlem2  26084  basellem3  26137  bcp1ctr  26332  gausslemma2dlem6  26425  lgseisenlem2  26429  lgseisenlem4  26431  lgsquadlem1  26433  2sqlem4  26474  chebbnd1lem3  26524  rpvmasum2  26565  mulog2sumlem3  26589  selberglem1  26598  selberg4lem1  26613  selberg3r  26622  selberg34r  26624  pntrlog2bndlem4  26633  pntrlog2bndlem6  26636  pntlemr  26655  pntlemk  26659  ostth2lem3  26688  colinearalglem4  27180  branmfn  30368  vtsprod  32519  hgt750leme  32538  faclimlem1  33615  itgmulc2nc  35772  areacirclem1  35792  3factsumint2  39958  lcmineqlem10  39974  lcmineqlem11  39975  pellexlem6  40572  pell1234qrmulcl  40593  rmxyadd  40659  jm2.18  40726  jm2.19lem1  40727  jm2.22  40733  jm2.20nn  40735  proot1ex  40942  sqrtcval  41138  ofmul12  41832  binomcxplemnotnn0  41863  sineq0ALT  42446  mul13d  42707  stoweidlem11  43442  wallispi2lem1  43502  stirlinglem1  43505  stirlinglem3  43507  stirlinglem7  43511  stirlinglem15  43519  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem66  43603  fourierdlem83  43620  etransclem23  43688  mod42tp1mod8  44942  fppr2odd  45071  2zlidl  45380  itcovalt2lem2lem2  45908  itsclc0yqsollem1  45996  itscnhlc0xyqsol  45999  itscnhlinecirc02plem1  46016