Axiom ax-hvcom 10295

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 10212	. . . 4 class ~H
3	1, 2	wcel 1138	. . 3 wff A e. ~H
4		cB	. . . 4 class B
5	4, 2	wcel 1138	. . 3 wff B e. ~H
6	3, 5	wa 239	. 2 wff (A e. ~H /\ B e. ~H)
7		cva 10213	. . . 4 class +h
8	1, 4, 7	co 4695	. . 3 class (A +h B)
9	4, 1, 7	co 4695	. . 3 class (B +h A)
10	8, 9	wceq 1136	. 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 10313  hvaddid2 10316  hvadd23 10327  hvadd12 10328  hvpncan2 10333  hvaddcan2 10362  hilabl 10452  hhssabli 10557  pjtheu2i 10675  pjpj0i 10680  pjpo 10686  shscom 10708  spanunsni 10927  hoaddcomi 11127  hhlnoi 11255  pjimai 11540  superpos 11718  sumdmdii 11779  cdj3lem3 11802  cdj3lem3b 11804

Copyright terms: Public domain