This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inss

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

		Ref	Expression
	Assertion	inss	$⊢ (A \subseteq C \lor B \subseteq C) \to A \cap B \subseteq C$

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	$⊢ (A \subseteq C \lor B \subseteq C) \to A \cap B \subseteq C$