Axiom ax-hvcom 31076

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

This axiom is referenced by:  hvcomi  31094  hvaddlid  31098  hvadd32  31109  hvadd12  31110  hvpncan2  31115  hvsub32  31120  hvaddcan2  31146  hilablo  31235  hhssabloi  31337  shscom  31394  pjhtheu2  31491  pjpjpre  31494  pjpo  31503  spanunsni  31654  chscllem4  31715  hoaddcomi  31847  pjimai  32251  superpos  32429  sumdmdii  32490  cdj3lem3  32513  cdj3lem3b  32515