Metamath Proof Explorer


Theorem hvaddcli

Description: Closure of vector addition. (Contributed by NM, 1-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvaddcl.1
|- A e. ~H
hvaddcl.2
|- B e. ~H
Assertion hvaddcli
|- ( A +h B ) e. ~H

Proof

Step Hyp Ref Expression
1 hvaddcl.1
 |-  A e. ~H
2 hvaddcl.2
 |-  B e. ~H
3 hvaddcl
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H )
4 1 2 3 mp2an
 |-  ( A +h B ) e. ~H