Theorem nadddird

Description: Natural multiplication distributes over natural addition. Deduction form. (Contributed by Scott Fenton, 3-Aug-2026)

	Ref	Expression
Hypotheses	nadddid.1	$$⊢\phi \to A\in \mathrm{On}$$
	nadddid.2	$$⊢\phi \to B\in \mathrm{On}$$
	nadddid.3	$$⊢\phi \to C\in \mathrm{On}$$
Assertion	nadddird	Could not format assertion : No typesetting found for |- ( ph -> ( ( A +no B ) .no C ) = ( ( A .no C ) +no ( B .no C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadddid.1	$$⊢\phi \to A\in \mathrm{On}$$
2		nadddid.2	$$⊢\phi \to B\in \mathrm{On}$$
3		nadddid.3	$$⊢\phi \to C\in \mathrm{On}$$
4	3 1 2	nadddid	Could not format ( ph -> ( C .no ( A +no B ) ) = ( ( C .no A ) +no ( C .no B ) ) ) : No typesetting found for |- ( ph -> ( C .no ( A +no B ) ) = ( ( C .no A ) +no ( C .no B ) ) ) with typecode |-
5	1 2	naddcld	$$⊢\phi \to A+B\in \mathrm{On}$$
6	5 3	nmulcomd	Could not format ( ph -> ( ( A +no B ) .no C ) = ( C .no ( A +no B ) ) ) : No typesetting found for |- ( ph -> ( ( A +no B ) .no C ) = ( C .no ( A +no B ) ) ) with typecode |-
7	1 3	nmulcomd	Could not format ( ph -> ( A .no C ) = ( C .no A ) ) : No typesetting found for |- ( ph -> ( A .no C ) = ( C .no A ) ) with typecode |-
8	2 3	nmulcomd	Could not format ( ph -> ( B .no C ) = ( C .no B ) ) : No typesetting found for |- ( ph -> ( B .no C ) = ( C .no B ) ) with typecode |-
9	7 8	oveq12d	Could not format ( ph -> ( ( A .no C ) +no ( B .no C ) ) = ( ( C .no A ) +no ( C .no B ) ) ) : No typesetting found for |- ( ph -> ( ( A .no C ) +no ( B .no C ) ) = ( ( C .no A ) +no ( C .no B ) ) ) with typecode |-
10	4 6 9	3eqtr4d	Could not format ( ph -> ( ( A +no B ) .no C ) = ( ( A .no C ) +no ( B .no C ) ) ) : No typesetting found for |- ( ph -> ( ( A +no B ) .no C ) = ( ( A .no C ) +no ( B .no C ) ) ) with typecode |-