Axiom ax-hvcom 29408

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 29326	. . . 4 class ℋ
3	1, 2	wcel 2104	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2104	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 397	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 29327	. . . 4 class +ℎ
8	1, 4, 7	co 7307	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7307	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1539	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  29426  hvaddid2  29430  hvadd32  29441  hvadd12  29442  hvpncan2  29447  hvsub32  29452  hvaddcan2  29478  hilablo  29567  hhssabloi  29669  shscom  29726  pjhtheu2  29823  pjpjpre  29826  pjpo  29835  spanunsni  29986  chscllem4  30047  hoaddcomi  30179  pjimai  30583  superpos  30761  sumdmdii  30822  cdj3lem3  30845  cdj3lem3b  30847