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

Theorem mul12d 10458
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 10415 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1477 1 (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2140  (class class class)co 6815  cc 10147   · cmul 10154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-mulcom 10213  ax-mulass 10215
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818
This theorem is referenced by:  divrec  10914  remullem  14088  sqreulem  14319  cvgrat  14835  binomrisefac  14993  tanval3  15084  sinadd  15114  dvdsmulgcd  15497  lcmgcdlem  15542  cncongr1  15604  prmdiv  15713  vdwlem6  15913  itgmulc2  23820  dvexp3  23961  aaliou3lem8  24320  dvradcnv  24395  pserdvlem2  24402  abelthlem6  24410  abelthlem7  24412  tangtx  24478  tanarg  24586  dvcxp1  24702  dvcncxp1  24705  heron  24786  dcubic1  24793  mcubic  24795  dquart  24801  quart1  24804  quartlem1  24805  asinsin  24840  lgamgulmlem2  24977  basellem3  25030  bcp1ctr  25225  gausslemma2dlem6  25318  lgseisenlem2  25322  lgseisenlem4  25324  lgsquadlem1  25326  2sqlem4  25367  chebbnd1lem3  25381  rpvmasum2  25422  mulog2sumlem3  25446  selberglem1  25455  selberg4lem1  25470  selberg3r  25479  selberg34r  25481  pntrlog2bndlem4  25490  pntrlog2bndlem6  25493  pntlemr  25512  pntlemk  25516  ostth2lem3  25545  colinearalglem4  26010  branmfn  29295  vtsprod  31048  hgt750leme  31067  faclimlem1  31958  itgmulc2nc  33810  areacirclem1  33832  pellexlem6  37919  pell1234qrmulcl  37940  rmxyadd  38007  jm2.18  38076  jm2.19lem1  38077  jm2.22  38083  jm2.20nn  38085  proot1ex  38300  ofmul12  39045  binomcxplemnotnn0  39076  sineq0ALT  39691  mul13d  40009  stoweidlem11  40750  wallispi2lem1  40810  stirlinglem1  40813  stirlinglem3  40815  stirlinglem7  40819  stirlinglem15  40827  dirkertrigeqlem3  40839  dirkercncflem2  40843  fourierdlem66  40911  fourierdlem83  40928  etransclem23  40996  mod42tp1mod8  42048  2zlidl  42463
  Copyright terms: Public domain W3C validator