Theorem mul12d 11382

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  (class class class)co 7385  ℂcc 11061   · cmul 11068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-mulcom 11127  ax-mulass 11129

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388

This theorem is referenced by:  divrec  11851  remullem  15131  sqreulem  15363  cvgrat  15889  binomrisefac  16048  tanval3  16142  sinadd  16172  dvdsmulgcd  16566  lcmgcdlem  16616  cncongr1  16677  prmdiv  16796  vdwlem6  16998  itgmulc2  25869  dvexp3  26013  aaliou3lem8  26379  dvradcnv  26454  pserdvlem2  26461  abelthlem6  26469  abelthlem7  26471  tangtx  26540  tanarg  26654  dvcxp1  26775  dvcncxp1  26778  heron  26873  dcubic1  26880  mcubic  26882  dquart  26888  quart1  26891  quartlem1  26892  asinsin  26927  lgamgulmlem2  27064  basellem3  27117  bcp1ctr  27313  gausslemma2dlem6  27406  lgseisenlem2  27410  lgseisenlem4  27412  lgsquadlem1  27414  2sqlem4  27455  chebbnd1lem3  27505  rpvmasum2  27546  mulog2sumlem3  27570  selberglem1  27579  selberg4lem1  27594  selberg3r  27603  selberg34r  27605  pntrlog2bndlem4  27614  pntrlog2bndlem6  27617  pntlemr  27636  pntlemk  27640  ostth2lem3  27669  colinearalglem4  29049  branmfn  32247  constrrtlc1  33983  constrrtcclem  33985  constrmulcl  34022  cos9thpiminplylem2  34034  vtsprod  34890  hgt750leme  34909  faclimlem1  36041  itgmulc2nc  38135  areacirclem1  38155  3factsumint2  42587  lcmineqlem10  42603  lcmineqlem11  42604  posbezout  42665  readvrec2  42918  pellexlem6  43359  pell1234qrmulcl  43380  rmxyadd  43446  jm2.18  43513  jm2.19lem1  43514  jm2.22  43520  jm2.20nn  43522  proot1ex  43721  sqrtcval  44165  ofmul12  44849  binomcxplemnotnn0  44880  sineq0ALT  45460  mul13d  45807  stoweidlem11  46533  wallispi2lem1  46593  stirlinglem1  46596  stirlinglem3  46598  stirlinglem7  46602  stirlinglem15  46610  dirkertrigeqlem3  46622  dirkercncflem2  46626  fourierdlem66  46694  fourierdlem83  46711  etransclem23  46779  cos3t  47414  sin5tlem3  47417  mod42tp1mod8  48159  nprmdvdsfacm1lem1  48177  fppr2odd  48301  2zlidl  48810  itcovalt2lem2lem2  49244  itsclc0yqsollem1  49332  itscnhlc0xyqsol  49335  itscnhlinecirc02plem1  49352