Metamath Proof Explorer


Theorem shlessi

Description: Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 A S
shincl.2 B S
shless.1 C S
Assertion shlessi A B A + C B + C

Proof

Step Hyp Ref Expression
1 shincl.1 A S
2 shincl.2 B S
3 shless.1 C S
4 shless A S B S C S A B A + C B + C
5 4 ex A S B S C S A B A + C B + C
6 1 2 3 5 mp3an A B A + C B + C