Axiom ax-hvcom 31033

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 30951	. . . 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 30952	. . . 4 class +ℎ
8	1, 4, 7	co 7448	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7448	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1537	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  31051  hvaddlid  31055  hvadd32  31066  hvadd12  31067  hvpncan2  31072  hvsub32  31077  hvaddcan2  31103  hilablo  31192  hhssabloi  31294  shscom  31351  pjhtheu2  31448  pjpjpre  31451  pjpo  31460  spanunsni  31611  chscllem4  31672  hoaddcomi  31804  pjimai  32208  superpos  32386  sumdmdii  32447  cdj3lem3  32470  cdj3lem3b  32472