apply imply₂!
case mp.hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯) ⟶ (p✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯
no goals