Theorem mul4d 11345

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 11301	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
6	1, 2, 3, 4, 5	syl22anc 838	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  remullem  15051  absmul  15217  binomrisefac  15965  cosadd  16090  tanadd  16092  eulerthlem2  16709  mul4sqlem  16881  odadd2  19778  itgmulc2  25791  plymullem1  26175  chordthmlem4  26801  heron  26804  quartlem1  26823  dchrmulcl  27216  bposlem9  27259  lgsdir  27299  lgsdi  27301  lgsquad2lem1  27351  chtppilimlem1  27440  rplogsumlem1  27451  dchrvmasumlem1  27462  dchrvmasum2lem  27463  chpdifbndlem1  27520  pntlemf  27572  brbtwn2  28978  colinearalglem4  28982  binom2subadd  32821  zringfrac  33635  constrmulcl  33928  madjusmdetlem4  33987  hgt750lemf  34810  hgt750leme  34815  circum  35868  itgmulc2nc  37885  flt4lem5e  42895  pellexlem6  43072  pell1234qrmulcl  43093  rmxyadd  43159  wallispi2lem2  46312  dirkertrigeqlem3  46340  cevathlem1  47107  itsclc0xyqsolr  49011