Metamath Proof Explorer


Theorem shsel2i

Description: A subspace sum contains a member of one of its subspaces. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 AS
shincl.2 BS
Assertion shsel2i CBCA+B

Proof

Step Hyp Ref Expression
1 shincl.1 AS
2 shincl.2 BS
3 shsel2 ASBSCBCA+B
4 1 2 3 mp2an CBCA+B