Axiom ax-hvcom 31353

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

This axiom is referenced by:  hvcomi  31371  hvaddlid  31375  hvadd32  31386  hvadd12  31387  hvpncan2  31392  hvsub32  31397  hvaddcan2  31423  hilablo  31512  hhssabloi  31614  shscom  31671  pjhtheu2  31768  pjpjpre  31771  pjpo  31780  spanunsni  31931  chscllem4  31992  hoaddcomi  32124  pjimai  32528  superpos  32706  sumdmdii  32767  cdj3lem3  32790  cdj3lem3b  32792