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

Metamath Proof Explorer

Theorem ssrind

Description: Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

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