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

Metamath Proof Explorer

Theorem ssind

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	ssind.1	$⊢ φ \to A \subseteq B$
	ssind.2	$⊢ φ \to A \subseteq C$
Assertion	ssind	$⊢ φ \to A \subseteq B \cap C$

Proof

Step	Hyp	Ref	Expression
1		ssind.1	$⊢ φ \to A \subseteq B$
2		ssind.2	$⊢ φ \to A \subseteq C$
3	1 2	jca	$⊢ φ \to (A \subseteq B \land A \subseteq C)$
4		ssin	$⊢ (A \subseteq B \land A \subseteq C) \leftrightarrow A \subseteq B \cap C$
5	3 4	sylib	$⊢ φ \to A \subseteq B \cap C$