Axiom ax-hvcom 31596

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

This axiom is used by:  hvcomi  31614  hvaddlid  31618  hvadd32  31629  hvadd12  31630  hvpncan2  31635  hvsub32  31640  hvaddcan2  31666  hilablo  31755  hhssabloi  31857  shscom  31914  pjhtheu2  32011  pjpjpre  32014  pjpo  32023  spanunsni  32174  chscllem4  32235  hoaddcomi  32367  pjimai  32771  superpos  32949  sumdmdii  33010  cdj3lem3  33033  cdj3lem3b  33035