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

Metamath Proof Explorer

Theorem ss2in

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000)

		Ref	Expression
	Assertion	ss2in	$⊢ (A \subseteq B \land C \subseteq D) \to A \cap C \subseteq B \cap D$

Step	Hyp	Ref	Expression
1		ssrin	$⊢ A \subseteq B \to A \cap C \subseteq B \cap C$
2		sslin	$⊢ C \subseteq D \to B \cap C \subseteq B \cap D$
3	1 2	sylan9ss	$⊢ (A \subseteq B \land C \subseteq D) \to A \cap C \subseteq B \cap D$