Theorem mul12d 11459

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7424  ℂcc 11142   · cmul 11149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-mulcom 11208  ax-mulass 11210

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-iota 6503  df-fv 6559  df-ov 7427

This theorem is referenced by:  divrec  11924  remullem  15113  sqreulem  15344  cvgrat  15867  binomrisefac  16024  tanval3  16116  sinadd  16146  dvdsmulgcd  16536  lcmgcdlem  16582  cncongr1  16643  prmdiv  16759  vdwlem6  16960  itgmulc2  25781  dvexp3  25928  aaliou3lem8  26298  dvradcnv  26375  pserdvlem2  26383  abelthlem6  26391  abelthlem7  26393  tangtx  26458  tanarg  26571  dvcxp1  26692  dvcncxp1  26695  heron  26788  dcubic1  26795  mcubic  26797  dquart  26803  quart1  26806  quartlem1  26807  asinsin  26842  lgamgulmlem2  26980  basellem3  27033  bcp1ctr  27230  gausslemma2dlem6  27323  lgseisenlem2  27327  lgseisenlem4  27329  lgsquadlem1  27331  2sqlem4  27372  chebbnd1lem3  27422  rpvmasum2  27463  mulog2sumlem3  27487  selberglem1  27496  selberg4lem1  27511  selberg3r  27520  selberg34r  27522  pntrlog2bndlem4  27531  pntrlog2bndlem6  27534  pntlemr  27553  pntlemk  27557  ostth2lem3  27586  colinearalglem4  28738  branmfn  31933  vtsprod  34276  hgt750leme  34295  faclimlem1  35342  itgmulc2nc  37166  areacirclem1  37186  3factsumint2  41497  lcmineqlem10  41513  lcmineqlem11  41514  posbezout  41575  pellexlem6  42257  pell1234qrmulcl  42278  rmxyadd  42345  jm2.18  42412  jm2.19lem1  42413  jm2.22  42419  jm2.20nn  42421  proot1ex  42627  sqrtcval  43074  ofmul12  43765  binomcxplemnotnn0  43796  sineq0ALT  44379  mul13d  44663  stoweidlem11  45401  wallispi2lem1  45461  stirlinglem1  45464  stirlinglem3  45466  stirlinglem7  45470  stirlinglem15  45478  dirkertrigeqlem3  45490  dirkercncflem2  45494  fourierdlem66  45562  fourierdlem83  45579  etransclem23  45647  mod42tp1mod8  46944  fppr2odd  47073  2zlidl  47353  itcovalt2lem2lem2  47798  itsclc0yqsollem1  47886  itscnhlc0xyqsol  47889  itscnhlinecirc02plem1  47906