Theorem adddirp1d

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

	Ref	Expression
Hypotheses	adddirp1d.a	|- ( ph -> A e. CC )
	adddirp1d.b	|- ( ph -> B e. CC )
Assertion	adddirp1d	|- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) )

Proof

Step	Hyp	Ref	Expression
1		adddirp1d.a	|- ( ph -> A e. CC )
2		adddirp1d.b	|- ( ph -> B e. CC )
3		1cnd	|- ( ph -> 1 e. CC )
4	1 3 2	adddird	|- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + ( 1 x. B ) ) )
5	2	mullidd	|- ( ph -> ( 1 x. B ) = B )
6	5	oveq2d	|- ( ph -> ( ( A x. B ) + ( 1 x. B ) ) = ( ( A x. B ) + B ) )
7	4 6	eqtrd	|- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) )