Metamath Proof Explorer


Axiom ax-hvdistr1

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hvdistr1 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 chba class
5 3 4 wcel wff B
6 cC class C
7 6 4 wcel wff C
8 2 5 7 w3a wff A B C
9 csm class
10 cva class +
11 3 6 10 co class B + C
12 0 11 9 co class A B + C
13 0 3 9 co class A B
14 0 6 9 co class A C
15 13 14 10 co class A B + A C
16 12 15 wceq wff A B + C = A B + A C
17 8 16 wi wff A B C A B + C = A B + A C