Theorem mul12d 11383

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-mulcom 11132  ax-mulass 11134

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  divrec  11853  remullem  15094  sqreulem  15326  cvgrat  15849  binomrisefac  16008  tanval3  16102  sinadd  16132  dvdsmulgcd  16526  lcmgcdlem  16576  cncongr1  16637  prmdiv  16755  vdwlem6  16957  itgmulc2  25735  dvexp3  25882  aaliou3lem8  26253  dvradcnv  26330  pserdvlem2  26338  abelthlem6  26346  abelthlem7  26348  tangtx  26414  tanarg  26528  dvcxp1  26649  dvcncxp1  26652  heron  26748  dcubic1  26755  mcubic  26757  dquart  26763  quart1  26766  quartlem1  26767  asinsin  26802  lgamgulmlem2  26940  basellem3  26993  bcp1ctr  27190  gausslemma2dlem6  27283  lgseisenlem2  27287  lgseisenlem4  27289  lgsquadlem1  27291  2sqlem4  27332  chebbnd1lem3  27382  rpvmasum2  27423  mulog2sumlem3  27447  selberglem1  27456  selberg4lem1  27471  selberg3r  27480  selberg34r  27482  pntrlog2bndlem4  27491  pntrlog2bndlem6  27494  pntlemr  27513  pntlemk  27517  ostth2lem3  27546  colinearalglem4  28836  branmfn  32034  constrrtlc1  33722  constrrtcclem  33724  constrmulcl  33761  cos9thpiminplylem2  33773  vtsprod  34630  hgt750leme  34649  faclimlem1  35730  itgmulc2nc  37682  areacirclem1  37702  3factsumint2  42010  lcmineqlem10  42026  lcmineqlem11  42027  posbezout  42088  readvrec2  42349  pellexlem6  42822  pell1234qrmulcl  42843  rmxyadd  42910  jm2.18  42977  jm2.19lem1  42978  jm2.22  42984  jm2.20nn  42986  proot1ex  43185  sqrtcval  43630  ofmul12  44314  binomcxplemnotnn0  44345  sineq0ALT  44926  mul13d  45278  stoweidlem11  46009  wallispi2lem1  46069  stirlinglem1  46072  stirlinglem3  46074  stirlinglem7  46078  stirlinglem15  46086  dirkertrigeqlem3  46098  dirkercncflem2  46102  fourierdlem66  46170  fourierdlem83  46187  etransclem23  46255  mod42tp1mod8  47603  fppr2odd  47732  2zlidl  48228  itcovalt2lem2lem2  48663  itsclc0yqsollem1  48751  itscnhlc0xyqsol  48754  itscnhlinecirc02plem1  48771