Axiom ax-hvcom 31161

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 31079	. . . 4 class ℋ
3	1, 2	wcel 2141	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2141	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 399	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 31080	. . . 4 class +ℎ
8	1, 4, 7	co 7391	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7391	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1559	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  31179  hvaddlid  31183  hvadd32  31194  hvadd12  31195  hvpncan2  31200  hvsub32  31205  hvaddcan2  31231  hilablo  31320  hhssabloi  31422  shscom  31479  pjhtheu2  31576  pjpjpre  31579  pjpo  31588  spanunsni  31739  chscllem4  31800  hoaddcomi  31932  pjimai  32336  superpos  32514  sumdmdii  32575  cdj3lem3  32598  cdj3lem3b  32600