Theorem inabs3

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

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

Proof

Step	Hyp	Ref	Expression
1		inass	$$⊢\left(A\cap B\right)\cap C=A\cap \left(B\cap C\right)$$
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 \left(B\cap C\right)=A\cap C$$
5	1 4	syl5eq	$$⊢C\subseteq B\to \left(A\cap B\right)\cap C=A\cap C$$