Axiom ax-hvcom 30949

Description: Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hvcom	⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

Detailed syntax breakdown of Axiom ax-hvcom

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		chba 30867	. . . 4 class ℋ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2109	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 395	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 30868	. . . 4 class +ℎ
8	1, 4, 7	co 7349	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7349	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1540	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  30967  hvaddlid  30971  hvadd32  30982  hvadd12  30983  hvpncan2  30988  hvsub32  30993  hvaddcan2  31019  hilablo  31108  hhssabloi  31210  shscom  31267  pjhtheu2  31364  pjpjpre  31367  pjpo  31376  spanunsni  31527  chscllem4  31588  hoaddcomi  31720  pjimai  32124  superpos  32302  sumdmdii  32363  cdj3lem3  32386  cdj3lem3b  32388