Theorem mul12d 10245

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	|- ( ph -> A e. CC )
addcomd.2	|- ( ph -> B e. CC )
addcand.3	|- ( ph -> C e. CC )

Assertion

Ref	Expression
mul12d	|- ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )

Proof of Theorem mul12d

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addcomd.2	. 2 |- ( ph -> B e. CC )
3		addcand.3	. 2 |- ( ph -> C e. CC )
4		mul12 10202	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
5	1, 2, 3, 4	syl3anc 1326	1 |- ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-mulcom 10000  ax-mulass 10002

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  divrec  10701  remullem  13868  sqreulem  14099  cvgrat  14615  binomrisefac  14773  tanval3  14864  sinadd  14894  dvdsmulgcd  15274  lcmgcdlem  15319  cncongr1  15381  prmdiv  15490  vdwlem6  15690  itgmulc2  23600  dvexp3  23741  aaliou3lem8  24100  dvradcnv  24175  pserdvlem2  24182  abelthlem6  24190  abelthlem7  24192  tangtx  24257  tanarg  24365  dvcxp1  24481  dvcncxp1  24484  heron  24565  dcubic1  24572  mcubic  24574  dquart  24580  quart1  24583  quartlem1  24584  asinsin  24619  lgamgulmlem2  24756  basellem3  24809  bcp1ctr  25004  gausslemma2dlem6  25097  lgseisenlem2  25101  lgseisenlem4  25103  lgsquadlem1  25105  2sqlem4  25146  chebbnd1lem3  25160  rpvmasum2  25201  mulog2sumlem3  25225  selberglem1  25234  selberg4lem1  25249  selberg3r  25258  selberg34r  25260  pntrlog2bndlem4  25269  pntrlog2bndlem6  25272  pntlemr  25291  pntlemk  25295  ostth2lem3  25324  colinearalglem4  25789  branmfn  28964  vtsprod  30717  hgt750leme  30736  faclimlem1  31629  itgmulc2nc  33478  areacirclem1  33500  pellexlem6  37398  pell1234qrmulcl  37419  rmxyadd  37486  jm2.18  37555  jm2.19lem1  37556  jm2.22  37562  jm2.20nn  37564  proot1ex  37779  ofmul12  38524  binomcxplemnotnn0  38555  sineq0ALT  39173  mul13d  39491  stoweidlem11  40228  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem3  40293  stirlinglem7  40297  stirlinglem15  40305  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem66  40389  fourierdlem83  40406  etransclem23  40474  mod42tp1mod8  41519  2zlidl  41934