Axiom ax-hvcom 30937

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

This axiom is referenced by:  hvcomi  30955  hvaddlid  30959  hvadd32  30970  hvadd12  30971  hvpncan2  30976  hvsub32  30981  hvaddcan2  31007  hilablo  31096  hhssabloi  31198  shscom  31255  pjhtheu2  31352  pjpjpre  31355  pjpo  31364  spanunsni  31515  chscllem4  31576  hoaddcomi  31708  pjimai  32112  superpos  32290  sumdmdii  32351  cdj3lem3  32374  cdj3lem3b  32376