Axiom ax-hvcom 8792

Description: Vector addition is commutative.

Assertion

Ref	Expression
ax-hvcom	⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (A +h B) = (B +h A))

Detailed syntax breakdown of Axiom ax-hvcom

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 8727	. . . 4 class ℋ
3	1, 2	wcel 955	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 955	. . 3 wff B ∈ ℋ
6	3, 5	wa 223	. 2 wff (A ∈ ℋ ⋀ B ∈ ℋ )
7		cva 8728	. . . 4 class +h
8	1, 4, 7	co 3948	. . 3 class (A +h B)
9	4, 1, 7	co 3948	. . 3 class (B +h A)
10	8, 9	wceq 953	. 2 wff (A +h B) = (B +h A)
11	6, 10	wi 3	1 wff ((A ∈ ℋ ⋀ B ∈ ℋ ) → (A +h B) = (B +h A))

This axiom is referenced by:  hvcom 8810  hvaddid2t 8813  hvadd23t 8824  hvadd12t 8825  hvpncan2t 8830  hvaddcan2t 8859  hilabl 8948  hhssabl 9053  pjtheu2 9165  pjpj0 9170  pjpot 9176  shscomt 9198  spanunsn 9419  hoaddcom 9615  hhlno 9743  pjima 10015  superpos 10189  sumdmdi 10249  cdj3lem3 10270  cdj3lem3b 10272

Copyright terms: Public domain