no goals
ι : Type ?u.73226
α : Type u_1
β : Type ?u.73232
π : ι → Type ?u.73237
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
simp_rw [symmDiff_assoc, symmDiff_left_comm]