Theorem mul4d 11170

Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addcand.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
mul4d.4	⊢ (𝜑 → 𝐷 ∈ ℂ)

Assertion

Ref	Expression
mul4d	⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Proof of Theorem mul4d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcand.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mul4d.4	. 2 ⊢ (𝜑 → 𝐷 ∈ ℂ)
5		mul4 11126	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
6	1, 2, 3, 4, 5	syl22anc 835	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   · cmul 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-mulcl 10917  ax-mulcom 10919  ax-mulass 10921

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  remullem  14820  absmul  14987  binomrisefac  15733  cosadd  15855  tanadd  15857  eulerthlem2  16464  mul4sqlem  16635  odadd2  19431  itgmulc2  24979  plymullem1  25356  chordthmlem4  25966  heron  25969  quartlem1  25988  dchrmulcl  26378  bposlem9  26421  lgsdir  26461  lgsdi  26463  lgsquad2lem1  26513  chtppilimlem1  26602  rplogsumlem1  26613  dchrvmasumlem1  26624  dchrvmasum2lem  26625  chpdifbndlem1  26682  pntlemf  26734  brbtwn2  27254  colinearalglem4  27258  madjusmdetlem4  31759  hgt750lemf  32612  hgt750leme  32617  circum  33611  itgmulc2nc  35824  flt4lem5e  40473  pellexlem6  40636  pell1234qrmulcl  40657  rmxyadd  40723  wallispi2lem2  43567  dirkertrigeqlem3  43595  cevathlem1  44334  itsclc0xyqsolr  46067