Axiom ax-hvcom 30963

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

This axiom is referenced by:  hvcomi  30981  hvaddlid  30985  hvadd32  30996  hvadd12  30997  hvpncan2  31002  hvsub32  31007  hvaddcan2  31033  hilablo  31122  hhssabloi  31224  shscom  31281  pjhtheu2  31378  pjpjpre  31381  pjpo  31390  spanunsni  31541  chscllem4  31602  hoaddcomi  31734  pjimai  32138  superpos  32316  sumdmdii  32377  cdj3lem3  32400  cdj3lem3b  32402