Axiom ax-distr 9228

Description: Distributive law for complex numbers. Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9204. Proofs should normally use adddi 9250 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 9159	. . . 4
3	1, 2	wcel 1732	. . 3
4		cB	. . . 4
5	4, 2	wcel 1732	. . 3
6		cC	. . . 4
7	6, 2	wcel 1732	. . 3
8	3, 5, 7	w3a 939	. 2
9		caddc 9164	. . . . 5
10	4, 6, 9	co 6103	. . . 4
11		cmul 9166	. . . 4
12	1, 10, 11	co 6103	. . 3
13	1, 4, 11	co 6103	. . . 4
14	1, 6, 11	co 6103	. . . 4
15	13, 14, 9	co 6103	. . 3
16	12, 15	wceq 1670	. 2
17	8, 16	wi 4	1

This axiom is referenced by:  adddi  9250