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

Metamath Proof Explorer

Theorem inabs3

Description: Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	inabs3	$⊢ C \subseteq B \to (A \cap B) \cap C = A \cap C$

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap B) \cap C = A \cap (B \cap C)$
2		sseqin2	$⊢ C \subseteq B \leftrightarrow B \cap C = C$
3	2	biimpi	$⊢ C \subseteq B \to B \cap C = C$
4	3	ineq2d	$⊢ C \subseteq B \to A \cap (B \cap C) = A \cap C$
5	1 4	eqtrid	$⊢ C \subseteq B \to (A \cap B) \cap C = A \cap C$