Metamath Proof Explorer


Theorem in31

Description: A rearrangement of intersection. (Contributed by NM, 27-Aug-2012)

Ref Expression
Assertion in31 ⊢ A ∩ B ∩ C = C ∩ B ∩ A

Proof

Step Hyp Ref Expression
1 in12 ⊢ C ∩ A ∩ B = A ∩ C ∩ B
2 incom ⊢ A ∩ B ∩ C = C ∩ A ∩ B
3 incom ⊢ C ∩ B ∩ A = A ∩ C ∩ B
4 1 2 3 3eqtr4i ⊢ A ∩ B ∩ C = C ∩ B ∩ A