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 AB

Proof

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