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

Metamath Proof Explorer

Theorem ssinss1d

Description: Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	ssinss1d.1	$⊢ φ \to A \subseteq C$
	Assertion	ssinss1d	$⊢ φ \to A \cap B \subseteq C$

Step	Hyp	Ref	Expression
1		ssinss1d.1	$⊢ φ \to A \subseteq C$
2		ssinss1	$⊢ A \subseteq C \to A \cap B \subseteq C$
3	1 2	syl	$⊢ φ \to A \cap B \subseteq C$