Metamath Proof Explorer


Theorem hvsubcli

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

Ref Expression
Hypotheses hvaddcl.1 A
hvaddcl.2 B
Assertion hvsubcli A - B

Proof

Step Hyp Ref Expression
1 hvaddcl.1 A
2 hvaddcl.2 B
3 hvsubcl A B A - B
4 1 2 3 mp2an A - B