Axiom ax-hvcom 31400

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 31318	. . . 4 class ℋ
3	1, 2	wcel 2146	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2146	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 401	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 31319	. . . 4 class +ℎ
8	1, 4, 7	co 7416	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7416	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1570	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is used by:  hvcomi  31418  hvaddlid  31422  hvadd32  31433  hvadd12  31434  hvpncan2  31439  hvsub32  31444  hvaddcan2  31470  hilablo  31559  hhssabloi  31661  shscom  31718  pjhtheu2  31815  pjpjpre  31818  pjpo  31827  spanunsni  31978  chscllem4  32039  hoaddcomi  32171  pjimai  32575  superpos  32753  sumdmdii  32814  cdj3lem3  32837  cdj3lem3b  32839