Axiom ax-hvcom 31020

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

This axiom is referenced by:  hvcomi  31038  hvaddlid  31042  hvadd32  31053  hvadd12  31054  hvpncan2  31059  hvsub32  31064  hvaddcan2  31090  hilablo  31179  hhssabloi  31281  shscom  31338  pjhtheu2  31435  pjpjpre  31438  pjpo  31447  spanunsni  31598  chscllem4  31659  hoaddcomi  31791  pjimai  32195  superpos  32373  sumdmdii  32434  cdj3lem3  32457  cdj3lem3b  32459