Theorem mul4d 11426

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-mulcl 11172  ax-mulcom 11174  ax-mulass 11176

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  remullem  15075  absmul  15241  binomrisefac  15986  cosadd  16108  tanadd  16110  eulerthlem2  16715  mul4sqlem  16886  odadd2  19717  itgmulc2  25351  plymullem1  25728  chordthmlem4  26340  heron  26343  quartlem1  26362  dchrmulcl  26752  bposlem9  26795  lgsdir  26835  lgsdi  26837  lgsquad2lem1  26887  chtppilimlem1  26976  rplogsumlem1  26987  dchrvmasumlem1  26998  dchrvmasum2lem  26999  chpdifbndlem1  27056  pntlemf  27108  brbtwn2  28163  colinearalglem4  28167  madjusmdetlem4  32810  hgt750lemf  33665  hgt750leme  33670  circum  34659  itgmulc2nc  36556  flt4lem5e  41398  pellexlem6  41572  pell1234qrmulcl  41593  rmxyadd  41660  wallispi2lem2  44788  dirkertrigeqlem3  44816  cevathlem1  45583  itsclc0xyqsolr  47455