ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-distr Unicode version

Axiom ax-distr 6787
Description: Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 6758. Proofs should normally use adddi 6811 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
ax-distr  CC  CC  C  CC  x.  +  C  x.  +  x.  C

Detailed syntax breakdown of Axiom ax-distr
StepHypRef Expression
1 cA . . . 4
2 cc 6709 . . . 4  CC
31, 2wcel 1390 . . 3  CC
4 cB . . . 4
54, 2wcel 1390 . . 3  CC
6 cC . . . 4  C
76, 2wcel 1390 . . 3  C  CC
83, 5, 7w3a 884 . 2  CC  CC  C  CC
9 caddc 6714 . . . . 5  +
104, 6, 9co 5455 . . . 4  +  C
11 cmul 6716 . . . 4  x.
121, 10, 11co 5455 . . 3  x.  +  C
131, 4, 11co 5455 . . . 4  x.
141, 6, 11co 5455 . . . 4  x.  C
1513, 14, 9co 5455 . . 3  x.  +  x.  C
1612, 15wceq 1242 . 2  x.  +  C  x.  +  x.  C
178, 16wi 4 1  CC  CC  C  CC  x.  +  C  x.  +  x.  C
Colors of variables: wff set class
This axiom is referenced by:  adddi  6811
  Copyright terms: Public domain W3C validator