Theorem adddirp1d

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

	Ref	Expression
Hypotheses	adddirp1d.a	$$⊢\phi \to A\in ℂ$$
	adddirp1d.b	$$⊢\phi \to B\in ℂ$$
Assertion	adddirp1d	$$⊢\phi \to \left(A+1\right)B=AB+B$$

Proof

Step	Hyp	Ref	Expression
1		adddirp1d.a	$$⊢\phi \to A\in ℂ$$
2		adddirp1d.b	$$⊢\phi \to B\in ℂ$$
3		1cnd	$$⊢\phi \to 1\in ℂ$$
4	1 3 2	adddird	$$⊢\phi \to \left(A+1\right)B=AB+1B$$
5	2	mullidd	$$⊢\phi \to 1B=B$$
6	5	oveq2d	$$⊢\phi \to AB+1B=AB+B$$
7	4 6	eqtrd	$$⊢\phi \to \left(A+1\right)B=AB+B$$