Axiom ax-hvcom 28430

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 28348	. . . 4 class ℋ
3	1, 2	wcel 2106	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2106	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 386	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 28349	. . . 4 class +ℎ
8	1, 4, 7	co 6922	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 6922	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1601	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  28448  hvaddid2  28452  hvadd32  28463  hvadd12  28464  hvpncan2  28469  hvsub32  28474  hvaddcan2  28500  hilablo  28589  hhssabloi  28691  shscom  28750  pjhtheu2  28847  pjpjpre  28850  pjpo  28859  spanunsni  29010  chscllem4  29071  hoaddcomi  29203  pjimai  29607  superpos  29785  sumdmdii  29846  cdj3lem3  29869  cdj3lem3b  29871