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

Metamath Proof Explorer

Theorem adddirp1d

Description: Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses adddirp1d.a ⊢ φ → A ∈ ℂ
adddirp1d.b ⊢ φ → B ∈ ℂ
Assertion adddirp1d ⊢ φ → A + 1 ⁢ B = A ⁢ B + B

Proof

Step Hyp Ref Expression
1 adddirp1d.a ⊢ φ → A ∈ ℂ
2 adddirp1d.b ⊢ φ → B ∈ ℂ
3 1cnd ⊢ φ → 1 ∈ ℂ
4 1 3 2 adddird ⊢ φ → A + 1 ⁢ B = A ⁢ B + 1 ⁢ B
5 2 mullidd ⊢ φ → 1 ⁢ B = B
6 5 oveq2d ⊢ φ → A ⁢ B + 1 ⁢ B = A ⁢ B + B
7 4 6 eqtrd ⊢ φ → A + 1 ⁢ B = A ⁢ B + B