Metamath Proof Explorer


Theorem inabs3

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

Ref Expression
Assertion inabs3 C B A B C = A C

Proof

Step Hyp Ref Expression
1 inass A B C = A B C
2 sseqin2 C B B C = C
3 2 biimpi C B B C = C
4 3 ineq2d C B A B C = A C
5 1 4 syl5eq C B A B C = A C