Metamath Proof Explorer

Theorem inrot

Description: Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012)

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

Proof

Step Hyp Ref Expression
1 in31 
 |-  ( ( A i^i B ) i^i C ) = ( ( C i^i B ) i^i A )
2 in32 
 |-  ( ( C i^i B ) i^i A ) = ( ( C i^i A ) i^i B )
3 1 2 eqtri 
 |-  ( ( A i^i B ) i^i C ) = ( ( C i^i A ) i^i B )