Theorem mul12d 11420

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   · cmul 11112

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 2704  ax-mulcom 11171  ax-mulass 11173

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  divrec  11885  remullem  15072  sqreulem  15303  cvgrat  15826  binomrisefac  15983  tanval3  16074  sinadd  16104  dvdsmulgcd  16494  lcmgcdlem  16540  cncongr1  16601  prmdiv  16715  vdwlem6  16916  itgmulc2  25343  dvexp3  25487  aaliou3lem8  25850  dvradcnv  25925  pserdvlem2  25932  abelthlem6  25940  abelthlem7  25942  tangtx  26007  tanarg  26119  dvcxp1  26238  dvcncxp1  26241  heron  26333  dcubic1  26340  mcubic  26342  dquart  26348  quart1  26351  quartlem1  26352  asinsin  26387  lgamgulmlem2  26524  basellem3  26577  bcp1ctr  26772  gausslemma2dlem6  26865  lgseisenlem2  26869  lgseisenlem4  26871  lgsquadlem1  26873  2sqlem4  26914  chebbnd1lem3  26964  rpvmasum2  27005  mulog2sumlem3  27029  selberglem1  27038  selberg4lem1  27053  selberg3r  27062  selberg34r  27064  pntrlog2bndlem4  27073  pntrlog2bndlem6  27076  pntlemr  27095  pntlemk  27099  ostth2lem3  27128  colinearalglem4  28157  branmfn  31346  vtsprod  33640  hgt750leme  33659  faclimlem1  34702  itgmulc2nc  36545  areacirclem1  36565  3factsumint2  40876  lcmineqlem10  40892  lcmineqlem11  40893  pellexlem6  41558  pell1234qrmulcl  41579  rmxyadd  41646  jm2.18  41713  jm2.19lem1  41714  jm2.22  41720  jm2.20nn  41722  proot1ex  41929  sqrtcval  42378  ofmul12  43070  binomcxplemnotnn0  43101  sineq0ALT  43684  mul13d  43976  stoweidlem11  44714  wallispi2lem1  44774  stirlinglem1  44777  stirlinglem3  44779  stirlinglem7  44783  stirlinglem15  44791  dirkertrigeqlem3  44803  dirkercncflem2  44807  fourierdlem66  44875  fourierdlem83  44892  etransclem23  44960  mod42tp1mod8  46257  fppr2odd  46386  2zlidl  46786  itcovalt2lem2lem2  47314  itsclc0yqsollem1  47402  itscnhlc0xyqsol  47405  itscnhlinecirc02plem1  47422