Axiom ax-hvcom 31660

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

This axiom is used by:  hvcomi  31678  hvaddlid  31682  hvadd32  31693  hvadd12  31694  hvpncan2  31699  hvsub32  31704  hvaddcan2  31730  hilablo  31819  hhssabloi  31921  shscom  31978  pjhtheu2  32075  pjpjpre  32078  pjpo  32087  spanunsni  32238  chscllem4  32299  hoaddcomi  32431  pjimai  32835  superpos  33013  sumdmdii  33074  cdj3lem3  33097  cdj3lem3b  33099