Axiom ax-hvcom 27858

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 27776	. . . 4 class ℋ
3	1, 2	wcel 1990	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 1990	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 384	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 27777	. . . 4 class +ℎ
8	1, 4, 7	co 6650	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 6650	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1483	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  27876  hvaddid2  27880  hvadd32  27891  hvadd12  27892  hvpncan2  27897  hvsub32  27902  hvaddcan2  27928  hilablo  28017  hhssabloi  28119  shscom  28178  pjhtheu2  28275  pjpjpre  28278  pjpo  28287  spanunsni  28438  chscllem4  28499  hoaddcomi  28631  pjimai  29035  superpos  29213  sumdmdii  29274  cdj3lem3  29297  cdj3lem3b  29299