Axiom ax-hvcom 31088

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

This axiom is referenced by:  hvcomi  31106  hvaddlid  31110  hvadd32  31121  hvadd12  31122  hvpncan2  31127  hvsub32  31132  hvaddcan2  31158  hilablo  31247  hhssabloi  31349  shscom  31406  pjhtheu2  31503  pjpjpre  31506  pjpo  31515  spanunsni  31666  chscllem4  31727  hoaddcomi  31859  pjimai  32263  superpos  32441  sumdmdii  32502  cdj3lem3  32525  cdj3lem3b  32527