Metamath Proof Explorer


Theorem inrot

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

Ref Expression
Assertion inrot ABC=CAB

Proof

Step Hyp Ref Expression
1 in31 ABC=CBA
2 in32 CBA=CAB
3 1 2 eqtri ABC=CAB