Metamath Proof Explorer

Theorem inin

Description: Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion inin 
|- ( A i^i ( A i^i B ) ) = ( A i^i B )

Proof

Step Hyp Ref Expression
1 in13 
 |-  ( A i^i ( A i^i B ) ) = ( B i^i ( A i^i A ) )
2 inidm 
 |-  ( A i^i A ) = A
3 2 ineq2i 
 |-  ( B i^i ( A i^i A ) ) = ( B i^i A )
4 incom 
 |-  ( B i^i A ) = ( A i^i B )
5 1 3 4 3eqtri 
 |-  ( A i^i ( A i^i B ) ) = ( A i^i B )