Theorem mul4d 11430

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110   · cmul 11117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414

This theorem is referenced by:  remullem  15079  absmul  15245  binomrisefac  15990  cosadd  16112  tanadd  16114  eulerthlem2  16719  mul4sqlem  16890  odadd2  19758  itgmulc2  25575  plymullem1  25952  chordthmlem4  26564  heron  26567  quartlem1  26586  dchrmulcl  26976  bposlem9  27019  lgsdir  27059  lgsdi  27061  lgsquad2lem1  27111  chtppilimlem1  27200  rplogsumlem1  27211  dchrvmasumlem1  27222  dchrvmasum2lem  27223  chpdifbndlem1  27280  pntlemf  27332  brbtwn2  28418  colinearalglem4  28422  madjusmdetlem4  33096  hgt750lemf  33951  hgt750leme  33956  circum  34945  itgmulc2nc  36859  flt4lem5e  41700  pellexlem6  41874  pell1234qrmulcl  41895  rmxyadd  41962  wallispi2lem2  45087  dirkertrigeqlem3  45115  cevathlem1  45882  itsclc0xyqsolr  47543