Axiom ax-hvcom 29372

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 29290	. . . 4 class ℋ
3	1, 2	wcel 2110	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2110	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 396	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 29291	. . . 4 class +ℎ
8	1, 4, 7	co 7272	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7272	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1542	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  29390  hvaddid2  29394  hvadd32  29405  hvadd12  29406  hvpncan2  29411  hvsub32  29416  hvaddcan2  29442  hilablo  29531  hhssabloi  29633  shscom  29690  pjhtheu2  29787  pjpjpre  29790  pjpo  29799  spanunsni  29950  chscllem4  30011  hoaddcomi  30143  pjimai  30547  superpos  30725  sumdmdii  30786  cdj3lem3  30809  cdj3lem3b  30811