Theorem sslin

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999)

	Ref	Expression
Assertion	sslin	$$⊢A\subseteq B\to C\cap A\subseteq C\cap B$$

Proof

Step	Hyp	Ref	Expression
1		ssrin	$$⊢A\subseteq B\to A\cap C\subseteq B\cap C$$
2		incom	$$⊢C\cap A=A\cap C$$
3		incom	$$⊢C\cap B=B\cap C$$
4	1 2 3	3sstr4g	$$⊢A\subseteq B\to C\cap A\subseteq C\cap B$$