MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-distr Unicode version

Axiom ax-distr 9108
Description: Distributive law for complex numbers. Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9084. Proofs should normally use adddi 9130 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
ax-distr

Detailed syntax breakdown of Axiom ax-distr
StepHypRef Expression
1 cA . . . 4
2 cc 9039 . . . 4
31, 2wcel 1728 . . 3
4 cB . . . 4
54, 2wcel 1728 . . 3
6 cC . . . 4
76, 2wcel 1728 . . 3
83, 5, 7w3a 937 . 2
9 caddc 9044 . . . . 5
104, 6, 9co 6129 . . . 4
11 cmul 9046 . . . 4
121, 10, 11co 6129 . . 3
131, 4, 11co 6129 . . . 4
141, 6, 11co 6129 . . . 4
1513, 14, 9co 6129 . . 3
1612, 15wceq 1654 . 2
178, 16wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  adddi  9130
  Copyright terms: Public domain W3C validator