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

Theorem mul12d 10837
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 10793 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1363 1 (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-mulcom 10589  ax-mulass 10591
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  divrec  11302  remullem  14475  sqreulem  14707  cvgrat  15227  binomrisefac  15384  tanval3  15475  sinadd  15505  dvdsmulgcd  15893  lcmgcdlem  15938  cncongr1  15999  prmdiv  16110  vdwlem6  16310  itgmulc2  24361  dvexp3  24502  aaliou3lem8  24861  dvradcnv  24936  pserdvlem2  24943  abelthlem6  24951  abelthlem7  24953  tangtx  25018  tanarg  25129  dvcxp1  25248  dvcncxp1  25251  heron  25343  dcubic1  25350  mcubic  25352  dquart  25358  quart1  25361  quartlem1  25362  asinsin  25397  lgamgulmlem2  25534  basellem3  25587  bcp1ctr  25782  gausslemma2dlem6  25875  lgseisenlem2  25879  lgseisenlem4  25881  lgsquadlem1  25883  2sqlem4  25924  chebbnd1lem3  25974  rpvmasum2  26015  mulog2sumlem3  26039  selberglem1  26048  selberg4lem1  26063  selberg3r  26072  selberg34r  26074  pntrlog2bndlem4  26083  pntrlog2bndlem6  26086  pntlemr  26105  pntlemk  26109  ostth2lem3  26138  colinearalglem4  26622  branmfn  29809  vtsprod  31809  hgt750leme  31828  faclimlem1  32872  itgmulc2nc  34841  areacirclem1  34863  pellexlem6  39309  pell1234qrmulcl  39330  rmxyadd  39396  jm2.18  39463  jm2.19lem1  39464  jm2.22  39470  jm2.20nn  39472  proot1ex  39679  ofmul12  40534  binomcxplemnotnn0  40565  sineq0ALT  41148  mul13d  41421  stoweidlem11  42173  wallispi2lem1  42233  stirlinglem1  42236  stirlinglem3  42238  stirlinglem7  42242  stirlinglem15  42250  dirkertrigeqlem3  42262  dirkercncflem2  42266  fourierdlem66  42334  fourierdlem83  42351  etransclem23  42419  mod42tp1mod8  43644  fppr2odd  43773  2zlidl  44133  itsclc0yqsollem1  44677  itscnhlc0xyqsol  44680  itscnhlinecirc02plem1  44697
  Copyright terms: Public domain W3C validator