Axiom ax-distr 9580

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9556. Proofs should normally use adddi 9602 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
ax-distr

Detailed syntax breakdown of Axiom ax-distr

Step	Hyp	Ref	Expression
1		cA	. . . 4
2		cc 9511	. . . 4
3	1, 2	wcel 1818	. . 3
4		cB	. . . 4
5	4, 2	wcel 1818	. . 3
6		cC	. . . 4
7	6, 2	wcel 1818	. . 3
8	3, 5, 7	w3a 973	. 2
9		caddc 9516	. . . . 5
10	4, 6, 9	co 6296	. . . 4
11		cmul 9518	. . . 4
12	1, 10, 11	co 6296	. . 3
13	1, 4, 11	co 6296	. . . 4
14	1, 6, 11	co 6296	. . . 4
15	13, 14, 9	co 6296	. . 3
16	12, 15	wceq 1395	. 2
17	8, 16	wi 4	1

This axiom is referenced by:  adddi  9602