Axiom ax-hvcom 28784

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

This axiom is referenced by:  hvcomi  28802  hvaddid2  28806  hvadd32  28817  hvadd12  28818  hvpncan2  28823  hvsub32  28828  hvaddcan2  28854  hilablo  28943  hhssabloi  29045  shscom  29102  pjhtheu2  29199  pjpjpre  29202  pjpo  29211  spanunsni  29362  chscllem4  29423  hoaddcomi  29555  pjimai  29959  superpos  30137  sumdmdii  30198  cdj3lem3  30221  cdj3lem3b  30223