ι : Type ?u.75762
α : Type u_1
β : Type ?u.75768
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
ι : Type ?u.75762
α : Type u_1
β : Type ?u.75768
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
no goals
ι : Type ?u.75762
α : Type u_1
β : Type ?u.75768
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
exact himp_inf_le.trans le_himp_himp