Axiom ax-hvcom 30985

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

This axiom is referenced by:  hvcomi  31003  hvaddlid  31007  hvadd32  31018  hvadd12  31019  hvpncan2  31024  hvsub32  31029  hvaddcan2  31055  hilablo  31144  hhssabloi  31246  shscom  31303  pjhtheu2  31400  pjpjpre  31403  pjpo  31412  spanunsni  31563  chscllem4  31624  hoaddcomi  31756  pjimai  32160  superpos  32338  sumdmdii  32399  cdj3lem3  32422  cdj3lem3b  32424