Theorem inss

Description: Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014)

	Ref	Expression
Assertion	inss	$$⊢\left(A\subseteq C\vee B\subseteq C\right)\to A\cap B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		ssinss1	$$⊢A\subseteq C\to A\cap B\subseteq C$$
2		incom	$$⊢A\cap B=B\cap A$$
3		ssinss1	$$⊢B\subseteq C\to B\cap A\subseteq C$$
4	2 3	eqsstrid	$$⊢B\subseteq C\to A\cap B\subseteq C$$
5	1 4	jaoi	$$⊢\left(A\subseteq C\vee B\subseteq C\right)\to A\cap B\subseteq C$$