This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem joinlmuladdmuld

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

Ref Expression
Hypotheses joinlmuladdmuld.1 ⊢ φ → A ∈ ℂ
joinlmuladdmuld.2 ⊢ φ → B ∈ ℂ
joinlmuladdmuld.3 ⊢ φ → C ∈ ℂ
joinlmuladdmuld.4 ⊢ φ → A ⁢ B + C ⁢ B = D
Assertion joinlmuladdmuld ⊢ φ → A + C ⁢ B = D

Proof

Step Hyp Ref Expression
1 joinlmuladdmuld.1 ⊢ φ → A ∈ ℂ
2 joinlmuladdmuld.2 ⊢ φ → B ∈ ℂ
3 joinlmuladdmuld.3 ⊢ φ → C ∈ ℂ
4 joinlmuladdmuld.4 ⊢ φ → A ⁢ B + C ⁢ B = D
5 1 3 2 adddird ⊢ φ → A + C ⁢ B = A ⁢ B + C ⁢ B
6 5 4 eqtrd ⊢ φ → A + C ⁢ B = D