Theorem mul12d 11470

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-mulcom 11219  ax-mulass 11221

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  divrec  11938  remullem  15167  sqreulem  15398  cvgrat  15919  binomrisefac  16078  tanval3  16170  sinadd  16200  dvdsmulgcd  16593  lcmgcdlem  16643  cncongr1  16704  prmdiv  16822  vdwlem6  17024  itgmulc2  25869  dvexp3  26016  aaliou3lem8  26387  dvradcnv  26464  pserdvlem2  26472  abelthlem6  26480  abelthlem7  26482  tangtx  26547  tanarg  26661  dvcxp1  26782  dvcncxp1  26785  heron  26881  dcubic1  26888  mcubic  26890  dquart  26896  quart1  26899  quartlem1  26900  asinsin  26935  lgamgulmlem2  27073  basellem3  27126  bcp1ctr  27323  gausslemma2dlem6  27416  lgseisenlem2  27420  lgseisenlem4  27422  lgsquadlem1  27424  2sqlem4  27465  chebbnd1lem3  27515  rpvmasum2  27556  mulog2sumlem3  27580  selberglem1  27589  selberg4lem1  27604  selberg3r  27613  selberg34r  27615  pntrlog2bndlem4  27624  pntrlog2bndlem6  27627  pntlemr  27646  pntlemk  27650  ostth2lem3  27679  colinearalglem4  28924  branmfn  32124  constrrtlc1  33773  constrrtcclem  33775  vtsprod  34654  hgt750leme  34673  faclimlem1  35743  itgmulc2nc  37695  areacirclem1  37715  3factsumint2  42023  lcmineqlem10  42039  lcmineqlem11  42040  posbezout  42101  readvrec2  42391  pellexlem6  42845  pell1234qrmulcl  42866  rmxyadd  42933  jm2.18  43000  jm2.19lem1  43001  jm2.22  43007  jm2.20nn  43009  proot1ex  43208  sqrtcval  43654  ofmul12  44344  binomcxplemnotnn0  44375  sineq0ALT  44957  mul13d  45291  stoweidlem11  46026  wallispi2lem1  46086  stirlinglem1  46089  stirlinglem3  46091  stirlinglem7  46095  stirlinglem15  46103  dirkertrigeqlem3  46115  dirkercncflem2  46119  fourierdlem66  46187  fourierdlem83  46204  etransclem23  46272  mod42tp1mod8  47589  fppr2odd  47718  2zlidl  48156  itcovalt2lem2lem2  48595  itsclc0yqsollem1  48683  itscnhlc0xyqsol  48686  itscnhlinecirc02plem1  48703