Axiom ax-hvcom 30930

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 30848	. . . 4 class ℋ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2109	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 395	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 30849	. . . 4 class +ℎ
8	1, 4, 7	co 7387	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7387	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1540	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  30948  hvaddlid  30952  hvadd32  30963  hvadd12  30964  hvpncan2  30969  hvsub32  30974  hvaddcan2  31000  hilablo  31089  hhssabloi  31191  shscom  31248  pjhtheu2  31345  pjpjpre  31348  pjpo  31357  spanunsni  31508  chscllem4  31569  hoaddcomi  31701  pjimai  32105  superpos  32283  sumdmdii  32344  cdj3lem3  32367  cdj3lem3b  32369