Theorem mul4d 11471

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   · cmul 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-mulcl 11215  ax-mulcom 11217  ax-mulass 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  remullem  15164  absmul  15330  binomrisefac  16075  cosadd  16198  tanadd  16200  eulerthlem2  16816  mul4sqlem  16987  odadd2  19882  itgmulc2  25884  plymullem1  26268  chordthmlem4  26893  heron  26896  quartlem1  26915  dchrmulcl  27308  bposlem9  27351  lgsdir  27391  lgsdi  27393  lgsquad2lem1  27443  chtppilimlem1  27532  rplogsumlem1  27543  dchrvmasumlem1  27554  dchrvmasum2lem  27555  chpdifbndlem1  27612  pntlemf  27664  brbtwn2  28935  colinearalglem4  28939  zringfrac  33562  madjusmdetlem4  33791  hgt750lemf  34647  hgt750leme  34652  circum  35659  itgmulc2nc  37675  flt4lem5e  42643  pellexlem6  42822  pell1234qrmulcl  42843  rmxyadd  42910  wallispi2lem2  46028  dirkertrigeqlem3  46056  cevathlem1  46823  itsclc0xyqsolr  48619