Axiom ax-hvcom 30983

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

This axiom is referenced by:  hvcomi  31001  hvaddlid  31005  hvadd32  31016  hvadd12  31017  hvpncan2  31022  hvsub32  31027  hvaddcan2  31053  hilablo  31142  hhssabloi  31244  shscom  31301  pjhtheu2  31398  pjpjpre  31401  pjpo  31410  spanunsni  31561  chscllem4  31622  hoaddcomi  31754  pjimai  32158  superpos  32336  sumdmdii  32397  cdj3lem3  32420  cdj3lem3b  32422