Theorem joinlmuladdmuld 11157

Description: Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)

Hypotheses

Ref	Expression
joinlmuladdmuld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
joinlmuladdmuld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
joinlmuladdmuld.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
joinlmuladdmuld.4	⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)

Assertion

Ref	Expression
joinlmuladdmuld	⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)

Proof of Theorem joinlmuladdmuld

Step	Hyp	Ref	Expression
1		joinlmuladdmuld.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		joinlmuladdmuld.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
3		joinlmuladdmuld.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4	1, 2, 3	adddird 11155	. 2 ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = ((𝐴 · 𝐵) + (𝐶 · 𝐵)))
5		joinlmuladdmuld.4	. 2 ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)
6	4, 5	eqtrd 2769	1 ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   + caddc 11027   · cmul 11029

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 2706  ax-addcl 11084  ax-mulcom 11088  ax-distr 11091

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  1p1times  11302  div4p1lem1div2  12394  ltdifltdiv  13752  discr1  14160  arisum  15781  bezoutlem3  16466  bezoutlem4  16467  mbfi1fseqlem4  25673  itgmulc2  25789  tangtx  26468  binom4  26814  axcontlem8  28993  zringfrac  33584  constrrtcclem  33840  cos9thpiminplylem2  33889  int-rightdistd  44363  fmtnorec2lem  47730  joinlmuladdmuli  49960