Axiom ax-hvcom 28772

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

This axiom is referenced by:  hvcomi  28790  hvaddid2  28794  hvadd32  28805  hvadd12  28806  hvpncan2  28811  hvsub32  28816  hvaddcan2  28842  hilablo  28931  hhssabloi  29033  shscom  29090  pjhtheu2  29187  pjpjpre  29190  pjpo  29199  spanunsni  29350  chscllem4  29411  hoaddcomi  29543  pjimai  29947  superpos  30125  sumdmdii  30186  cdj3lem3  30209  cdj3lem3b  30211