Axiom ax-hvcom 31290

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 31208	. . . 4 class ℋ
3	1, 2	wcel 2149	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2149	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 400	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 31209	. . . 4 class +ℎ
8	1, 4, 7	co 7408	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7408	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1567	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  31308  hvaddlid  31312  hvadd32  31323  hvadd12  31324  hvpncan2  31329  hvsub32  31334  hvaddcan2  31360  hilablo  31449  hhssabloi  31551  shscom  31608  pjhtheu2  31705  pjpjpre  31708  pjpo  31717  spanunsni  31868  chscllem4  31929  hoaddcomi  32061  pjimai  32465  superpos  32643  sumdmdii  32704  cdj3lem3  32727  cdj3lem3b  32729