no goals
ι : Type ?u.45050
α : Type u_1
β : Type ?u.45056
π : ι → Type ?u.45061
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]