Axiom ax-hvcom 30521

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 30439	. . . 4 class ℋ
3	1, 2	wcel 2104	. . 3 wff 𝐴 ∈ ℋ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2104	. . 3 wff 𝐵 ∈ ℋ
6	3, 5	wa 394	. 2 wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ)
7		cva 30440	. . . 4 class +ℎ
8	1, 4, 7	co 7411	. . 3 class (𝐴 +ℎ 𝐵)
9	4, 1, 7	co 7411	. . 3 class (𝐵 +ℎ 𝐴)
10	8, 9	wceq 1539	. 2 wff (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))

This axiom is referenced by:  hvcomi  30539  hvaddlid  30543  hvadd32  30554  hvadd12  30555  hvpncan2  30560  hvsub32  30565  hvaddcan2  30591  hilablo  30680  hhssabloi  30782  shscom  30839  pjhtheu2  30936  pjpjpre  30939  pjpo  30948  spanunsni  31099  chscllem4  31160  hoaddcomi  31292  pjimai  31696  superpos  31874  sumdmdii  31935  cdj3lem3  31958  cdj3lem3b  31960