Axiom ax-hvcom 30928

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 30846	. . . 4 class ℋ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2108	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 395	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 30847	. . . 4 class +ℎ
8	1, 4, 7	co 7403	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7403	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1540	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  30946  hvaddlid  30950  hvadd32  30961  hvadd12  30962  hvpncan2  30967  hvsub32  30972  hvaddcan2  30998  hilablo  31087  hhssabloi  31189  shscom  31246  pjhtheu2  31343  pjpjpre  31346  pjpo  31355  spanunsni  31506  chscllem4  31567  hoaddcomi  31699  pjimai  32103  superpos  32281  sumdmdii  32342  cdj3lem3  32365  cdj3lem3b  32367