Axiom ax-hvcom 31612

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

This axiom is used by:  hvcomi  31630  hvaddlid  31634  hvadd32  31645  hvadd12  31646  hvpncan2  31651  hvsub32  31656  hvaddcan2  31682  hilablo  31771  hhssabloi  31873  shscom  31930  pjhtheu2  32027  pjpjpre  32030  pjpo  32039  spanunsni  32190  chscllem4  32251  hoaddcomi  32383  pjimai  32787  superpos  32965  sumdmdii  33026  cdj3lem3  33049  cdj3lem3b  33051