Axiom ax-hvcom 29342

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 29260	. . . 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 29261	. . . 4 class +ℎ
8	1, 4, 7	co 7268	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7268	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1541	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  29360  hvaddid2  29364  hvadd32  29375  hvadd12  29376  hvpncan2  29381  hvsub32  29386  hvaddcan2  29412  hilablo  29501  hhssabloi  29603  shscom  29660  pjhtheu2  29757  pjpjpre  29760  pjpo  29769  spanunsni  29920  chscllem4  29981  hoaddcomi  30113  pjimai  30517  superpos  30695  sumdmdii  30756  cdj3lem3  30779  cdj3lem3b  30781