MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul12d Structured version   Visualization version   GIF version

Theorem mul12d 10841
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
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcand.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mul12 10797 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1365 1 (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2106  (class class class)co 7151  cc 10527   · cmul 10534
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 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-mulcom 10593  ax-mulass 10595
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154
This theorem is referenced by:  divrec  11306  remullem  14480  sqreulem  14712  cvgrat  15231  binomrisefac  15388  tanval3  15479  sinadd  15509  dvdsmulgcd  15897  lcmgcdlem  15942  cncongr1  16003  prmdiv  16114  vdwlem6  16314  itgmulc2  24349  dvexp3  24490  aaliou3lem8  24849  dvradcnv  24924  pserdvlem2  24931  abelthlem6  24939  abelthlem7  24941  tangtx  25006  tanarg  25115  dvcxp1  25234  dvcncxp1  25237  heron  25329  dcubic1  25336  mcubic  25338  dquart  25344  quart1  25347  quartlem1  25348  asinsin  25383  lgamgulmlem2  25521  basellem3  25574  bcp1ctr  25769  gausslemma2dlem6  25862  lgseisenlem2  25866  lgseisenlem4  25868  lgsquadlem1  25870  2sqlem4  25911  chebbnd1lem3  25961  rpvmasum2  26002  mulog2sumlem3  26026  selberglem1  26035  selberg4lem1  26050  selberg3r  26059  selberg34r  26061  pntrlog2bndlem4  26070  pntrlog2bndlem6  26073  pntlemr  26092  pntlemk  26096  ostth2lem3  26125  colinearalglem4  26610  branmfn  29797  vtsprod  31797  hgt750leme  31816  faclimlem1  32860  itgmulc2nc  34828  areacirclem1  34850  pellexlem6  39293  pell1234qrmulcl  39314  rmxyadd  39380  jm2.18  39447  jm2.19lem1  39448  jm2.22  39454  jm2.20nn  39456  proot1ex  39663  ofmul12  40519  binomcxplemnotnn0  40550  sineq0ALT  41133  mul13d  41407  stoweidlem11  42159  wallispi2lem1  42219  stirlinglem1  42222  stirlinglem3  42224  stirlinglem7  42228  stirlinglem15  42236  dirkertrigeqlem3  42248  dirkercncflem2  42252  fourierdlem66  42320  fourierdlem83  42337  etransclem23  42405  mod42tp1mod8  43596  fppr2odd  43725  2zlidl  44034  itsclc0yqsollem1  44578  itscnhlc0xyqsol  44581  itscnhlinecirc02plem1  44598
  Copyright terms: Public domain W3C validator