Axiom ax-hvcom 31072

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

This axiom is referenced by:  hvcomi  31090  hvaddlid  31094  hvadd32  31105  hvadd12  31106  hvpncan2  31111  hvsub32  31116  hvaddcan2  31142  hilablo  31231  hhssabloi  31333  shscom  31390  pjhtheu2  31487  pjpjpre  31490  pjpo  31499  spanunsni  31650  chscllem4  31711  hoaddcomi  31843  pjimai  32247  superpos  32425  sumdmdii  32486  cdj3lem3  32509  cdj3lem3b  32511