Metamath Proof Explorer


Theorem hvmulcli

Description: Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvmulcl.1 A
hvmulcl.2 B
Assertion hvmulcli A B

Proof

Step Hyp Ref Expression
1 hvmulcl.1 A
2 hvmulcl.2 B
3 hvmulcl A B A B
4 1 2 3 mp2an A B