Axiom ax-hvcom 31090

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 31008	. . . 4 class ℋ
3	1, 2	wcel 2119	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2119	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 396	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 31009	. . . 4 class +ℎ
8	1, 4, 7	co 7356	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7356	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1547	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  31108  hvaddlid  31112  hvadd32  31123  hvadd12  31124  hvpncan2  31129  hvsub32  31134  hvaddcan2  31160  hilablo  31249  hhssabloi  31351  shscom  31408  pjhtheu2  31505  pjpjpre  31508  pjpo  31517  spanunsni  31668  chscllem4  31729  hoaddcomi  31861  pjimai  32265  superpos  32443  sumdmdii  32504  cdj3lem3  32527  cdj3lem3b  32529