Axiom ax-hvcom 8871

Description: Vector addition is commutative.

Assertion

Ref	Expression
ax-hvcom	|- ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))

Detailed syntax breakdown of Axiom ax-hvcom

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 8788	. . . 4 class H~
3	1, 2	wcel 958	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 958	. . 3 wff B e. H~
6	3, 5	wa 223	. 2 wff (A e. H~ /\ B e. H~)
7		cva 8789	. . . 4 class +h
8	1, 4, 7	co 3963	. . 3 class (A +h B)
9	4, 1, 7	co 3963	. . 3 class (B +h A)
10	8, 9	wceq 956	. 2 wff (A +h B) = (B +h A)
11	6, 10	wi 3	1 wff ((A e. H~ /\ B e. H~) -> (A +h B) = (B +h A))

This axiom is referenced by:  hvcom 8889  hvaddid2t 8892  hvadd23t 8903  hvadd12t 8904  hvpncan2t 8909  hvaddcan2t 8938  hilabl 9027  hhssabl 9132  pjtheu2 9250  pjpj0 9255  pjpot 9261  shscomt 9283  spanunsn 9502  hoaddcom 9698  hhlno 9826  pjima 10104  superpos 10281  sumdmdi 10342  cdj3lem3 10365  cdj3lem3b 10367

Copyright terms: Public domain