ι : Type ?u.71182
α : Type u_1
β : Type ?u.71188
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
ι : Type ?u.71182
α : Type u_1
β : Type ?u.71188
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)
rw [le_inf_iff, le_himp_comm, sup_le_iff]
no goals
ι : Type ?u.71182
α : Type u_1
β : Type ?u.71188
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
simp_rw [le_himp_comm]