Axiom ax-hvcom 27986

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		chil 27904	. . . 4 class ℋ
3	1, 2	wcel 2030	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2030	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 383	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 27905	. . . 4 class +ℎ
8	1, 4, 7	co 6690	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 6690	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1523	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  28004  hvaddid2  28008  hvadd32  28019  hvadd12  28020  hvpncan2  28025  hvsub32  28030  hvaddcan2  28056  hilablo  28145  hhssabloi  28247  shscom  28306  pjhtheu2  28403  pjpjpre  28406  pjpo  28415  spanunsni  28566  chscllem4  28627  hoaddcomi  28759  pjimai  29163  superpos  29341  sumdmdii  29402  cdj3lem3  29425  cdj3lem3b  29427