no goals
α : Type u_1
β : Type ?u.182360
γ : Type ?u.182363
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ s₃ ∩ s₂
simp only [mem_inter, and_right_comm]