Axiom ax-hvcom 30979

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

This axiom is referenced by:  hvcomi  30997  hvaddlid  31001  hvadd32  31012  hvadd12  31013  hvpncan2  31018  hvsub32  31023  hvaddcan2  31049  hilablo  31138  hhssabloi  31240  shscom  31297  pjhtheu2  31394  pjpjpre  31397  pjpo  31406  spanunsni  31557  chscllem4  31618  hoaddcomi  31750  pjimai  32154  superpos  32332  sumdmdii  32393  cdj3lem3  32416  cdj3lem3b  32418