Axiom ax-hvcom 31482

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 31400	. . . 4 class ℋ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2145	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 401	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 31401	. . . 4 class +ℎ
8	1, 4, 7	co 7413	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7413	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1570	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is used by:  hvcomi  31500  hvaddlid  31504  hvadd32  31515  hvadd12  31516  hvpncan2  31521  hvsub32  31526  hvaddcan2  31552  hilablo  31641  hhssabloi  31743  shscom  31800  pjhtheu2  31897  pjpjpre  31900  pjpo  31909  spanunsni  32060  chscllem4  32121  hoaddcomi  32253  pjimai  32657  superpos  32835  sumdmdii  32896  cdj3lem3  32919  cdj3lem3b  32921