Theorem mul12d 10852

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  (class class class)co 7159  ℂcc 10538   · cmul 10545

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-mulcom 10604  ax-mulass 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162

This theorem is referenced by:  divrec  11317  remullem  14490  sqreulem  14722  cvgrat  15242  binomrisefac  15399  tanval3  15490  sinadd  15520  dvdsmulgcd  15908  lcmgcdlem  15953  cncongr1  16014  prmdiv  16125  vdwlem6  16325  itgmulc2  24437  dvexp3  24578  aaliou3lem8  24937  dvradcnv  25012  pserdvlem2  25019  abelthlem6  25027  abelthlem7  25029  tangtx  25094  tanarg  25205  dvcxp1  25324  dvcncxp1  25327  heron  25419  dcubic1  25426  mcubic  25428  dquart  25434  quart1  25437  quartlem1  25438  asinsin  25473  lgamgulmlem2  25610  basellem3  25663  bcp1ctr  25858  gausslemma2dlem6  25951  lgseisenlem2  25955  lgseisenlem4  25957  lgsquadlem1  25959  2sqlem4  26000  chebbnd1lem3  26050  rpvmasum2  26091  mulog2sumlem3  26115  selberglem1  26124  selberg4lem1  26139  selberg3r  26148  selberg34r  26150  pntrlog2bndlem4  26159  pntrlog2bndlem6  26162  pntlemr  26181  pntlemk  26185  ostth2lem3  26214  colinearalglem4  26698  branmfn  29885  vtsprod  31914  hgt750leme  31933  faclimlem1  32979  itgmulc2nc  34964  areacirclem1  34986  pellexlem6  39437  pell1234qrmulcl  39458  rmxyadd  39524  jm2.18  39591  jm2.19lem1  39592  jm2.22  39598  jm2.20nn  39600  proot1ex  39807  ofmul12  40663  binomcxplemnotnn0  40694  sineq0ALT  41277  mul13d  41551  stoweidlem11  42303  wallispi2lem1  42363  stirlinglem1  42366  stirlinglem3  42368  stirlinglem7  42372  stirlinglem15  42380  dirkertrigeqlem3  42392  dirkercncflem2  42396  fourierdlem66  42464  fourierdlem83  42481  etransclem23  42549  mod42tp1mod8  43774  fppr2odd  43903  2zlidl  44212  itsclc0yqsollem1  44756  itscnhlc0xyqsol  44759  itscnhlinecirc02plem1  44776