Metamath Proof Explorer


Theorem inindir

Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 inidm
 |-  ( C i^i C ) = C
2 1 ineq2i
 |-  ( ( A i^i B ) i^i ( C i^i C ) ) = ( ( A i^i B ) i^i C )
3 in4
 |-  ( ( A i^i B ) i^i ( C i^i C ) ) = ( ( A i^i C ) i^i ( B i^i C ) )
4 2 3 eqtr3i
 |-  ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i ( B i^i C ) )