Axiom ax-hvass 4986

Description: Vector addition is associative.

Assertion

Ref	Expression
ax-hvass	|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) +v C) = (A +v (B +v C)))

Detailed syntax breakdown of Axiom ax-hvass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class H~
3	1, 2	wcel 1092	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B e. H~
6		cC	. . . 4 class C
7	6, 2	wcel 1092	. . 3 wff C e. H~
8	3, 5, 7	w3a 581	. 2 wff (A e. H~ /\ B e. H~ /\ C e. H~)
9		cva 4959	. . . . 5 class +v
10	1, 4, 9	co 3001	. . . 4 class (A +v B)
11	10, 6, 9	co 3001	. . 3 class ((A +v B) +v C)
12	4, 6, 9	co 3001	. . . 4 class (B +v C)
13	1, 12, 9	co 3001	. . 3 class (A +v (B +v C))
14	11, 13	wceq 1091	. 2 wff ((A +v B) +v C) = (A +v (B +v C))
15	8, 14	wi 2	1 wff ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) +v C) = (A +v (B +v C)))

This axiom is referenced by:  hvadd23t 5011  hvadd12t 5012  hvadd4t 5013  hvsubcan1t 5016  hvaddsubasst 5018  hvass 5025  spanunsn 5482  hosass 5607

metamath.org