Theorem mul4d 11464

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144   · cmul 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-mulcl 11208  ax-mulcom 11210  ax-mulass 11212

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429

This theorem is referenced by:  remullem  15115  absmul  15281  binomrisefac  16026  cosadd  16149  tanadd  16151  eulerthlem2  16758  mul4sqlem  16929  odadd2  19811  itgmulc2  25783  plymullem1  26168  chordthmlem4  26787  heron  26790  quartlem1  26809  dchrmulcl  27202  bposlem9  27245  lgsdir  27285  lgsdi  27287  lgsquad2lem1  27337  chtppilimlem1  27426  rplogsumlem1  27437  dchrvmasumlem1  27448  dchrvmasum2lem  27449  chpdifbndlem1  27506  pntlemf  27558  brbtwn2  28736  colinearalglem4  28740  zringfrac  33277  madjusmdetlem4  33464  hgt750lemf  34318  hgt750leme  34323  circum  35311  itgmulc2nc  37194  flt4lem5e  42111  pellexlem6  42285  pell1234qrmulcl  42306  rmxyadd  42373  wallispi2lem2  45489  dirkertrigeqlem3  45517  cevathlem1  46284  itsclc0xyqsolr  47920