Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
inabs3
Next ⟩
pwpwuni
Metamath Proof Explorer
Ascii
Unicode
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