Axiom ax-hvcom 28778

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 28696	. . . 4 class ℋ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2114	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 398	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 28697	. . . 4 class +ℎ
8	1, 4, 7	co 7156	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7156	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1537	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  28796  hvaddid2  28800  hvadd32  28811  hvadd12  28812  hvpncan2  28817  hvsub32  28822  hvaddcan2  28848  hilablo  28937  hhssabloi  29039  shscom  29096  pjhtheu2  29193  pjpjpre  29196  pjpo  29205  spanunsni  29356  chscllem4  29417  hoaddcomi  29549  pjimai  29953  superpos  30131  sumdmdii  30192  cdj3lem3  30215  cdj3lem3b  30217