no goals
ι : Type ?u.70589
α : Type u_1
β : Type ?u.70595
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]