Theorem addmuldir1d

Description: Distributive law with summands being products. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Hypotheses	addmuldir1d.a	$$⊢\phi \to A\in ℂ$$
	addmuldir1d.b	$$⊢\phi \to B\in ℂ$$
	addmuldir1d.c	$$⊢\phi \to C\in ℂ$$
	addmuldir1d.d	$$⊢\phi \to D\in ℂ$$
	addmuldir1d.e	$$⊢\phi \to E\in ℂ$$
	addmuldir1d.f	$$⊢\phi \to F\in ℂ$$
Assertion	addmuldir1d	$$⊢\phi \to \left(A+BC\right)\left(D+EF\right)=AD+AEF+DBC+BCEF$$

Proof

Step	Hyp	Ref	Expression
1		addmuldir1d.a	$$⊢\phi \to A\in ℂ$$
2		addmuldir1d.b	$$⊢\phi \to B\in ℂ$$
3		addmuldir1d.c	$$⊢\phi \to C\in ℂ$$
4		addmuldir1d.d	$$⊢\phi \to D\in ℂ$$
5		addmuldir1d.e	$$⊢\phi \to E\in ℂ$$
6		addmuldir1d.f	$$⊢\phi \to F\in ℂ$$
7	2 3	mulcld	$$⊢\phi \to BC\in ℂ$$
8	5 6	mulcld	$$⊢\phi \to EF\in ℂ$$
9	1 7 4 8	muladdd	$$⊢\phi \to \left(A+BC\right)\left(D+EF\right)=AD+EFBC+AEF+DBC$$
10	1 4	mulcld	$$⊢\phi \to AD\in ℂ$$
11	8 7	mulcld	$$⊢\phi \to EFBC\in ℂ$$
12	1 8	mulcld	$$⊢\phi \to AEF\in ℂ$$
13	4 7	mulcld	$$⊢\phi \to DBC\in ℂ$$
14	10 11 12 13	add42d	$$⊢\phi \to AD+EFBC+AEF+DBC=AD+AEF+DBC+EFBC$$
15	8 7	mulcomd	$$⊢\phi \to EFBC=BCEF$$
16	15	oveq2d	$$⊢\phi \to DBC+EFBC=DBC+BCEF$$
17	16	oveq2d	$$⊢\phi \to AD+AEF+DBC+EFBC=AD+AEF+DBC+BCEF$$
18	9 14 17	3eqtrd	$$⊢\phi \to \left(A+BC\right)\left(D+EF\right)=AD+AEF+DBC+BCEF$$