Axiom ax-hvass 10296

Description: Vector addition is associative.

Assertion

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

Detailed syntax breakdown of Axiom ax-hvass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 10212	. . . 4 class ~H
3	1, 2	wcel 1138	. . 3 wff A e. ~H
4		cB	. . . 4 class B
5	4, 2	wcel 1138	. . 3 wff B e. ~H
6		cC	. . . 4 class C
7	6, 2	wcel 1138	. . 3 wff C e. ~H
8	3, 5, 7	w3a 855	. 2 wff (A e. ~H /\ B e. ~H /\ C e. ~H)
9		cva 10213	. . . . 5 class +h
10	1, 4, 9	co 4695	. . . 4 class (A +h B)
11	10, 6, 9	co 4695	. . 3 class ((A +h B) +h C)
12	4, 6, 9	co 4695	. . . 4 class (B +h C)
13	1, 12, 9	co 4695	. . 3 class (A +h (B +h C))
14	11, 13	wceq 1136	. 2 wff ((A +h B) +h C) = (A +h (B +h C))
15	8, 14	wi 3	1 wff ((A e. ~H /\ B e. ~H /\ C e. ~H) -> ((A +h B) +h C) = (A +h (B +h C)))

This axiom is referenced by:  hvadd23 10327  hvadd12 10328  hvadd4 10329  hvpncan 10332  hvaddsubass 10334  hvassi 10344  hilabl 10452  spanunsni 10927  hoaddassi 11131

Copyright terms: Public domain