Theorem mul32d 10246

Description: Commutative/associative law that swaps the last 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
mul32d	|- ( ph -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )

Proof of Theorem mul32d

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		mul32 10203	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
5	1, 2, 3, 4	syl3anc 1326	1 |- ( ph -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )

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:  conjmul  10742  modmul1  12723  binom3  12985  bernneq  12990  expmulnbnd  12996  discr  13001  bcm1k  13102  bcp1n  13103  reccn2  14327  binomlem  14561  binomfallfaclem2  14771  tanadd  14897  eirrlem  14932  dvds2ln  15014  bezoutlem4  15259  divgcdcoprm0  15379  modprm0  15510  nrginvrcnlem  22495  tchcphlem2  23035  csbren  23182  radcnvlem1  24167  tanarg  24365  cxpeq  24498  quad2  24566  binom4  24577  dquartlem2  24579  dquart  24580  quart1lem  24582  dvatan  24662  log2cnv  24671  basellem8  24814  bcmono  25002  gausslemma2d  25099  lgsquadlem1  25105  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  rplogsumlem1  25173  dchrisumlem2  25179  chpdifbndlem1  25242  selberg3lem1  25246  selberg4  25250  selberg3r  25258  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntlemf  25294  pntlemo  25296  ostth2lem1  25307  ostth2lem3  25324  logdivsqrle  30728  circum  31568  jm2.25  37566  jm2.27c  37574  binomcxplemnotnn0  38555  dvasinbx  40135  stirlinglem3  40293  dirkercncflem2  40321  cevathlem1  41056