Axiom ax-hvcom 31087

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

This axiom is referenced by:  hvcomi  31105  hvaddlid  31109  hvadd32  31120  hvadd12  31121  hvpncan2  31126  hvsub32  31131  hvaddcan2  31157  hilablo  31246  hhssabloi  31348  shscom  31405  pjhtheu2  31502  pjpjpre  31505  pjpo  31514  spanunsni  31665  chscllem4  31726  hoaddcomi  31858  pjimai  32262  superpos  32440  sumdmdii  32501  cdj3lem3  32524  cdj3lem3b  32526