Axiom ax-hvcom 31258

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

This axiom is referenced by:  hvcomi  31276  hvaddlid  31280  hvadd32  31291  hvadd12  31292  hvpncan2  31297  hvsub32  31302  hvaddcan2  31328  hilablo  31417  hhssabloi  31519  shscom  31576  pjhtheu2  31673  pjpjpre  31676  pjpo  31685  spanunsni  31836  chscllem4  31897  hoaddcomi  32029  pjimai  32433  superpos  32611  sumdmdii  32672  cdj3lem3  32695  cdj3lem3b  32697