Theorem inabs3

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

	Ref	Expression
Assertion	inabs3	|- ( C C_ B -> ( ( A i^i B ) i^i C ) = ( A i^i C ) )

Proof

Step	Hyp	Ref	Expression
1		inass	|- ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) )
2		sseqin2	|- ( C C_ B <-> ( B i^i C ) = C )
3	2	biimpi	|- ( C C_ B -> ( B i^i C ) = C )
4	3	ineq2d	|- ( C C_ B -> ( A i^i ( B i^i C ) ) = ( A i^i C ) )
5	1 4	syl5eq	|- ( C C_ B -> ( ( A i^i B ) i^i C ) = ( A i^i C ) )