Axiom ax-hvcom 27242

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		chil 27160	. . . 4 class ℋ
3	1, 2	wcel 1977	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 1977	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 383	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 27161	. . . 4 class +ℎ
8	1, 4, 7	co 6549	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 6549	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1475	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  27260  hvaddid2  27264  hvadd32  27275  hvadd12  27276  hvpncan2  27281  hvsub32  27286  hvaddcan2  27312  hilablo  27401  hhssabloi  27503  shscom  27562  pjhtheu2  27659  pjpjpre  27662  pjpo  27671  spanunsni  27822  chscllem4  27883  hoaddcomi  28015  pjimai  28419  superpos  28597  sumdmdii  28658  cdj3lem3  28681  cdj3lem3b  28683