Metamath Proof Explorer


Theorem inindir

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

Ref Expression
Assertion inindir A B C = A C B C

Proof

Step Hyp Ref Expression
1 inidm C C = C
2 1 ineq2i A B C C = A B C
3 in4 A B C C = A C B C
4 2 3 eqtr3i A B C = A C B C