Axiom ax-hvcom 30254

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

This axiom is referenced by:  hvcomi  30272  hvaddlid  30276  hvadd32  30287  hvadd12  30288  hvpncan2  30293  hvsub32  30298  hvaddcan2  30324  hilablo  30413  hhssabloi  30515  shscom  30572  pjhtheu2  30669  pjpjpre  30672  pjpo  30681  spanunsni  30832  chscllem4  30893  hoaddcomi  31025  pjimai  31429  superpos  31607  sumdmdii  31668  cdj3lem3  31691  cdj3lem3b  31693