Metamath Proof Explorer

Theorem inindi

Description: Intersection distributes over itself. (Contributed by NM, 6-May-1994)

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

Proof

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