Metamath Proof Explorer


Axiom ax-distr

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

Ref Expression
Assertion ax-distr A B C A B + C = A B + A C

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class
2 0 1 wcel wff A
3 cB class B
4 3 1 wcel wff B
5 cC class C
6 5 1 wcel wff C
7 2 4 6 w3a wff A B C
8 cmul class ×
9 caddc class +
10 3 5 9 co class B + C
11 0 10 8 co class A B + C
12 0 3 8 co class A B
13 0 5 8 co class A C
14 12 13 9 co class A B + A C
15 11 14 wceq wff A B + C = A B + A C
16 7 15 wi wff A B C A B + C = A B + A C