Axiom ax-hvcom 9146

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 9063	. . . 4 class H~
3	1, 2	wcel 994	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 994	. . 3 wff B e. H~
6	3, 5	wa 221	. 2 wff (A e. H~ /\ B e. H~)
7		cva 9064	. . . 4 class +h
8	1, 4, 7	co 4021	. . 3 class (A +h B)
9	4, 1, 7	co 4021	. . 3 class (B +h A)
10	8, 9	wceq 992	. 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:  hvcomi 9164  hvaddid2 9167  hvadd23 9178  hvadd12 9179  hvpncan2 9184  hvaddcan2 9213  hilabl 9303  hhssabli 9408  pjtheu2i 9526  pjpj0i 9531  pjpo 9537  shscom 9559  spanunsni 9778  hoaddcomi 9978  hhlnoi 10106  pjimai 10384  superpos 10562  sumdmdii 10624  cdj3lem3 10647  cdj3lem3b 10649

Copyright terms: Public domain